From 25674d94ea8b2471152de2a0bb75372a5e151840 Mon Sep 17 00:00:00 2001 From: euprunin Date: Sat, 15 Nov 2025 23:33:59 +0100 Subject: [PATCH] chore: remove some uses of `erw` introduced in relation to lean4 PR #2644 --- Mathlib/Algebra/Category/ModuleCat/Kernels.lean | 6 +----- Mathlib/Algebra/Lie/Classical.lean | 3 +-- Mathlib/Data/Matrix/Reflection.lean | 3 +-- Mathlib/GroupTheory/HNNExtension.lean | 3 +-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean | 3 +-- Mathlib/LinearAlgebra/FreeModule/Norm.lean | 5 +---- Mathlib/ModelTheory/DirectLimit.lean | 4 +--- 7 files changed, 7 insertions(+), 20 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean index 4735438d07853e..7b72b9215209aa 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Kernels.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Kernels.lean @@ -33,11 +33,7 @@ def kernelIsLimit : IsLimit (kernelCone f) := (fun s => ofHom <| -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker LinearMap.codRestrict (LinearMap.ker f.hom) (Fork.ι s).hom fun c => - LinearMap.mem_ker.2 <| by - -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 - erw [← ConcreteCategory.comp_apply] - rw [Fork.condition, HasZeroMorphisms.comp_zero (Fork.ι s) N] - rfl) + LinearMap.mem_ker.2 <| by simp [← ConcreteCategory.comp_apply]) (fun _ => hom_ext <| LinearMap.subtype_comp_codRestrict _ _ _) fun s m h => hom_ext <| LinearMap.ext fun x => Subtype.ext_iff.2 (by simp [← h]; rfl) diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index 571493849a3c04..5aa1ebe6fbd34c 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -233,8 +233,7 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) : (soIndefiniteEquiv p q R hi A : Matrix (p ⊕ q) (p ⊕ q) R) = (Pso p q R i)⁻¹ * (A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i := by rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply] - -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 - erw [skewAdjointMatricesLieSubalgebraEquiv_apply] + grind [skewAdjointMatricesLieSubalgebraEquiv_apply] /-- A matrix defining a canonical even-rank symmetric bilinear form. diff --git a/Mathlib/Data/Matrix/Reflection.lean b/Mathlib/Data/Matrix/Reflection.lean index 9adfb4a328927b..c7ec92ae7e4ae8 100644 --- a/Mathlib/Data/Matrix/Reflection.lean +++ b/Mathlib/Data/Matrix/Reflection.lean @@ -213,8 +213,7 @@ example (A : Matrix (Fin 2) (Fin 2) α) : -/ theorem etaExpand_eq {m n} (A : Matrix (Fin m) (Fin n) α) : etaExpand A = A := by simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of] - -- This to be in the above `simp_rw` before https://github.com/leanprover/lean4/pull/2644 - erw [Equiv.refl_apply] + grind example (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] := (etaExpand_eq _).symm diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index 98062429f493a6..941d5f33ac4c83 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -526,8 +526,7 @@ theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) : -- simp [equiv_symm_eq_conj, mul_assoc]. simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, Units.val_neg, Units.val_one, Int.reduceNeg, zpow_neg, zpow_one, inv_inv] - erw [equiv_symm_eq_conj] - simp [mul_assoc] + grind [equiv_symm_eq_conj, mul_assoc] · simp only [unitsSMulGroup, SetLike.coe_sort_coe, prod_cons, prod_group_smul, map_mul, map_inv] rcases Int.units_eq_one_or u with (rfl | rfl) · -- Before https://github.com/leanprover/lean4/pull/2644, this proof was just diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index dbdd403907e067..ba4fb8eab5c59b 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -402,8 +402,7 @@ theorem AffineEquiv.affineIndependent_iff {p : ι → P} (e : P ≃ᵃ[k] P₂) theorem AffineEquiv.affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) : AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P) := by have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl - -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 - erw [← e.affineIndependent_iff, this, affineIndependent_equiv] + simp [← e.affineIndependent_iff, this, affineIndependent_equiv] end Composition diff --git a/Mathlib/LinearAlgebra/FreeModule/Norm.lean b/Mathlib/LinearAlgebra/FreeModule/Norm.lean index df9daf7916b34d..866a5035ded9d6 100644 --- a/Mathlib/LinearAlgebra/FreeModule/Norm.lean +++ b/Mathlib/LinearAlgebra/FreeModule/Norm.lean @@ -42,10 +42,7 @@ theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf : zero_smul, Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply] change _ = f * _ rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply] - -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 - erw [LinearEquiv.coord_apply_smul] - rw [Ideal.selfBasis_def] - rfl + grind [LinearEquiv.coord_apply_smul, Ideal.selfBasis_def] end CommRing diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index ed244f4eb795a1..960a3cdbd11d26 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -58,9 +58,7 @@ theorem coe_natLERec (m n : ℕ) (h : m ≤ n) : obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h ext x induction k with - | zero => - -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 - erw [natLERec, Nat.leRecOn_self, Embedding.refl_apply, Nat.leRecOn_self] + | zero => simp [natLERec, Nat.leRecOn_self] | succ k ih => -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 erw [Nat.leRecOn_succ le_self_add, natLERec, Nat.leRecOn_succ le_self_add, ← natLERec,