From b99084a9df2154a53974a3bc6825eb694efaa5a0 Mon Sep 17 00:00:00 2001 From: damiano Date: Wed, 13 Mar 2024 20:53:15 +0000 Subject: [PATCH] chore: remove unused tactics (#11351) I removed some of the tactics that were not used and are hopefully uncontroversial arising from the linter at #11308. As the commit messages should convey, the removed tactics are, essentially, ``` push_cast norm_cast congr norm_num dsimp funext intro infer_instance ``` --- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean | 4 ---- Mathlib/Algebra/Lie/Classical.lean | 1 - Mathlib/AlgebraicGeometry/AffineScheme.lean | 2 +- Mathlib/Analysis/Analytic/Basic.lean | 1 - Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean | 1 - Mathlib/Analysis/Calculus/Taylor.lean | 1 - Mathlib/Analysis/Convex/Uniform.lean | 1 - Mathlib/Analysis/Normed/Group/AddCircle.lean | 1 - Mathlib/Analysis/NormedSpace/AddTorsor.lean | 1 - Mathlib/Analysis/SpecialFunctions/CompareExp.lean | 2 +- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean | 1 - Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean | 4 ---- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean | 2 +- Mathlib/Analysis/SpecificLimits/Normed.lean | 1 - Mathlib/CategoryTheory/Abelian/Exact.lean | 3 +-- Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean | 1 - Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean | 2 +- Mathlib/Geometry/RingedSpace/Basic.lean | 1 - Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean | 1 - Mathlib/MeasureTheory/Function/UniformIntegrable.lean | 3 +-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean | 1 - Mathlib/NumberTheory/LegendreSymbol/Basic.lean | 2 -- Mathlib/Probability/Independence/Conditional.lean | 3 +-- Mathlib/RingTheory/FinitePresentation.lean | 1 - Mathlib/RingTheory/Ideal/MinimalPrime.lean | 1 - Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean | 2 +- Mathlib/RingTheory/RingHom/Finite.lean | 4 ++-- Mathlib/RingTheory/UniqueFactorizationDomain.lean | 4 ++-- Mathlib/Topology/Category/Stonean/Limits.lean | 1 - Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean | 2 -- Mathlib/Topology/MetricSpace/GromovHausdorff.lean | 1 - Mathlib/Topology/MetricSpace/Holder.lean | 1 - 32 files changed, 12 insertions(+), 45 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index 48a1a830e2d67..9b07bf71b5cf9 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -88,7 +88,6 @@ def μ (α β : Type u) : (free R).obj α ⊗ (free R).obj β ≅ (free R).obj ( theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') : ((free R).map f ⊗ (free R).map g) ≫ (μ R Y Y').hom = (μ R X X').hom ≫ (free R).map (f ⊗ g) := by - intros -- Porting note (#11041): broken ext apply TensorProduct.ext apply Finsupp.lhom_ext' @@ -113,7 +112,6 @@ theorem μ_natural {X Y X' Y' : Type u} (f : X ⟶ Y) (g : X' ⟶ Y') : theorem left_unitality (X : Type u) : (λ_ ((free R).obj X)).hom = (ε R ⊗ 𝟙 ((free R).obj X)) ≫ (μ R (𝟙_ (Type u)) X).hom ≫ map (free R).obj (λ_ X).hom := by - intros -- Porting note (#11041): broken ext apply TensorProduct.ext apply LinearMap.ext_ring @@ -134,7 +132,6 @@ theorem left_unitality (X : Type u) : theorem right_unitality (X : Type u) : (ρ_ ((free R).obj X)).hom = (𝟙 ((free R).obj X) ⊗ ε R) ≫ (μ R X (𝟙_ (Type u))).hom ≫ map (free R).obj (ρ_ X).hom := by - intros -- Porting note (#11041): broken ext apply TensorProduct.ext apply Finsupp.lhom_ext' @@ -156,7 +153,6 @@ theorem associativity (X Y Z : Type u) : ((μ R X Y).hom ⊗ 𝟙 ((free R).obj Z)) ≫ (μ R (X ⊗ Y) Z).hom ≫ map (free R).obj (α_ X Y Z).hom = (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫ (𝟙 ((free R).obj X) ⊗ (μ R Y Z).hom) ≫ (μ R X (Y ⊗ Z)).hom := by - intros -- Porting note (#11041): broken ext apply TensorProduct.ext apply TensorProduct.ext diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index 448ec7725eccc..b9304d423ec62 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -272,7 +272,6 @@ theorem jd_transform [Fintype l] : (PD l R)ᵀ * JD l R * PD l R = (2 : R) • S have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply] rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul] - congr simp [two_smul] #align lie_algebra.orthogonal.JD_transform LieAlgebra.Orthogonal.jd_transform diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 45fa777026f52..550bca2881f1d 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -220,7 +220,7 @@ theorem Scheme.map_PrimeSpectrum_basicOpen_of_affine change SpecΓIdentity.hom.app (X.presheaf.obj <| op ⊤) = _ rw [← ΓSpec.adjunction_unit_app_app_top X] rfl - · dsimp; congr + · dsimp refine' (Scheme.preimage_basicOpen _ _).trans _ congr 1 exact IsIso.inv_hom_id_apply _ _ diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 1caf3f1d27741..49106266a3638 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -1448,7 +1448,6 @@ theorem hasFPowerSeriesAt_iff : simp only [dist_zero_right] at h apply FormalMultilinearSeries.le_radius_of_tendsto convert tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero - funext simp [norm_smul, mul_comm] refine' lt_of_lt_of_le _ this simp only [ENNReal.coe_pos] diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean index 43a2ca2d8f711..079a96fc96ffa 100644 --- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean +++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean @@ -300,7 +300,6 @@ theorem mkPiRing_coeff_eq (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : @[simp] theorem apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n := by convert (p n).toMultilinearMap.map_smul_univ y 1 - funext simp only [Pi.one_apply, Algebra.id.smul_eq_mul, mul_one] #align formal_multilinear_series.apply_eq_prod_smul_coeff FormalMultilinearSeries.apply_eq_prod_smul_coeff diff --git a/Mathlib/Analysis/Calculus/Taylor.lean b/Mathlib/Analysis/Calculus/Taylor.lean index b4f526f09be3a..0e65eded7722d 100644 --- a/Mathlib/Analysis/Calculus/Taylor.lean +++ b/Mathlib/Analysis/Calculus/Taylor.lean @@ -184,7 +184,6 @@ theorem hasDerivWithinAt_taylorWithinEval {f : ℝ → E} {x y : ℝ} {n : ℕ} mul_one, zero_add, one_smul] simp only [iteratedDerivWithin_zero] at hf' rw [iteratedDerivWithin_one (hs_unique _ (h hy))] - norm_num exact hf'.hasDerivWithinAt.mono h simp_rw [Nat.add_succ, taylorWithinEval_succ] simp only [add_zero, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one] diff --git a/Mathlib/Analysis/Convex/Uniform.lean b/Mathlib/Analysis/Convex/Uniform.lean index 80ee8397e683a..66da4113e1403 100644 --- a/Mathlib/Analysis/Convex/Uniform.lean +++ b/Mathlib/Analysis/Convex/Uniform.lean @@ -120,7 +120,6 @@ theorem exists_forall_closed_ball_dist_add_le_two_mul_sub (hε : 0 < ε) (r : obtain ⟨δ, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (div_pos hε hr) refine' ⟨δ * r, mul_pos hδ hr, fun x hx y hy hxy => _⟩ rw [← div_le_one hr, div_eq_inv_mul, ← norm_smul_of_nonneg (inv_nonneg.2 hr.le)] at hx hy - try infer_instance have := h hx hy simp_rw [← smul_add, ← smul_sub, norm_smul_of_nonneg (inv_nonneg.2 hr.le), ← div_eq_inv_mul, div_le_div_right hr, div_le_iff hr, sub_mul] at this diff --git a/Mathlib/Analysis/Normed/Group/AddCircle.lean b/Mathlib/Analysis/Normed/Group/AddCircle.lean index fa7b3ebbb33cc..ea7c84deca1f5 100644 --- a/Mathlib/Analysis/Normed/Group/AddCircle.lean +++ b/Mathlib/Analysis/Normed/Group/AddCircle.lean @@ -87,7 +87,6 @@ theorem norm_eq {x : ℝ} : ‖(x : AddCircle p)‖ = |x - round (p⁻¹ * x) * suffices ∀ x : ℝ, ‖(x : AddCircle (1 : ℝ))‖ = |x - round x| by rcases eq_or_ne p 0 with (rfl | hp) · simp - intros have hx := norm_coe_mul p x p⁻¹ rw [abs_inv, eq_inv_mul_iff_mul_eq₀ ((not_congr abs_eq_zero).mpr hp)] at hx rw [← hx, inv_mul_cancel hp, this, ← abs_mul, mul_sub, mul_inv_cancel_left₀ hp, mul_comm p] diff --git a/Mathlib/Analysis/NormedSpace/AddTorsor.lean b/Mathlib/Analysis/NormedSpace/AddTorsor.lean index 26116f4d0f558..c98c0c890469e 100644 --- a/Mathlib/Analysis/NormedSpace/AddTorsor.lean +++ b/Mathlib/Analysis/NormedSpace/AddTorsor.lean @@ -212,7 +212,6 @@ theorem nndist_right_midpoint (p₁ p₂ : P) : theorem dist_midpoint_midpoint_le' (p₁ p₂ p₃ p₄ : P) : dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖(2 : 𝕜)‖ := by rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, midpoint_vsub_midpoint] - try infer_instance rw [midpoint_eq_smul_add, norm_smul, invOf_eq_inv, norm_inv, ← div_eq_inv_mul] exact div_le_div_of_nonneg_right (norm_add_le _ _) (norm_nonneg _) #align dist_midpoint_midpoint_le' dist_midpoint_midpoint_le' diff --git a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean index a37b621052846..8f707ef0ff250 100644 --- a/Mathlib/Analysis/SpecialFunctions/CompareExp.lean +++ b/Mathlib/Analysis/SpecialFunctions/CompareExp.lean @@ -59,7 +59,7 @@ theorem of_isBigO_im_re_rpow (hre : Tendsto re l atTop) (r : ℝ) (hr : im =O[l] ⟨hre, fun n => IsLittleO.isBigO <| calc - (fun z : ℂ => z.im ^ n) =O[l] fun z => (z.re ^ r) ^ n := by norm_cast; exact hr.pow n + (fun z : ℂ => z.im ^ n) =O[l] fun z => (z.re ^ r) ^ n := hr.pow n _ =ᶠ[l] fun z => z.re ^ (r * n) := ((hre.eventually_ge_atTop 0).mono fun z hz => by simp only [Real.rpow_mul hz r n, Real.rpow_nat_cast]) diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean index fc888f0701d92..ae538b2ddd1ef 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean @@ -100,7 +100,6 @@ lemma hasDerivAt_logTaylor (n : ℕ) (z : ℂ) : lemma hasDerivAt_log_sub_logTaylor (n : ℕ) {z : ℂ} (hz : 1 + z ∈ slitPlane) : HasDerivAt (fun z : ℂ ↦ log (1 + z) - logTaylor (n + 1) z) ((-z) ^ n * (1 + z)⁻¹) z := by convert ((hasDerivAt_log hz).comp_const_add 1 z).sub (hasDerivAt_logTaylor n z) using 1 - push_cast have hz' : -z ≠ 1 := by intro H rw [neg_eq_iff_eq_neg] at H diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean index 24080f85e1e00..45379635d715c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean @@ -122,16 +122,12 @@ theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) : /-- The function `x ^ (1 / x)` tends to `1` at `+∞`. -/ theorem tendsto_rpow_div : Tendsto (fun x => x ^ ((1 : ℝ) / x)) atTop (𝓝 1) := by convert tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one - funext - congr 2 ring #align tendsto_rpow_div tendsto_rpow_div /-- The function `x ^ (-1 / x)` tends to `1` at `+∞`. -/ theorem tendsto_rpow_neg_div : Tendsto (fun x => x ^ (-(1 : ℝ) / x)) atTop (𝓝 1) := by convert tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one - funext - congr 2 ring #align tendsto_rpow_neg_div tendsto_rpow_neg_div diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean index 88d9640b53815..1a5eb46b0ecfa 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean @@ -33,7 +33,7 @@ theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1 have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 := by rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul, add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub] - congr 3; ring_nf + ring_nf rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm] refine' exists_congr fun x => _ refine' (iff_of_eq <| congr_arg _ _).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index f7a489aee6f01..d15194562c793 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -659,7 +659,6 @@ theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded (hfa : Antitone convert hf0.neg norm_num convert (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg - funext simp #align antitone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded diff --git a/Mathlib/CategoryTheory/Abelian/Exact.lean b/Mathlib/CategoryTheory/Abelian/Exact.lean index 5f3b3cd2e303b..b96e4c7fe1889 100644 --- a/Mathlib/CategoryTheory/Abelian/Exact.lean +++ b/Mathlib/CategoryTheory/Abelian/Exact.lean @@ -77,8 +77,7 @@ theorem exact_iff : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f · refine kernel.lift (cokernel.π f) u ?_ ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso _).inv rw [← kernel.lift_ι g u hu, Category.assoc, h.2, comp_zero] · aesop_cat - · intros - rw [← cancel_mono (imageSubobject f).arrow, h] + · rw [← cancel_mono (imageSubobject f).arrow, h] simp #align category_theory.abelian.exact_iff CategoryTheory.Abelian.exact_iff diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean index 096831555b3b9..2f0b73859092f 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean @@ -126,7 +126,6 @@ lemma le_sum_distinctPairs_edgeDensity_sq (x : {i // i ∈ P.parts.offDiag}) (h ((if G.IsUniform ε x.1.1 x.1.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤ (∑ i in distinctPairs G ε hP x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ P.parts.card := by rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm] - push_cast split_ifs with h · rw [add_zero] exact edgeDensity_chunk_uniform hPα hPε _ _ diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index 2a6c2c7335d0c..ff85af4725ab2 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -79,7 +79,7 @@ theorem oangle_zero_right (x : V) : o.oangle x 0 = 0 := by simp [oangle] /-- If the two vectors passed to `oangle` are the same, the result is 0. -/ @[simp] theorem oangle_self (x : V) : o.oangle x x = 0 := by - rw [oangle, kahler_apply_self, ← ofReal_pow]; norm_cast + rw [oangle, kahler_apply_self, ← ofReal_pow] convert QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π)) apply arg_ofReal_of_nonneg positivity diff --git a/Mathlib/Geometry/RingedSpace/Basic.lean b/Mathlib/Geometry/RingedSpace/Basic.lean index 3fce79d04166f..fe009c9e06ccb 100644 --- a/Mathlib/Geometry/RingedSpace/Basic.lean +++ b/Mathlib/Geometry/RingedSpace/Basic.lean @@ -218,7 +218,6 @@ theorem basicOpen_mul {U : Opens X} (f g : X.presheaf.obj (op U)) : ext1 dsimp [RingedSpace.basicOpen] rw [← Set.image_inter Subtype.coe_injective] - congr ext x simp [map_mul, Set.mem_image] set_option linter.uppercaseLean3 false in diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index 41e360854167d..e85698877198e 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -187,7 +187,6 @@ theorem affineIndependent_iff_finrank_vectorSpan_eq [Fintype ι] (p : ι → P) rw [affineIndependent_iff_linearIndependent_vsub _ _ i₁, linearIndependent_iff_card_eq_finrank_span, eq_comm, vectorSpan_range_eq_span_range_vsub_right_ne k p i₁, Set.finrank] - congr rw [← Finset.card_univ] at hc rw [Fintype.subtype_card] simp [Finset.filter_ne', Finset.card_erase_of_mem, hc] diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index e1be6d6b52a5d..6be572c779cd3 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -664,8 +664,7 @@ theorem unifIntegrable_of' (hp : 1 ≤ p) (hp' : p ≠ ∞) {f : ι → α → change _ = fun x => (s ∩ { x : α | C ≤ ‖f i x‖₊ }).indicator (f i) x + (s ∩ { x : α | ‖f i x‖₊ < C }).indicator (f i) x rw [← Set.indicator_union_of_disjoint] - · congr - rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_lt] : + · rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_lt] : { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ), Set.inter_univ] · refine' (Disjoint.inf_right' _ _).inf_left' _ diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean index bd8318e8f0a2c..e6bb682ff9c2e 100644 --- a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean +++ b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean @@ -464,7 +464,6 @@ theorem AECover.integrable_of_integral_norm_bounded [l.NeBot] [l.IsCountablyGene rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict] conv at hbounded in ENNReal.ofReal _ => - dsimp rw [← coe_nnnorm] rw [ENNReal.ofReal_coe_nnreal] refine' hbounded.mono fun i hi => _ diff --git a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean index c7400e21c4da3..5140b5e3af38f 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/Basic.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/Basic.lean @@ -127,8 +127,6 @@ theorem eq_pow (a : ℤ) : (legendreSym p a : ZMod p) = (a : ZMod p) ^ (p / 2) : · tauto · simp · convert quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p) - norm_cast - congr exact (card p).symm #align legendre_sym.eq_pow legendreSym.eq_pow diff --git a/Mathlib/Probability/Independence/Conditional.lean b/Mathlib/Probability/Independence/Conditional.lean index 76ad2f39b4047..1927cab67d1f1 100644 --- a/Mathlib/Probability/Independence/Conditional.lean +++ b/Mathlib/Probability/Independence/Conditional.lean @@ -231,8 +231,7 @@ lemma iCondIndepSets_singleton_iff (s : ι → Set Ω) (hπ : ∀ i, MeasurableS apply congr_arg₂ · exact Set.iInter₂_congr hf · rfl - · congr - simp_rw [Finset.prod_apply] + · simp_rw [Finset.prod_apply] refine Finset.prod_congr rfl (fun i hi ↦ ?_) rw [hf i hi] · simpa only [Set.mem_singleton_iff, forall_eq] diff --git a/Mathlib/RingTheory/FinitePresentation.lean b/Mathlib/RingTheory/FinitePresentation.lean index 68e70be56887a..b12fd66b899a9 100644 --- a/Mathlib/RingTheory/FinitePresentation.lean +++ b/Mathlib/RingTheory/FinitePresentation.lean @@ -238,7 +238,6 @@ theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX) (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })] refine congrArg (Subalgebra.restrictScalars R) ?_ - congr 1 rw [adjoin_algebraMap, ht] apply Subalgebra.restrictScalars_injective R rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top, diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index acd2f18fb49bc..d947ab6517d4a 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -75,7 +75,6 @@ theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.mi @[simp] theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes := by rw [Ideal.minimalPrimes, Ideal.minimalPrimes] - congr ext p refine' ⟨_, _⟩ <;> rintro ⟨⟨a, ha⟩, b⟩ · refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩ diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index aca1cb409f28c..12240d14ff0df 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -119,7 +119,7 @@ theorem cyclotomic_pos_and_nonneg (n : ℕ) {R} [LinearOrderedCommRing R] (x : R simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one, eval_add, eval_sub, sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self, and_self_iff] - · constructor <;> intro <;> set_option tactic.skipAssignedInstances false in norm_num; linarith + · constructor <;> intro <;> linarith · have : 2 < n + 3 := by linarith constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos this #align polynomial.cyclotomic_pos_and_nonneg Polynomial.cyclotomic_pos_and_nonneg diff --git a/Mathlib/RingTheory/RingHom/Finite.lean b/Mathlib/RingTheory/RingHom/Finite.lean index 7674fa7fc3d79..aa2f5bb355494 100644 --- a/Mathlib/RingTheory/RingHom/Finite.lean +++ b/Mathlib/RingTheory/RingHom/Finite.lean @@ -36,9 +36,9 @@ theorem finite_stableUnderBaseChange : StableUnderBaseChange @Finite := by classical introv h replace h : Module.Finite R T := by - rw [RingHom.Finite] at h; convert h; ext; intros; simp_rw [Algebra.smul_def]; rfl + rw [RingHom.Finite] at h; convert h; ext; simp_rw [Algebra.smul_def]; rfl suffices Module.Finite S (S ⊗[R] T) by - rw [RingHom.Finite]; convert this; congr; ext; intros; simp_rw [Algebra.smul_def]; rfl + rw [RingHom.Finite]; convert this; congr; ext; simp_rw [Algebra.smul_def]; rfl exact inferInstance #align ring_hom.finite_stable_under_base_change RingHom.finite_stableUnderBaseChange diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index 722e801d3a85d..d5a2d2bf7155d 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -1975,8 +1975,8 @@ noncomputable def UniqueFactorizationMonoid.toNormalizedGCDMonoid (α : Type*) gcd_mul_lcm := fun a b => by rw [← out_mul, mul_comm, sup_mul_inf, mk_mul_mk, out_mk] exact normalize_associated (a * b) - normalize_gcd := fun a b => by congr; apply normalize_out _ - normalize_lcm := fun a b => by congr; apply normalize_out _ } + normalize_gcd := fun a b => by apply normalize_out _ + normalize_lcm := fun a b => by apply normalize_out _ } #align unique_factorization_monoid.to_normalized_gcd_monoid UniqueFactorizationMonoid.toNormalizedGCDMonoid instance (α) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : diff --git a/Mathlib/Topology/Category/Stonean/Limits.lean b/Mathlib/Topology/Category/Stonean/Limits.lean index ee2bf55573f9e..33c241876c93d 100644 --- a/Mathlib/Topology/Category/Stonean/Limits.lean +++ b/Mathlib/Topology/Category/Stonean/Limits.lean @@ -246,7 +246,6 @@ lemma pullback.lift_fst {W : Stonean} (a : W ⟶ X) (b : W ⟶ Y) (w : a ≫ f = lemma pullback.lift_snd {X Y Z W : Stonean} (f : X ⟶ Z) {i : Y ⟶ Z} (hi : OpenEmbedding i) (a : W ⟶ X) (b : W ⟶ Y) (w : a ≫ f = b ≫ i) : pullback.lift f hi a b w ≫ Stonean.pullback.snd f hi = b := by - congr ext z have := congr_fun (DFunLike.ext'_iff.mp w.symm) z have h : i (b z) = f (a z) := this diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index 70693ff527af2..6b194bf15d8fb 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -335,7 +335,6 @@ theorem embedding_of_pullback_embeddings {X Y S : TopCat} {f : X ⟶ S} {g : Y (H₂ : Embedding g) : Embedding (limit.π (cospan f g) WalkingCospan.one) := by convert H₂.comp (snd_embedding_of_left_embedding H₁ g) erw [← coe_comp] - congr rw [← limit.w _ WalkingCospan.Hom.inr] rfl #align Top.embedding_of_pullback_embeddings TopCat.embedding_of_pullback_embeddings @@ -364,7 +363,6 @@ theorem openEmbedding_of_pullback_open_embeddings {X Y S : TopCat} {f : X ⟶ S} OpenEmbedding (limit.π (cospan f g) WalkingCospan.one) := by convert H₂.comp (snd_openEmbedding_of_left_openEmbedding H₁ g) erw [← coe_comp] - congr rw [← limit.w _ WalkingCospan.Hom.inr] rfl #align Top.open_embedding_of_pullback_open_embeddings TopCat.openEmbedding_of_pullback_open_embeddings diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorff.lean b/Mathlib/Topology/MetricSpace/GromovHausdorff.lean index 07ce0ea521c13..a283dbfe7b571 100644 --- a/Mathlib/Topology/MetricSpace/GromovHausdorff.lean +++ b/Mathlib/Topology/MetricSpace/GromovHausdorff.lean @@ -438,7 +438,6 @@ instance : MetricSpace GHSpace where hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ∘ Prod.swap '' { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y } := by - congr funext simp only [comp_apply, Prod.fst_swap, Prod.snd_swap] congr diff --git a/Mathlib/Topology/MetricSpace/Holder.lean b/Mathlib/Topology/MetricSpace/Holder.lean index 3bc0437ceafcd..3fd16d48ce67b 100644 --- a/Mathlib/Topology/MetricSpace/Holder.lean +++ b/Mathlib/Topology/MetricSpace/Holder.lean @@ -236,7 +236,6 @@ namespace HolderWith theorem nndist_le_of_le (hf : HolderWith C r f) {x y : X} {d : ℝ≥0} (hd : nndist x y ≤ d) : nndist (f x) (f y) ≤ C * d ^ (r : ℝ) := by - norm_cast rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul, ← ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg] apply hf.edist_le_of_le