From 3d6731dcdc44a17f3f57d0ef17157c073bd131a7 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 20 Jun 2023 12:35:57 +0000 Subject: [PATCH] chore: remove superfluous parentheses in calls to `ext` (#5258) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Joël Riou Co-authored-by: Riccardo Brasca Co-authored-by: Yury G. Kudryashov Co-authored-by: Scott Morrison Co-authored-by: Scott Morrison Co-authored-by: Jeremy Tan Jie Rui Co-authored-by: Pol'tta / Miyahara Kō Co-authored-by: Jason Yuen Co-authored-by: Mario Carneiro Co-authored-by: Jireh Loreaux Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Kyle Miller Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Jujian Zhang Co-authored-by: Yaël Dillies --- Archive/Wiedijk100Theorems/Partition.lean | 2 +- .../Category/ModuleCat/Adjunctions.lean | 4 +-- .../Algebra/Category/Ring/Constructions.lean | 5 ++- Mathlib/Algebra/DirectSum/Algebra.lean | 4 +-- Mathlib/Algebra/DirectSum/Ring.lean | 2 +- Mathlib/Algebra/GCDMonoid/Basic.lean | 4 +-- Mathlib/Algebra/Group/Ext.lean | 6 ++-- Mathlib/Algebra/Homology/Homotopy.lean | 6 ++-- Mathlib/Algebra/Lie/Classical.lean | 3 +- Mathlib/Algebra/Lie/DirectSum.lean | 4 +-- Mathlib/Algebra/Lie/OfAssociative.lean | 4 +-- Mathlib/Algebra/Lie/TensorProduct.lean | 6 ++-- Mathlib/Algebra/Lie/Weights.lean | 4 +-- Mathlib/Algebra/Module/GradedModule.lean | 2 +- Mathlib/Algebra/MonoidAlgebra/Basic.lean | 4 +-- .../Algebra/Polynomial/GroupRingAction.lean | 2 +- .../AlgebraicTopology/DoldKan/Homotopies.lean | 2 +- Mathlib/Analysis/Analytic/Composition.lean | 4 +-- Mathlib/Analysis/Calculus/ContDiff.lean | 4 +-- Mathlib/Analysis/Calculus/ContDiffDef.lean | 4 +-- Mathlib/Analysis/Complex/Isometry.lean | 2 +- Mathlib/Analysis/InnerProductSpace/PiL2.lean | 2 +- .../Analysis/InnerProductSpace/TwoDim.lean | 2 +- Mathlib/Analysis/NormedSpace/Multilinear.lean | 6 ++-- Mathlib/Analysis/Seminorm.lean | 2 +- .../Preadditive/HomOrthogonal.lean | 6 ++-- Mathlib/CategoryTheory/Sites/Closed.lean | 2 +- .../CategoryTheory/Sites/DenseSubsite.lean | 4 +-- .../CategoryTheory/Sites/SheafOfTypes.lean | 2 +- Mathlib/CategoryTheory/Sites/Subsheaf.lean | 8 ++--- .../Combinatorics/SimpleGraph/AdjMatrix.lean | 4 +-- Mathlib/Combinatorics/SimpleGraph/Basic.lean | 16 +++++----- Mathlib/Combinatorics/SimpleGraph/Hasse.lean | 2 +- .../Combinatorics/SimpleGraph/IncMatrix.lean | 2 +- Mathlib/Control/Functor/Multivariate.lean | 10 +++--- Mathlib/Control/LawfulFix.lean | 2 +- Mathlib/Data/Complex/Module.lean | 2 +- Mathlib/Data/Dfinsupp/Basic.lean | 13 ++++---- Mathlib/Data/Dfinsupp/Interval.lean | 2 +- Mathlib/Data/FinEnum.lean | 4 +-- Mathlib/Data/Finset/Pi.lean | 2 +- Mathlib/Data/Finsupp/Indicator.lean | 2 +- Mathlib/Data/Finsupp/ToDfinsupp.lean | 2 +- Mathlib/Data/Holor.lean | 2 +- Mathlib/Data/Matrix/Basic.lean | 2 +- Mathlib/Data/Matrix/Basis.lean | 4 +-- Mathlib/Data/Matrix/Block.lean | 32 +++++++++---------- Mathlib/Data/Matrix/Kronecker.lean | 14 ++++---- Mathlib/Data/Matrix/Notation.lean | 24 +++++++------- Mathlib/Data/Matrix/PEquiv.lean | 4 +-- Mathlib/Data/Multiset/Pi.lean | 2 +- Mathlib/Data/MvPolynomial/Equiv.lean | 2 +- Mathlib/Data/Nat/Bits.lean | 2 +- Mathlib/Data/Nat/Hyperoperation.lean | 6 ++-- Mathlib/Data/Nat/Interval.lean | 2 +- Mathlib/Data/Nat/Upto.lean | 2 +- Mathlib/Data/PEquiv.lean | 2 +- Mathlib/Data/PFunctor/Multivariate/W.lean | 4 +-- Mathlib/Data/Polynomial/HasseDeriv.lean | 4 +-- .../QPF/Multivariate/Constructions/Fix.lean | 2 +- Mathlib/Data/Rel.lean | 6 ++-- Mathlib/Data/TypeVec.lean | 14 ++++---- Mathlib/GroupTheory/DoubleCoset.lean | 4 +-- .../GroupTheory/FreeAbelianGroupFinsupp.lean | 2 +- Mathlib/GroupTheory/FreeProduct.lean | 2 +- Mathlib/GroupTheory/Perm/Basic.lean | 2 +- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean | 4 +-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean | 2 +- Mathlib/LinearAlgebra/Basic.lean | 2 +- Mathlib/LinearAlgebra/BilinearMap.lean | 2 +- Mathlib/LinearAlgebra/Contraction.lean | 16 +++++----- Mathlib/LinearAlgebra/Determinant.lean | 4 +-- .../DirectSum/TensorProduct.lean | 4 +-- Mathlib/LinearAlgebra/Dual.lean | 6 ++-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean | 2 +- Mathlib/LinearAlgebra/Finsupp.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Adjugate.lean | 16 +++++----- Mathlib/LinearAlgebra/Matrix/Basis.lean | 18 +++++------ .../LinearAlgebra/Matrix/BilinearForm.lean | 6 ++-- Mathlib/LinearAlgebra/Matrix/Block.lean | 4 +-- .../LinearAlgebra/Matrix/Charpoly/Basic.lean | 4 +-- Mathlib/LinearAlgebra/Matrix/Circulant.lean | 8 ++--- Mathlib/LinearAlgebra/Matrix/Determinant.lean | 10 +++--- Mathlib/LinearAlgebra/Matrix/Dual.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Hermitian.lean | 4 +-- Mathlib/LinearAlgebra/Matrix/IsDiag.lean | 2 +- Mathlib/LinearAlgebra/Matrix/LDL.lean | 4 +-- .../Matrix/SesquilinearForm.lean | 6 ++-- .../Matrix/SpecialLinearGroup.lean | 2 +- Mathlib/LinearAlgebra/Matrix/Spectrum.lean | 4 +-- Mathlib/LinearAlgebra/Matrix/ToLin.lean | 18 +++++------ .../LinearAlgebra/Matrix/Transvection.lean | 12 +++---- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 4 +-- Mathlib/LinearAlgebra/Pi.lean | 4 +-- .../LinearAlgebra/QuadraticForm/Basic.lean | 2 +- Mathlib/LinearAlgebra/SesquilinearForm.lean | 4 +-- Mathlib/LinearAlgebra/StdBasis.lean | 4 +-- Mathlib/LinearAlgebra/TensorPower.lean | 2 +- Mathlib/LinearAlgebra/TensorProduct.lean | 8 ++--- .../LinearAlgebra/TensorProduct/Matrix.lean | 6 ++-- Mathlib/LinearAlgebra/Trace.lean | 6 ++-- Mathlib/LinearAlgebra/Vandermonde.lean | 4 +-- .../MeasureTheory/Measure/Lebesgue/Basic.lean | 2 +- Mathlib/Order/Hom/Basic.lean | 6 ++-- Mathlib/Order/Lattice.lean | 4 +-- Mathlib/Order/LocallyFinite.lean | 8 ++--- Mathlib/Order/RelIso/Basic.lean | 2 +- Mathlib/Probability/Kernel/WithDensity.lean | 2 +- Mathlib/RepresentationTheory/Basic.lean | 5 ++- Mathlib/RingTheory/GradedAlgebra/Basic.lean | 2 +- Mathlib/RingTheory/IsTensorProduct.lean | 2 +- Mathlib/RingTheory/PolynomialAlgebra.lean | 2 +- Mathlib/RingTheory/TensorProduct.lean | 2 +- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 2 +- Mathlib/Topology/MetricSpace/Basic.lean | 2 +- Mathlib/Topology/PathConnected.lean | 2 +- 116 files changed, 282 insertions(+), 284 deletions(-) diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean index 19a347906cf3e..84eed05fac285 100644 --- a/Archive/Wiedijk100Theorems/Partition.lean +++ b/Archive/Wiedijk100Theorems/Partition.lean @@ -104,7 +104,7 @@ def cut {ι : Type _} (s : Finset ι) (n : ℕ) : Finset (ι → ℕ) := Finset.filter (fun f => s.sum f = n) ((s.pi fun _ => range (n + 1)).map ⟨fun f i => if h : i ∈ s then f i h else 0, fun f g h => by - ext (i hi); simpa [dif_pos hi] using congr_fun h i⟩) + ext i hi; simpa [dif_pos hi] using congr_fun h i⟩) #align theorems_100.cut Theorems100.cut theorem mem_cut {ι : Type _} (s : Finset ι) (n : ℕ) (f : ι → ℕ) : diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index 86ae14b174f77..b04096dfad69c 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -291,7 +291,7 @@ instance : Preadditive (Free R C) where comp_add X Y Z f g g' := by dsimp [CategoryTheory.categoryFree] rw [← Finsupp.sum_add] - congr ; ext (r h) + congr; ext r h rw [Finsupp.sum_add_index'] <;> · simp [mul_add] instance : Linear R (Free R C) where @@ -302,7 +302,7 @@ instance : Linear R (Free R C) where comp_smul X Y Z f r g := by dsimp [CategoryTheory.categoryFree] simp_rw [Finsupp.smul_sum] - congr ; ext (h s) + congr; ext h s rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_left_comm] theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) : diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean index 84bf7d558e298..5cb2fa1cca9a3 100644 --- a/Mathlib/Algebra/Category/Ring/Constructions.lean +++ b/Mathlib/Algebra/Category/Ring/Constructions.lean @@ -159,7 +159,7 @@ instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRin apply hasStrictTerminalObjects_of_terminal_is_strict (CommRingCat.of PUnit) intro X f refine ⟨⟨⟨1, rfl, fun _ _ => rfl⟩, by ext; rfl, ?_⟩⟩ - ext (x : X) + ext x have e : (0 : X) = 1 := by rw [← f.map_one, ← f.map_zero] congr @@ -204,8 +204,7 @@ def prodFanIsLimit : IsLimit (prodFan A B) where FunctorToTypes.map_comp_apply, forget_map, coe_of, RingHom.prod_apply] <;> rfl uniq s m h := by - dsimp - ext (x : s.pt) + ext x change m x = (BinaryFan.fst s x, BinaryFan.snd s x) have eq1 := congr_hom (h ⟨WalkingPair.left⟩) x have eq2 := congr_hom (h ⟨WalkingPair.right⟩) x diff --git a/Mathlib/Algebra/DirectSum/Algebra.lean b/Mathlib/Algebra/DirectSum/Algebra.lean index 7289f6ebf635c..dd0589ad7904e 100644 --- a/Mathlib/Algebra/DirectSum/Algebra.lean +++ b/Mathlib/Algebra/DirectSum/Algebra.lean @@ -73,14 +73,14 @@ instance : Algebra R (⨁ i, A i) where commutes' r x := by change AddMonoidHom.mul (DirectSum.of _ _ _) x = AddMonoidHom.mul.flip (DirectSum.of _ _ _) x apply FunLike.congr_fun _ x - ext (i xi) : 2 + ext i xi : 2 dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply] rw [of_mul_of, of_mul_of] apply Dfinsupp.single_eq_of_sigma_eq (GAlgebra.commutes r ⟨i, xi⟩) smul_def' r x := by change DistribMulAction.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x apply FunLike.congr_fun _ x - ext (i xi) : 2 + ext i xi : 2 dsimp only [AddMonoidHom.comp_apply, DistribMulAction.toAddMonoidHom_apply, AddMonoidHom.mul_apply] rw [DirectSum.of_mul_of, ← of_smul] diff --git a/Mathlib/Algebra/DirectSum/Ring.lean b/Mathlib/Algebra/DirectSum/Ring.lean index 64ceeadca8d67..798c5d1489ba0 100644 --- a/Mathlib/Algebra/DirectSum/Ring.lean +++ b/Mathlib/Algebra/DirectSum/Ring.lean @@ -658,7 +658,7 @@ def liftRingHom : simp [AddMonoidHom.comp_apply] rw [← F.map_mul (of A i ai), of_mul_of ai]⟩ left_inv f := by - ext (xi xv) + ext xi xv exact toAddMonoid_of (fun _ => f.1) xi xv right_inv F := by apply RingHom.coe_addMonoidHom_injective diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 3bace628c9c34..b99b1ef465818 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/Mathlib/Algebra/GCDMonoid/Basic.lean @@ -920,13 +920,13 @@ instance uniqueNormalizationMonoidOfUniqueUnits : Unique (NormalizationMonoid α instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) := ⟨fun g₁ g₂ => by have hgcd : g₁.gcd = g₂.gcd := by - ext (a b) + ext a b refine' associated_iff_eq.mp (associated_of_dvd_dvd _ _) -- Porting note: Lean4 seems to need help specifying `g₁` and `g₂` · exact dvd_gcd (@gcd_dvd_left _ _ g₁ _ _) (@gcd_dvd_right _ _ g₁ _ _) · exact @dvd_gcd _ _ g₁ _ _ _ (@gcd_dvd_left _ _ g₂ _ _) (@gcd_dvd_right _ _ g₂ _ _) have hlcm : g₁.lcm = g₂.lcm := by - ext (a b) + ext a b -- Porting note: Lean4 seems to need help specifying `g₁` and `g₂` refine' associated_iff_eq.mp (associated_of_dvd_dvd _ _) · exact (@lcm_dvd_iff _ _ g₁ ..).mpr ⟨@dvd_lcm_left _ _ g₂ _ _, @dvd_lcm_right _ _ g₂ _ _⟩ diff --git a/Mathlib/Algebra/Group/Ext.lean b/Mathlib/Algebra/Group/Ext.lean index b26153b5a3565..c140d3e5f3e7e 100644 --- a/Mathlib/Algebra/Group/Ext.lean +++ b/Mathlib/Algebra/Group/Ext.lean @@ -36,7 +36,7 @@ theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄ (h_mul : m₁.mul = m @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁) (fun x y => congr_fun (congr_fun h_mul x) y) have : m₁.npow = m₂.npow := by - ext (n x) + ext n x exact @MonoidHom.map_pow M M m₁ m₂ f x n rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩ rcases m₂ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩ @@ -130,10 +130,10 @@ theorem DivInvMonoid.ext {M : Type _} ⦃m₁ m₂ : DivInvMonoid M⦄ (h_mul : (fun x y => congr_fun (congr_fun h_mul x) y) have : m₁.npow = m₂.npow := congr_arg (·.npow) h_mon have : m₁.zpow = m₂.zpow := by - ext (m x) + ext m x exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m have : m₁.div = m₂.div := by - ext (a b) + ext a b exact @map_div' _ _ (@MonoidHom _ _ (_) _) (id _) _ (@MonoidHom.monoidHomClass _ _ (_) _) f (congr_fun h_inv) a b diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index eee0a888b2aa1..cb15060031e18 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/Mathlib/Algebra/Homology/Homotopy.lean @@ -282,7 +282,7 @@ theorem nullHomotopicMap'_comp (hom : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) ext n erw [nullHomotopicMap_comp] congr - ext (i j) + ext i j split_ifs · rfl · rw [zero_comp] @@ -304,7 +304,7 @@ theorem comp_nullHomotopicMap' (f : C ⟶ D) (hom : ∀ i j, c.Rel j i → (D.X ext n erw [comp_nullHomotopicMap] congr - ext (i j) + ext i j split_ifs · rfl · rw [comp_zero] @@ -328,7 +328,7 @@ theorem map_nullHomotopicMap' {W : Type _} [Category W] [Preadditive W] (G : V ext n erw [map_nullHomotopicMap] congr - ext (i j) + ext i j split_ifs · rfl · rw [G.map_zero] diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index 740bb84813d0c..9dadbf8d32ae6 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -363,9 +363,8 @@ theorem indefiniteDiagonal_assoc : indefiniteDiagonal (Sum Unit l) l R = Matrix.reindexLieEquiv (Equiv.sumAssoc Unit l l).symm (Matrix.fromBlocks 1 0 0 (indefiniteDiagonal l l R)) := by - ext (i j) + ext ⟨⟨i₁ | i₂⟩ | i₃⟩ ⟨⟨j₁ | j₂⟩ | j₃⟩ <;> -- Porting note: added `Sum.inl_injective.eq_iff`, `Sum.inr_injective.eq_iff` - rcases i with ⟨⟨i₁ | i₂⟩ | i₃⟩ <;> rcases j with ⟨⟨j₁ | j₂⟩ | j₃⟩ <;> simp only [indefiniteDiagonal, Matrix.diagonal_apply, Equiv.sumAssoc_apply_inl_inl, Matrix.reindexLieEquiv_apply, Matrix.submatrix_apply, Equiv.symm_symm, Matrix.reindex_apply, Sum.elim_inl, if_true, eq_self_iff_true, Matrix.one_apply_eq, Matrix.fromBlocks_apply₁₁, diff --git a/Mathlib/Algebra/Lie/DirectSum.lean b/Mathlib/Algebra/Lie/DirectSum.lean index cdb614708debe..d93030faee839 100644 --- a/Mathlib/Algebra/Lie/DirectSum.lean +++ b/Mathlib/Algebra/Lie/DirectSum.lean @@ -207,7 +207,7 @@ def toLieAlgebra [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L' ⁅toModule R ι L' f' x, toModule R ι L' f' (of L i y)⁆ by simp only [← LieAlgebra.ad_apply R] rw [← LinearMap.comp_apply, ← LinearMap.comp_apply] - congr; clear y; ext (i y); exact this i y + congr; clear y; ext i y; exact this i y -- Similarly, we can reduce to the case that `x` has only one non-zero component. suffices ∀ (i j) (y : L i) (x : L j), toModule R ι L' f' ⁅of L j x, of L i y⁆ = @@ -216,7 +216,7 @@ def toLieAlgebra [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L' rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)] simp only [LinearMap.map_neg, neg_inj, ← LieAlgebra.ad_apply R] rw [← LinearMap.comp_apply, ← LinearMap.comp_apply] - congr; clear x; ext (j x); exact this j i x y + congr; clear x; ext j x; exact this j i x y -- Tidy up and use `lie_of`. intro i j y x simp only [lie_of R, lieAlgebraOf_apply, LieHom.coe_toLinearMap, toAddMonoid_of, diff --git a/Mathlib/Algebra/Lie/OfAssociative.lean b/Mathlib/Algebra/Lie/OfAssociative.lean index 3890f9d556810..3cba92257a1db 100644 --- a/Mathlib/Algebra/Lie/OfAssociative.lean +++ b/Mathlib/Algebra/Lie/OfAssociative.lean @@ -241,7 +241,7 @@ theorem LieAlgebra.ad_apply (x y : L) : LieAlgebra.ad R L x y = ⁅x, y⁆ := @[simp] theorem LieModule.toEndomorphism_module_end : - LieModule.toEndomorphism R (Module.End R M) M = LieHom.id := by ext (g m); simp [lie_eq_smul] + LieModule.toEndomorphism R (Module.End R M) M = LieHom.id := by ext g m; simp [lie_eq_smul] #align lie_module.to_endomorphism_module_End LieModule.toEndomorphism_module_end theorem LieSubalgebra.toEndomorphism_eq (K : LieSubalgebra R L) {x : K} : @@ -288,7 +288,7 @@ open LieAlgebra theorem LieAlgebra.ad_eq_lmul_left_sub_lmul_right (A : Type v) [Ring A] [Algebra R A] : (ad R A : A → Module.End R A) = LinearMap.mulLeft R - LinearMap.mulRight R := by - ext (a b); simp [LieRing.of_associative_ring_bracket] + ext a b; simp [LieRing.of_associative_ring_bracket] #align lie_algebra.ad_eq_lmul_left_sub_lmul_right LieAlgebra.ad_eq_lmul_left_sub_lmul_right theorem LieSubalgebra.ad_comp_incl_eq (K : LieSubalgebra R L) (x : K) : diff --git a/Mathlib/Algebra/Lie/TensorProduct.lean b/Mathlib/Algebra/Lie/TensorProduct.lean index d7b3a5d9bddd0..d5e9034676244 100644 --- a/Mathlib/Algebra/Lie/TensorProduct.lean +++ b/Mathlib/Algebra/Lie/TensorProduct.lean @@ -66,7 +66,7 @@ instance lieRingModule : LieRingModule L (M ⊗[R] N) where suffices (hasBracketAux x).comp (hasBracketAux y) = hasBracketAux ⁅x, y⁆ + (hasBracketAux y).comp (hasBracketAux x) by simp only [← LinearMap.add_apply]; rw [← LinearMap.comp_apply, this]; rfl - ext (m n) + ext m n simp only [hasBracketAux, LieRing.of_associative_ring_bracket, LinearMap.mul_apply, mk_apply, LinearMap.lTensor_sub, LinearMap.compr₂_apply, Function.comp_apply, LinearMap.coe_comp, LinearMap.rTensor_tmul, LieHom.map_lie, toEndomorphism_apply_apply, LinearMap.add_apply, @@ -97,7 +97,7 @@ tensor-hom adjunction is equivariant with respect to the `L` action. -/ def lift : (M →ₗ[R] N →ₗ[R] P) ≃ₗ⁅R,L⁆ M ⊗[R] N →ₗ[R] P := { TensorProduct.lift.equiv R M N P with map_lie' := fun {x f} => by - ext (m n) + ext m n simp only [mk_apply, LinearMap.compr₂_apply, lie_tmul_right, LinearMap.sub_apply, lift.equiv_apply, LinearEquiv.toFun_eq_coe, LieHom.lie_apply, LinearMap.map_add] abel } @@ -122,7 +122,7 @@ theorem coe_liftLie_eq_lift_coe (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) : ⇑(liftLie R L M N P f) = lift R L M N P f := by suffices (liftLie R L M N P f : M ⊗[R] N →ₗ[R] P) = lift R L M N P f by rw [← this, LieModuleHom.coe_toLinearMap] - ext (m n) + ext m n simp only [liftLie, LinearEquiv.trans_apply, LieModuleEquiv.coe_to_linearEquiv, coe_linearMap_maxTrivLinearMapEquivLieModuleHom, coe_maxTrivEquiv_apply, coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm] diff --git a/Mathlib/Algebra/Lie/Weights.lean b/Mathlib/Algebra/Lie/Weights.lean index e368d7b081673..7d31c2c71649f 100644 --- a/Mathlib/Algebra/Lie/Weights.lean +++ b/Mathlib/Algebra/Lie/Weights.lean @@ -128,7 +128,7 @@ protected theorem weight_vector_multiplication (M₁ : Type w₁) (M₂ : Type w let f₁ : Module.End R (M₁ ⊗[R] M₂) := (toEndomorphism R L M₁ x - χ₁ x • ↑1).rTensor M₂ let f₂ : Module.End R (M₁ ⊗[R] M₂) := (toEndomorphism R L M₂ x - χ₂ x • ↑1).lTensor M₁ have h_comm_square : F ∘ₗ ↑g = (g : M₁ ⊗[R] M₂ →ₗ[R] M₃).comp (f₁ + f₂) := by - ext (m₁ m₂); + ext m₁ m₂; simp only [← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul, lie_tmul_right, tmul_smul, toEndomorphism_apply_apply, LieModuleHom.map_smul, LinearMap.one_apply, LieModuleHom.coe_toLinearMap, LinearMap.smul_apply, Function.comp_apply, LinearMap.coe_comp, @@ -152,7 +152,7 @@ protected theorem weight_vector_multiplication (M₁ : Type w₁) (M₂ : Type w -- It's now just an application of the binomial theorem. use k₁ + k₂ - 1 have hf_comm : Commute f₁ f₂ := by - ext (m₁ m₂) + ext m₁ m₂ simp only [LinearMap.mul_apply, LinearMap.rTensor_tmul, LinearMap.lTensor_tmul, AlgebraTensorModule.curry_apply, LinearMap.toFun_eq_coe, LinearMap.lTensor_tmul, curry_apply, LinearMap.coe_restrictScalars] diff --git a/Mathlib/Algebra/Module/GradedModule.lean b/Mathlib/Algebra/Module/GradedModule.lean index 63e3fc3bc9cc9..017cfae5a5646 100644 --- a/Mathlib/Algebra/Module/GradedModule.lean +++ b/Mathlib/Algebra/Module/GradedModule.lean @@ -134,7 +134,7 @@ private theorem mul_smul' [DecidableEq ι] [GSemiring A] [Gmodule A M] (a b : (smulAddMonoidHom A M).flip.compHom.comp <| smulAddMonoidHom A M).flip from-- `fun a b c ↦ a • (b • c)` as a bundled hom FunLike.congr_fun (FunLike.congr_fun (FunLike.congr_fun this a) b) c - ext (ai ax bi bx ci cx) : 6 + ext ai ax bi bx ci cx : 6 dsimp only [coe_comp, Function.comp_apply, compHom_apply_apply, flip_apply, flipHom_apply] rw [smulAddMonoidHom_apply_of_of, smulAddMonoidHom_apply_of_of, DirectSum.mulHom_of_of, smulAddMonoidHom_apply_of_of] diff --git a/Mathlib/Algebra/MonoidAlgebra/Basic.lean b/Mathlib/Algebra/MonoidAlgebra/Basic.lean index bb91a81574685..c2984d72f27cc 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Basic.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Basic.lean @@ -486,7 +486,7 @@ theorem mapDomain_mul {α : Type _} {β : Type _} {α₂ : Type _} [Semiring β] simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_mul] rw [Finsupp.sum_mapDomain_index] · congr - ext (a b) + ext a b rw [Finsupp.sum_mapDomain_index] · simp · simp [mul_add] @@ -1557,7 +1557,7 @@ theorem mapDomain_mul {α : Type _} {β : Type _} {α₂ : Type _} [Semiring β] simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_add] rw [Finsupp.sum_mapDomain_index] · congr - ext (a b) + ext a b rw [Finsupp.sum_mapDomain_index] · simp · simp [mul_add] diff --git a/Mathlib/Algebra/Polynomial/GroupRingAction.lean b/Mathlib/Algebra/Polynomial/GroupRingAction.lean index c212622f10ac2..ae2be28f31c36 100644 --- a/Mathlib/Algebra/Polynomial/GroupRingAction.lean +++ b/Mathlib/Algebra/Polynomial/GroupRingAction.lean @@ -38,7 +38,7 @@ theorem smul_eq_map [MulSemiringAction M R] (m : M) : (mapRingHom (MulSemiringAction.toRingHom M R m)).toAddMonoidHom by ext1 r exact FunLike.congr_fun this r - ext (n r) : 2 + ext n r : 2 change m • monomial n r = map (MulSemiringAction.toRingHom M R m) (monomial n r) rw [Polynomial.map_monomial, Polynomial.smul_monomial, MulSemiringAction.toRingHom_apply] #align polynomial.smul_eq_map Polynomial.smul_eq_map diff --git a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean index 84382442437a0..77799db7b60ba 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean @@ -178,7 +178,7 @@ def natTransHσ (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapCo unfold Hσ rw [nullHomotopicMap'_comp, comp_nullHomotopicMap'] congr - ext (n m hnm) + ext n m hnm simp only [alternatingFaceMapComplex_map_f, hσ'_naturality] set_option linter.uppercaseLean3 false in #align algebraic_topology.dold_kan.nat_trans_Hσ AlgebraicTopology.DoldKan.natTransHσ diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index 05515df552dee..22e6899fa551a 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/Mathlib/Analysis/Analytic/Composition.lean @@ -137,7 +137,7 @@ theorem applyComposition_single (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} @[simp] theorem removeZero_applyComposition (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (c : Composition n) : p.removeZero.applyComposition c = p.applyComposition c := by - ext (v i) + ext v i simp [applyComposition, zero_lt_one.trans_le (c.one_le_blocksFun i), removeZero_of_pos] #align formal_multilinear_series.remove_zero_apply_composition FormalMultilinearSeries.removeZero_applyComposition @@ -1193,7 +1193,7 @@ open Composition set_option maxHeartbeats 500000 in theorem comp_assoc (r : FormalMultilinearSeries 𝕜 G H) (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) : (r.comp q).comp p = r.comp (q.comp p) := by - ext (n v) + ext n v /- First, rewrite the two compositions appearing in the theorem as two sums over complicated sigma types, as in the description of the proof above. -/ let f : (Σ a : Composition n, Composition a.length) → H := fun c => diff --git a/Mathlib/Analysis/Calculus/ContDiff.lean b/Mathlib/Analysis/Calculus/ContDiff.lean index 7c4224d9a2020..2461fad15b4d6 100644 --- a/Mathlib/Analysis/Calculus/ContDiff.lean +++ b/Mathlib/Analysis/Calculus/ContDiff.lean @@ -71,7 +71,7 @@ variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAdd theorem iteratedFDeriv_zero_fun {n : ℕ} : (iteratedFDeriv 𝕜 n fun _ : E => (0 : F)) = 0 := by induction' n with n IH · ext m; simp - · ext (x m) + · ext x m rw [iteratedFDeriv_succ_apply_left, IH] change (fderiv 𝕜 (fun _ : E => (0 : E[×n]→L[𝕜] F)) x : E → E[×n]→L[𝕜] F) (m 0) (tail m) = _ rw [fderiv_const] @@ -369,7 +369,7 @@ theorem HasFTaylorSeriesUpToOn.compContinuousLinearMap (hf : HasFTaylorSeriesUpT · intro m hm x hx convert (hA m).hasFDerivAt.comp_hasFDerivWithinAt x ((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _)) - ext (y v) + ext y v change p (g x) (Nat.succ m) (g ∘ cons y v) = p (g x) m.succ (cons (g y) (g ∘ v)) rw [comp_cons] · intro m hm diff --git a/Mathlib/Analysis/Calculus/ContDiffDef.lean b/Mathlib/Analysis/Calculus/ContDiffDef.lean index 9079340344fad..ac1186f8564ee 100644 --- a/Mathlib/Analysis/Calculus/ContDiffDef.lean +++ b/Mathlib/Analysis/Calculus/ContDiffDef.lean @@ -386,7 +386,7 @@ theorem hasFTaylorSeriesUpToOn_succ_iff_right {n : ℕ} : ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'] at this convert this - ext (y v) + ext y v change (p x (Nat.succ (Nat.succ m))) (cons y v) = (p x m.succ.succ) (snoc (cons y (init v)) (v (last _))) @@ -1575,7 +1575,7 @@ theorem iteratedFDerivWithin_univ {n : ℕ} : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f := by induction' n with n IH · ext x; simp - · ext (x m) + · ext x m rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ] #align iterated_fderiv_within_univ iteratedFDerivWithin_univ diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean index 9e1d33bfddefa..f0829e54d79cc 100644 --- a/Mathlib/Analysis/Complex/Isometry.lean +++ b/Mathlib/Analysis/Complex/Isometry.lean @@ -157,7 +157,7 @@ theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) : theorem toMatrix_rotation (a : circle) : LinearMap.toMatrix basisOneI basisOneI (rotation a).toLinearEquiv = Matrix.planeConformalMatrix (re a) (im a) (by simp [pow_two, ← normSq_apply]) := by - ext (i j) + ext i j simp [LinearMap.toMatrix_apply] fin_cases i <;> fin_cases j <;> simp #align to_matrix_rotation toMatrix_rotation diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean index d219620354cf6..ecf1c0c5082ac 100644 --- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean +++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean @@ -694,7 +694,7 @@ variable (a b : OrthonormalBasis ι 𝕜 E) theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary : a.toBasis.toMatrix b ∈ Matrix.unitaryGroup ι 𝕜 := by rw [Matrix.mem_unitaryGroup_iff'] - ext (i j) + ext i j convert a.repr.inner_map_map (b i) (b j) rw [orthonormal_iff_ite.mp b.orthonormal i j] rfl diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean index 7bf6171d6438c..9cd0990e0ab92 100644 --- a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -126,7 +126,7 @@ theorem areaForm_swap (x y : E) : ω x y = -ω y x := by @[simp] theorem areaForm_neg_orientation : (-o).areaForm = -o.areaForm := by - ext (x y) + ext x y simp [areaForm_to_volumeForm] #align orientation.area_form_neg_orientation Orientation.areaForm_neg_orientation diff --git a/Mathlib/Analysis/NormedSpace/Multilinear.lean b/Mathlib/Analysis/NormedSpace/Multilinear.lean index 8216d620d53b7..98ce053fe84f8 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear.lean @@ -1370,7 +1370,7 @@ theorem ContinuousMultilinearMap.curryLeft_apply (f : ContinuousMultilinearMap theorem ContinuousLinearMap.curry_uncurryLeft (f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei i.succ) G) : f.uncurryLeft.curryLeft = f := by - ext (m x) + ext m x simp only [tail_cons, ContinuousLinearMap.uncurryLeft_apply, ContinuousMultilinearMap.curryLeft_apply] rw [cons_zero] @@ -1498,7 +1498,7 @@ theorem ContinuousMultilinearMap.curryRight_apply (f : ContinuousMultilinearMap theorem ContinuousMultilinearMap.curry_uncurryRight (f : ContinuousMultilinearMap 𝕜 (fun i : Fin n => Ei <| castSucc i) (Ei (last n) →L[𝕜] G)) : f.uncurryRight.curryRight = f := by - ext (m x) + ext m x simp only [snoc_last, ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply] rw [init_snoc] @@ -1829,7 +1829,7 @@ def currySumEquiv : ContinuousMultilinearMap 𝕜 (fun _ : Sum ι ι' => G) G' ext m exact congr_arg f (Sum.elim_comp_inl_inr m) right_inv := fun f => by - ext (m₁ m₂) + ext m₁ m₂ rfl } (fun f => MultilinearMap.mkContinuousMultilinear_norm_le _ (norm_nonneg f) _) fun f => by simp only [LinearEquiv.coe_symm_mk] diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index 588077c83ee5e..2c7cd0466b166 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -1203,7 +1203,7 @@ theorem coe_normSeminorm : ⇑(normSeminorm 𝕜 E) = norm := @[simp] theorem ball_normSeminorm : (normSeminorm 𝕜 E).ball = Metric.ball := by - ext (x r y) + ext x r y simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm] #align ball_norm_seminorm ball_normSeminorm diff --git a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean index 769310586933d..28b5155431b71 100644 --- a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean +++ b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean @@ -101,7 +101,7 @@ noncomputable def matrixDecomposition (o : HomOrthogonal s) {α β : Type} [Fint · symm apply o.eq_zero h right_inv z := by - ext (i ⟨j, w⟩ ⟨k, ⟨⟩⟩) + ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩ simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp] simp only [Set.mem_preimage, Set.mem_singleton_iff] split_ifs with h @@ -132,7 +132,7 @@ noncomputable def matrixDecompositionAddEquiv (o : HomOrthogonal s) {α β : Typ @[simp] theorem matrixDecomposition_id (o : HomOrthogonal s) {α : Type} [Fintype α] {f : α → ι} (i : ι) : o.matrixDecomposition (𝟙 (⨁ fun a => s (f a))) i = 1 := by - ext (⟨b, ⟨⟩⟩⟨a, j_property⟩) + ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩ simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property simp only [Category.comp_id, Category.id_comp, Category.assoc, End.one_def, eqToHom_refl, Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components] @@ -150,7 +150,7 @@ theorem matrixDecomposition_comp (o : HomOrthogonal s) {α β γ : Type} [Fintyp [Fintype γ] {f : α → ι} {g : β → ι} {h : γ → ι} (z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)) (w : (⨁ fun b => s (g b)) ⟶ ⨁ fun c => s (h c)) (i : ι) : o.matrixDecomposition (z ≫ w) i = o.matrixDecomposition w i ⬝ o.matrixDecomposition z i := by - ext (⟨c, ⟨⟩⟩⟨a, j_property⟩) + ext ⟨c, ⟨⟩⟩ ⟨a, j_property⟩ simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property simp only [Matrix.mul_apply, Limits.biproduct.components, HomOrthogonal.matrixDecomposition_apply, Category.comp_id, Category.id_comp, Category.assoc, diff --git a/Mathlib/CategoryTheory/Sites/Closed.lean b/Mathlib/CategoryTheory/Sites/Closed.lean index dcdb317a5f593..0e74bb3353b78 100644 --- a/Mathlib/CategoryTheory/Sites/Closed.lean +++ b/Mathlib/CategoryTheory/Sites/Closed.lean @@ -313,7 +313,7 @@ The topology given by the closure operator `J.close` on a Grothendieck topology -/ theorem topologyOfClosureOperator_self : (topologyOfClosureOperator J₁.closureOperator fun X Y => J₁.pullback_close) = J₁ := by - ext (X S) + ext X S apply GrothendieckTopology.close_eq_top_iff_mem #align category_theory.topology_of_closure_operator_self CategoryTheory.topologyOfClosureOperator_self diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean index b80dfde8c3732..96cba49e5a13e 100644 --- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean +++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean @@ -311,7 +311,7 @@ noncomputable def sheafCoyonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type _)).obj ℱ'.val where app X := presheafHom H (homOver α (unop X)) naturality X Y f := by - ext (U x) + ext U x change appHom H (homOver α (unop Y)) (unop U) (f.unop ≫ x) = f.unop ≫ appHom H (homOver α (unop X)) (unop U) x @@ -346,7 +346,7 @@ noncomputable def sheafYonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : { app := fun X => (α.app X).app U naturality := fun X Y f => by simpa using congr_app (α.naturality f) U } · intro U V i - ext (X x) + ext X x exact congr_fun ((α.app X).naturality i) x #align category_theory.cover_dense.sheaf_yoneda_hom CategoryTheory.CoverDense.sheafYonedaHom diff --git a/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean b/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean index 555d2bf0268b2..9e2124541a551 100644 --- a/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean +++ b/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean @@ -488,7 +488,7 @@ def natTransEquivCompatibleFamily {P : Cᵒᵖ ⥤ Type v₁} : ext ⟨f, hf⟩ apply t.2.to_sieveCompatible _ } left_inv α := by - ext (X⟨_, _⟩) + ext X ⟨_, _⟩ rfl right_inv := by rintro ⟨x, hx⟩ diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean index 2f65ebd5c2536..5792b4417100d 100644 --- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean +++ b/Mathlib/CategoryTheory/Sites/Subsheaf.lean @@ -126,7 +126,7 @@ theorem Subpresheaf.eq_top_iff_isIso : G = ⊤ ↔ IsIso G.ι := by · rintro rfl infer_instance · intro H - ext (U x) + ext U x apply iff_true_iff.mpr rw [← IsIso.inv_hom_id_apply (G.ι.app U) x] exact ((inv (G.ι.app U)) x).2 @@ -302,7 +302,7 @@ noncomputable def Subpresheaf.sheafifyLift (f : G.toPresheaf ⟶ F') (h : Presie theorem Subpresheaf.to_sheafifyLift (f : G.toPresheaf ⟶ F') (h : Presieve.IsSheaf J F') : Subpresheaf.homOfLe (G.le_sheafify J) ≫ G.sheafifyLift f h = f := by - ext (U s) + ext U s apply (h _ ((Subpresheaf.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext intro V i hi have := elementwise_of% f.naturality @@ -315,7 +315,7 @@ theorem Subpresheaf.to_sheafify_lift_unique (h : Presieve.IsSheaf J F') (l₁ l₂ : (G.sheafify J).toPresheaf ⟶ F') (e : Subpresheaf.homOfLe (G.le_sheafify J) ≫ l₁ = Subpresheaf.homOfLe (G.le_sheafify J) ≫ l₂) : l₁ = l₂ := by - ext (U⟨s, hs⟩) + ext U ⟨s, hs⟩ apply (h _ hs).isSeparatedFor.ext rintro V i hi dsimp at hi @@ -437,7 +437,7 @@ instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (imageSheafι f) := instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (toImageSheaf f) := by refine' ⟨@fun G' g₁ g₂ e => _⟩ - ext (U⟨s, hx⟩) + ext U ⟨s, hx⟩ apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext rintro V i ⟨y, e'⟩ change (g₁.val.app _ ≫ G'.val.map _) _ = (g₂.val.app _ ≫ G'.val.map _) _ diff --git a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean index e7e7ba3613796..854f0bc767870 100644 --- a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean @@ -136,7 +136,7 @@ theorem compl [Zero α] [One α] (h : IsAdjMatrix A) : IsAdjMatrix A.compl := theorem toGraph_compl_eq [MulZeroOneClass α] [Nontrivial α] (h : IsAdjMatrix A) : h.compl.toGraph = h.toGraphᶜ := by - ext (v w) + ext v w cases' h.zero_or_one v w with h h <;> by_cases hvw : v = w <;> simp [Matrix.compl, h, hvw] #align matrix.is_adj_matrix.to_graph_compl_eq Matrix.IsAdjMatrix.toGraph_compl_eq @@ -293,7 +293,7 @@ variable {A : Matrix V V α} (h : IsAdjMatrix A) /-- If `A` is qualified as an adjacency matrix, then the adjacency matrix of the graph induced by `A` is itself. -/ theorem adjMatrix_toGraph_eq [DecidableEq α] : h.toGraph.adjMatrix α = A := by - ext (i j) + ext i j obtain h' | h' := h.zero_or_one i j <;> simp [h'] #align matrix.is_adj_matrix.adj_matrix_to_graph_eq Matrix.IsAdjMatrix.adjMatrix_toGraph_eq diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index e7efe4fda009c..b36c33ec2a438 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -355,7 +355,7 @@ instance completeBooleanAlgebra : CompleteBooleanAlgebra (SimpleGraph V) := le_top := fun x v w h => x.ne_of_adj h bot_le := fun x v w h => h.elim sdiff_eq := fun x y => by - ext (v w) + ext v w refine' ⟨fun h => ⟨h.1, ⟨_, h.2⟩⟩, fun h => ⟨h.1, h.2.2⟩⟩ rintro rfl exact x.irrefl h.1 @@ -629,26 +629,26 @@ theorem edgeSet_fromEdgeSet : (fromEdgeSet s).edgeSet = s \ { e | e.IsDiag } := @[simp] theorem fromEdgeSet_edgeSet : fromEdgeSet G.edgeSet = G := by - ext (v w) + ext v w exact ⟨fun h => h.1, fun h => ⟨h, G.ne_of_adj h⟩⟩ #align simple_graph.from_edge_set_edge_set SimpleGraph.fromEdgeSet_edgeSet @[simp] theorem fromEdgeSet_empty : fromEdgeSet (∅ : Set (Sym2 V)) = ⊥ := by - ext (v w) + ext v w simp only [fromEdgeSet_adj, Set.mem_empty_iff_false, false_and_iff, bot_adj] #align simple_graph.from_edge_set_empty SimpleGraph.fromEdgeSet_empty @[simp] theorem fromEdgeSet_univ : fromEdgeSet (Set.univ : Set (Sym2 V)) = ⊤ := by - ext (v w) + ext v w simp only [fromEdgeSet_adj, Set.mem_univ, true_and_iff, top_adj] #align simple_graph.from_edge_set_univ SimpleGraph.fromEdgeSet_univ @[simp] theorem fromEdgeSet_inf (s t : Set (Sym2 V)) : fromEdgeSet s ⊓ fromEdgeSet t = fromEdgeSet (s ∩ t) := by - ext (v w) + ext v w simp only [fromEdgeSet_adj, Set.mem_inter_iff, Ne.def, inf_adj] tauto #align simple_graph.from_edge_set_inf SimpleGraph.fromEdgeSet_inf @@ -656,14 +656,14 @@ theorem fromEdgeSet_inf (s t : Set (Sym2 V)) : @[simp] theorem fromEdgeSet_sup (s t : Set (Sym2 V)) : fromEdgeSet s ⊔ fromEdgeSet t = fromEdgeSet (s ∪ t) := by - ext (v w) + ext v w simp [Set.mem_union, or_and_right] #align simple_graph.from_edge_set_sup SimpleGraph.fromEdgeSet_sup @[simp] theorem fromEdgeSet_sdiff (s t : Set (Sym2 V)) : fromEdgeSet s \ fromEdgeSet t = fromEdgeSet (s \ t) := by - ext (v w) + ext v w constructor <;> simp (config := { contextual := true }) #align simple_graph.from_edge_set_sdiff SimpleGraph.fromEdgeSet_sdiff @@ -1166,7 +1166,7 @@ theorem deleteEdges_eq_inter_edgeSet (s : Set (Sym2 V)) : theorem deleteEdges_sdiff_eq_of_le {H : SimpleGraph V} (h : H ≤ G) : G.deleteEdges (G.edgeSet \ H.edgeSet) = H := by - ext (v w) + ext v w constructor <;> simp (config := { contextual := true }) [@h v w] #align simple_graph.delete_edges_sdiff_eq_of_le SimpleGraph.deleteEdges_sdiff_eq_of_le diff --git a/Mathlib/Combinatorics/SimpleGraph/Hasse.lean b/Mathlib/Combinatorics/SimpleGraph/Hasse.lean index c1f63ab5fafef..9e8b3da6d6dbf 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Hasse.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Hasse.lean @@ -72,7 +72,7 @@ variable [PartialOrder α] [PartialOrder β] @[simp] theorem hasse_prod : hasse (α × β) = hasse α □ hasse β := by - ext (x y) + ext x y simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm] #align simple_graph.hasse_prod SimpleGraph.hasse_prod diff --git a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean index 4347dd4129ab9..08a68ed4f39af 100644 --- a/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean @@ -190,7 +190,7 @@ theorem incMatrix_mul_transpose_apply_of_adj (h : G.Adj a b) : theorem incMatrix_mul_transpose [Fintype α] [DecidableEq α] [DecidableRel G.Adj] : G.incMatrix R ⬝ (G.incMatrix R)ᵀ = fun a b => if a = b then (G.degree a : R) else if G.Adj a b then 1 else 0 := by - ext (a b) + ext a b split_ifs with h h' · subst b rename Semiring R => sr diff --git a/Mathlib/Control/Functor/Multivariate.lean b/Mathlib/Control/Functor/Multivariate.lean index c60774458d1cc..6181da610c983 100644 --- a/Mathlib/Control/Functor/Multivariate.lean +++ b/Mathlib/Control/Functor/Multivariate.lean @@ -191,14 +191,14 @@ theorem LiftP_PredLast_iff {β} (P : β → Prop) (x : F (α ::: β)) : LiftP' (PredLast' _ P) x ↔ LiftP (PredLast _ P) x := by dsimp only [LiftP, LiftP'] apply exists_iff_exists_of_mono F (f _ n α) (g _ n α) - · ext (i⟨x, _⟩) + · ext i ⟨x, _⟩ cases i <;> rfl · intros rw [MvFunctor.map_map] dsimp [(· ⊚ ·)] suffices (fun i => Subtype.val) = (fun i x => (MvFunctor.f P n α i x).val) by rw[this]; - ext (i⟨x, _⟩) + ext i ⟨x, _⟩ cases i <;> rfl #align mvfunctor.liftp_last_pred_iff MvFunctor.LiftP_PredLast_iff @@ -228,18 +228,18 @@ theorem LiftR_RelLast_iff (x y : F (α ::: β)) : LiftR' (RelLast' _ rr) x y ↔ LiftR (RelLast (i := _) _ rr) x y := by dsimp only [LiftR, LiftR'] apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _) - · ext (i⟨x, _⟩) : 2 + · ext i ⟨x, _⟩ : 2 cases i <;> rfl · intros simp [MvFunctor.map_map, (· ⊚ ·)] -- porting note: proof was -- rw [MvFunctor.map_map, MvFunctor.map_map, (· ⊚ ·), (· ⊚ ·)] - -- congr <;> ext (i⟨x, _⟩) <;> cases i <;> rfl + -- congr <;> ext i ⟨x, _⟩ <;> cases i <;> rfl suffices (fun i t => t.val.fst) = ((fun i x => (MvFunctor.f' rr n α i x).val.fst)) ∧ (fun i t => t.val.snd) = ((fun i x => (MvFunctor.f' rr n α i x).val.snd)) by rcases this with ⟨left, right⟩ rw[left, right]; - constructor <;> ext (i⟨x, _⟩) <;> cases i <;> rfl + constructor <;> ext i ⟨x, _⟩ <;> cases i <;> rfl #align mvfunctor.liftr_last_rel_iff MvFunctor.LiftR_RelLast_iff end LiftPLastPredIff diff --git a/Mathlib/Control/LawfulFix.lean b/Mathlib/Control/LawfulFix.lean index 071c98cad417f..67a5295ef883c 100644 --- a/Mathlib/Control/LawfulFix.lean +++ b/Mathlib/Control/LawfulFix.lean @@ -249,7 +249,7 @@ variable [(x y : _) → OmegaCompletePartialOrder <| γ x y] open OmegaCompletePartialOrder.Chain theorem continuous_curry : Continuous <| monotoneCurry α β γ := fun c ↦ by - ext (x y) + ext x y dsimp [curry, ωSup] rw [map_comp, map_comp] rfl diff --git a/Mathlib/Data/Complex/Module.lean b/Mathlib/Data/Complex/Module.lean index 8bae1155d2514..ab1a84c95857c 100644 --- a/Mathlib/Data/Complex/Module.lean +++ b/Mathlib/Data/Complex/Module.lean @@ -306,7 +306,7 @@ theorem conjAe_coe : ⇑conjAe = conj := @[simp] theorem toMatrix_conjAe : LinearMap.toMatrix basisOneI basisOneI conjAe.toLinearMap = !![1, 0; 0, -1] := by - ext (i j) + ext i j -- Porting note: replaced non-terminal `simp [LinearMap.toMatrix_apply]` fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply] #align complex.to_matrix_conj_ae Complex.toMatrix_conjAe diff --git a/Mathlib/Data/Dfinsupp/Basic.lean b/Mathlib/Data/Dfinsupp/Basic.lean index 177ef9bbf72a7..c1b7734ea6912 100644 --- a/Mathlib/Data/Dfinsupp/Basic.lean +++ b/Mathlib/Data/Dfinsupp/Basic.lean @@ -1481,7 +1481,7 @@ theorem sigmaCurry_apply [∀ i j, Zero (δ i j)] (f : Π₀ i : Σi, _, δ i.1 @[simp] theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] : sigmaCurry (0 : Π₀ i : Σi, _, δ i.1 i.2) = 0 := by - ext (i j) + ext i j rw [sigmaCurry_apply] rfl #align dfinsupp.sigma_curry_zero Dfinsupp.sigmaCurry_zero @@ -1489,7 +1489,7 @@ theorem sigmaCurry_zero [∀ i j, Zero (δ i j)] : sigmaCurry (0 : Π₀ i : Σi @[simp] theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ i : Σi, α i, δ i.1 i.2) : @sigmaCurry _ _ δ _ (f + g) = @sigmaCurry _ _ δ _ f + @sigmaCurry ι α δ _ g := by - ext (i j) + ext i j rw [@add_apply _ (fun i => Π₀ j, δ i j) _ (sigmaCurry _), add_apply, sigmaCurry_apply, sigmaCurry_apply, sigmaCurry_apply, add_apply] #align dfinsupp.sigma_curry_add Dfinsupp.sigmaCurry_add @@ -1498,7 +1498,7 @@ theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ i : Σi, α theorem sigmaCurry_smul [Monoid γ] [∀ i j, AddMonoid (δ i j)] [∀ i j, DistribMulAction γ (δ i j)] (r : γ) (f : Π₀ i : Σi, α i, δ i.1 i.2) : @sigmaCurry _ _ δ _ (r • f) = r • @sigmaCurry _ _ δ _ f := by - ext (i j) + ext i j rw [@smul_apply _ _ (fun i => Π₀ j, δ i j) _ _ _ _ (sigmaCurry _), smul_apply, sigmaCurry_apply, sigmaCurry_apply, smul_apply] #align dfinsupp.sigma_curry_smul Dfinsupp.sigmaCurry_smul @@ -1508,7 +1508,7 @@ theorem sigmaCurry_single [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)] (ij : Σi, α i) (x : δ ij.1 ij.2) : @sigmaCurry _ _ _ _ (single ij x) = single ij.1 (single ij.2 x : Π₀ j, δ ij.1 j) := by obtain ⟨i, j⟩ := ij - ext (i' j') + ext i' j' dsimp only rw [sigmaCurry_apply] obtain rfl | hi := eq_or_ne i i' @@ -1608,7 +1608,7 @@ noncomputable def sigmaCurryEquiv [∀ i j, Zero (δ i j)] ext ⟨i, j⟩ rw [sigmaUncurry_apply, sigmaCurry_apply] right_inv f := by - ext (i j) + ext i j rw [sigmaCurry_apply, sigmaUncurry_apply] #align dfinsupp.sigma_curry_equiv Dfinsupp.sigmaCurryEquiv @@ -1619,8 +1619,7 @@ variable {α : Option ι → Type v} /-- Adds a term to a dfinsupp, making a dfinsupp indexed by an `Option`. This is the dfinsupp version of `Option.rec`. -/ -def extendWith [∀ i, Zero (α i)] (a : α none) (f : Π₀ i, α (some i)) : Π₀ i, α i - where +def extendWith [∀ i, Zero (α i)] (a : α none) (f : Π₀ i, α (some i)) : Π₀ i, α i where toFun := fun i ↦ match i with | none => a | some _ => f _ support' := f.support'.map fun s => diff --git a/Mathlib/Data/Dfinsupp/Interval.lean b/Mathlib/Data/Dfinsupp/Interval.lean index ad2d9c00a01c1..c4054d2ea8d2d 100644 --- a/Mathlib/Data/Dfinsupp/Interval.lean +++ b/Mathlib/Data/Dfinsupp/Interval.lean @@ -36,7 +36,7 @@ def dfinsupp (s : Finset ι) (t : ∀ i, Finset (α i)) : Finset (Π₀ i, α i) (s.pi t).map ⟨fun f => Dfinsupp.mk s fun i => f i i.2, by refine' (mk_injective _).comp fun f g h => _ - ext (i hi) + ext i hi convert congr_fun h ⟨i, hi⟩⟩ #align finset.dfinsupp Finset.dfinsupp diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean index fb42e50b34cf7..c822ccfaa93e8 100644 --- a/Mathlib/Data/FinEnum.lean +++ b/Mathlib/Data/FinEnum.lean @@ -233,14 +233,14 @@ def pi {β : α → Type max u v} [DecidableEq α] : theorem mem_pi {β : α → Type _} [FinEnum α] [∀ a, FinEnum (β a)] (xs : List α) (f : ∀ a, a ∈ xs → β a) : f ∈ pi xs fun x => toList (β x) := by induction' xs with xs_hd xs_tl xs_ih <;> simp [pi, -List.map_eq_map, monad_norm, functor_norm] - · ext (a⟨⟩) + · ext a ⟨⟩ · exists Pi.cons xs_hd xs_tl (f _ (List.mem_cons_self _ _)) constructor exact ⟨_, rfl⟩ exists Pi.tail f constructor · apply xs_ih - · ext (x h) + · ext x h simp [Pi.cons] split_ifs · subst x diff --git a/Mathlib/Data/Finset/Pi.lean b/Mathlib/Data/Finset/Pi.lean index 563b34d75e4ac..c79006a4d945e 100644 --- a/Mathlib/Data/Finset/Pi.lean +++ b/Mathlib/Data/Finset/Pi.lean @@ -117,7 +117,7 @@ theorem pi_singletons {β : Type _} (s : Finset α) (f : α → β) : constructor · simp intro a ha - ext (i hi) + ext i hi rw [mem_pi] at ha simpa using ha i hi #align finset.pi_singletons Finset.pi_singletons diff --git a/Mathlib/Data/Finsupp/Indicator.lean b/Mathlib/Data/Finsupp/Indicator.lean index a6dede302d11c..76dd892b55608 100644 --- a/Mathlib/Data/Finsupp/Indicator.lean +++ b/Mathlib/Data/Finsupp/Indicator.lean @@ -62,7 +62,7 @@ theorem indicator_apply [DecidableEq ι] : indicator s f i = if hi : i ∈ s the theorem indicator_injective : Injective fun f : ∀ i ∈ s, α => indicator s f := by intro a b h - ext (i hi) + ext i hi rw [← indicator_of_mem hi a, ← indicator_of_mem hi b] exact FunLike.congr_fun h i #align finsupp.indicator_injective Finsupp.indicator_injective diff --git a/Mathlib/Data/Finsupp/ToDfinsupp.lean b/Mathlib/Data/Finsupp/ToDfinsupp.lean index 786bd3ea82cf9..0c09d6a53e4b7 100644 --- a/Mathlib/Data/Finsupp/ToDfinsupp.lean +++ b/Mathlib/Data/Finsupp/ToDfinsupp.lean @@ -327,7 +327,7 @@ theorem sigmaFinsuppEquivDfinsupp_single [DecidableEq ι] [Zero N] (a : Σi, η sigmaFinsuppEquivDfinsupp (Finsupp.single a n) = @Dfinsupp.single _ (fun i => η i →₀ N) _ _ a.1 (Finsupp.single a.2 n) := by obtain ⟨i, a⟩ := a - ext (j b) + ext j b by_cases h : i = j · subst h classical simp [split_apply, Finsupp.single_apply] diff --git a/Mathlib/Data/Holor.lean b/Mathlib/Data/Holor.lean index d9060ed60b0cf..b02b2bf07195f 100644 --- a/Mathlib/Data/Holor.lean +++ b/Mathlib/Data/Holor.lean @@ -295,7 +295,7 @@ theorem sum_unitVec_mul_slice [Ring α] (x : Holor α (d :: ds)) : unitVec d i ⊗ slice x i (Nat.succ_le_of_lt (Finset.mem_range.1 i.prop))) = x := by apply slice_eq _ _ _ - ext (i hid) + ext i hid rw [← slice_sum] simp only [slice_unitVec_mul hid] rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)] diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean index 52ff80ac796a9..feebf59b1960c 100644 --- a/Mathlib/Data/Matrix/Basic.lean +++ b/Mathlib/Data/Matrix/Basic.lean @@ -2873,7 +2873,7 @@ theorem diagonal_updateRow_single [DecidableEq n] [Zero α] (v : n → α) (i : theorem updateRow_submatrix_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n) : updateRow (A.submatrix e f) i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix e f := by - ext (i' j) + ext i' j simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply] #align matrix.update_row_submatrix_equiv Matrix.updateRow_submatrix_equiv diff --git a/Mathlib/Data/Matrix/Basis.lean b/Mathlib/Data/Matrix/Basis.lean index cfc8b79370f49..ae76827ba8d0d 100644 --- a/Mathlib/Data/Matrix/Basis.lean +++ b/Mathlib/Data/Matrix/Basis.lean @@ -196,7 +196,7 @@ theorem mul_right_apply_of_ne (a b : n) (hbj : b ≠ j) (M : Matrix n n α) : @[simp] theorem mul_same (k : n) (d : α) : stdBasisMatrix i j c ⬝ stdBasisMatrix j k d = stdBasisMatrix i k (c * d) := by - ext (a b) + ext a b simp only [mul_apply, stdBasisMatrix, boole_mul] by_cases h₁ : i = a <;> by_cases h₂ : k = b <;> simp [h₁, h₂] #align matrix.std_basis_matrix.mul_same Matrix.StdBasisMatrix.mul_same @@ -204,7 +204,7 @@ theorem mul_same (k : n) (d : α) : @[simp] theorem mul_of_ne {k l : n} (h : j ≠ k) (d : α) : stdBasisMatrix i j c ⬝ stdBasisMatrix k l d = 0 := by - ext (a b) + ext a b simp only [mul_apply, boole_mul, stdBasisMatrix] by_cases h₁ : i = a -- Porting note: was `simp [h₁, h, h.symm]` diff --git a/Mathlib/Data/Matrix/Block.lean b/Mathlib/Data/Matrix/Block.lean index ae0eb9c9bd932..2c152ec43766c 100644 --- a/Mathlib/Data/Matrix/Block.lean +++ b/Mathlib/Data/Matrix/Block.lean @@ -146,7 +146,7 @@ theorem fromBlocks_inj {A : Matrix n l α} {B : Matrix n m α} {C : Matrix o l theorem fromBlocks_map (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : α → β) : (fromBlocks A B C D).map f = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) := - by ext (i j); rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks] + by ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks] #align matrix.from_blocks_map Matrix.fromBlocks_map theorem fromBlocks_transpose (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) @@ -164,7 +164,7 @@ theorem fromBlocks_conjTranspose [Star α] (A : Matrix n l α) (B : Matrix n m theorem fromBlocks_submatrix_sum_swap_left (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : p → Sum l m) : (fromBlocks A B C D).submatrix Sum.swap f = (fromBlocks C D A B).submatrix id f := by - ext (i j) + ext i j cases i <;> dsimp <;> cases f j <;> rfl #align matrix.from_blocks_submatrix_sum_swap_left Matrix.fromBlocks_submatrix_sum_swap_left @@ -172,7 +172,7 @@ theorem fromBlocks_submatrix_sum_swap_left (A : Matrix n l α) (B : Matrix n m theorem fromBlocks_submatrix_sum_swap_right (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : p → Sum n o) : (fromBlocks A B C D).submatrix f Sum.swap = (fromBlocks B A D C).submatrix f id := by - ext (i j) + ext i j cases j <;> dsimp <;> cases f i <;> rfl #align matrix.from_blocks_submatrix_sum_swap_right Matrix.fromBlocks_submatrix_sum_swap_right @@ -225,7 +225,7 @@ theorem toSquareBlock_def (M : Matrix m m α) (b : m → β) (k : β) : theorem fromBlocks_smul [SMul R α] (x : R) (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) : x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D) := by - ext (i j); rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks] + ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks] #align matrix.from_blocks_smul Matrix.fromBlocks_smul theorem fromBlocks_neg [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix o l R) @@ -236,7 +236,7 @@ theorem fromBlocks_neg [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix @[simp] theorem fromBlocks_zero [Zero α] : fromBlocks (0 : Matrix n l α) 0 0 (0 : Matrix o m α) = 0 := by - ext (i j) + ext i j rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl #align matrix.from_blocks_zero Matrix.fromBlocks_zero @@ -244,7 +244,7 @@ theorem fromBlocks_add [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Mat (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α) (D' : Matrix o m α) : fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D') := - by ext (i j); rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl + by ext i j; rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl #align matrix.from_blocks_add Matrix.fromBlocks_add theorem fromBlocks_multiply [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) @@ -283,7 +283,7 @@ variable [Zero α] theorem toBlock_diagonal_self (d : m → α) (p : m → Prop) : Matrix.toBlock (diagonal d) p p = diagonal fun i : Subtype p => d ↑i := by - ext (i j) + ext i j by_cases i = j · simp [h] · simp [One.one, h, Subtype.val_injective.ne h] @@ -291,7 +291,7 @@ theorem toBlock_diagonal_self (d : m → α) (p : m → Prop) : theorem toBlock_diagonal_disjoint (d : m → α) {p q : m → Prop} (hpq : Disjoint p q) : Matrix.toBlock (diagonal d) p q = 0 := by - ext (⟨i, hi⟩⟨j, hj⟩) + ext ⟨i, hi⟩ ⟨j, hj⟩ have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩ simp [diagonal_apply_ne d this] #align matrix.to_block_diagonal_disjoint Matrix.toBlock_diagonal_disjoint @@ -311,7 +311,7 @@ variable [Zero α] [One α] @[simp] theorem fromBlocks_one : fromBlocks (1 : Matrix l l α) 0 0 (1 : Matrix m m α) = 1 := by - ext (i j) + ext i j rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [one_apply] #align matrix.from_blocks_one Matrix.fromBlocks_one @@ -404,7 +404,7 @@ theorem blockDiagonal_zero : blockDiagonal (0 : o → Matrix m n α) = 0 := by @[simp] theorem blockDiagonal_diagonal [DecidableEq m] (d : o → m → α) : (blockDiagonal fun k => diagonal (d k)) = diagonal fun ik => d ik.2 ik.1 := by - ext (⟨i, k⟩⟨j, k'⟩) + ext ⟨i, k⟩ ⟨j, k'⟩ simp only [blockDiagonal_apply, diagonal_apply, Prod.mk.inj_iff, ← ite_and] congr 1 rw [and_comm] @@ -457,7 +457,7 @@ theorem blockDiagonal_sub [AddGroup α] (M N : o → Matrix m n α) : theorem blockDiagonal_mul [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : o → Matrix m n α) (N : o → Matrix n p α) : (blockDiagonal fun k => M k ⬝ N k) = blockDiagonal M ⬝ blockDiagonal N := by - ext (⟨i, k⟩ ⟨j, k'⟩) + ext ⟨i, k⟩ ⟨j, k'⟩ simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product] split_ifs with h <;> simp [h] #align matrix.block_diagonal_mul Matrix.blockDiagonal_mul @@ -675,7 +675,7 @@ theorem blockDiagonal'_map (M : ∀ i, Matrix (m' i) (n' i) α) (f : α → β) @[simp] theorem blockDiagonal'_transpose (M : ∀ i, Matrix (m' i) (n' i) α) : (blockDiagonal' M)ᵀ = blockDiagonal' fun k => (M k)ᵀ := by - ext (⟨ii, ix⟩⟨ji, jx⟩) + ext ⟨ii, ix⟩ ⟨ji, jx⟩ simp only [transpose_apply, blockDiagonal'_apply] split_ifs with h -- Porting note: was split_ifs <;> cc · subst h; rfl @@ -700,7 +700,7 @@ theorem blockDiagonal'_zero : blockDiagonal' (0 : ∀ i, Matrix (m' i) (n' i) α @[simp] theorem blockDiagonal'_diagonal [∀ i, DecidableEq (m' i)] (d : ∀ i, m' i → α) : (blockDiagonal' fun k => diagonal (d k)) = diagonal fun ik => d ik.1 ik.2 := by - ext (⟨i, k⟩⟨j, k'⟩) + ext ⟨i, k⟩ ⟨j, k'⟩ simp only [blockDiagonal'_apply, diagonal] obtain rfl | hij := Decidable.eq_or_ne i j · simp @@ -755,7 +755,7 @@ theorem blockDiagonal'_sub [AddGroup α] (M N : ∀ i, Matrix (m' i) (n' i) α) theorem blockDiagonal'_mul [NonUnitalNonAssocSemiring α] [∀ i, Fintype (n' i)] [Fintype o] (M : ∀ i, Matrix (m' i) (n' i) α) (N : ∀ i, Matrix (n' i) (p' i) α) : (blockDiagonal' fun k => M k ⬝ N k) = blockDiagonal' M ⬝ blockDiagonal' N := by - ext (⟨k, i⟩⟨k', j⟩) + ext ⟨k, i⟩ ⟨k', j⟩ simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma] rw [Fintype.sum_eq_single k] · simp only [if_pos, dif_pos] -- porting note: added @@ -921,7 +921,7 @@ variable [CommRing R] theorem toBlock_mul_eq_mul {m n k : Type _} [Fintype n] (p : m → Prop) (q : k → Prop) (A : Matrix m n R) (B : Matrix n k R) : (A ⬝ B).toBlock p q = A.toBlock p ⊤ ⬝ B.toBlock ⊤ q := by - ext (i k) + ext i k simp only [toBlock_apply, mul_apply] rw [Finset.sum_subtype] simp [Pi.top_apply, Prop.top_eq_true] @@ -931,7 +931,7 @@ theorem toBlock_mul_eq_add {m n k : Type _} [Fintype n] (p : m → Prop) (q : n [DecidablePred q] (r : k → Prop) (A : Matrix m n R) (B : Matrix n k R) : (A ⬝ B).toBlock p r = A.toBlock p q ⬝ B.toBlock q r + (A.toBlock p fun i => ¬q i) ⬝ B.toBlock (fun i => ¬q i) r := by classical - ext (i k) + ext i k simp only [toBlock_apply, mul_apply, Pi.add_apply] exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm #align matrix.to_block_mul_eq_add Matrix.toBlock_mul_eq_add diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean index 1330c8a059ce5..7952e86a957ac 100644 --- a/Mathlib/Data/Matrix/Kronecker.lean +++ b/Mathlib/Data/Matrix/Kronecker.lean @@ -128,14 +128,14 @@ theorem kroneckerMap_smul_right [SMul R β] [SMul R γ] (f : α → β → γ) ( theorem kroneckerMap_diagonal_diagonal [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n] (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : m → α) (b : n → β) : kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.1) (b mn.2) := by - ext (⟨i₁, i₂⟩⟨j₁, j₂⟩) + ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂] #align matrix.kronecker_map_diagonal_diagonal Matrix.kroneckerMap_diagonal_diagonal theorem kroneckerMap_diagonal_right [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ) (hf : ∀ a, f a 0 = 0) (A : Matrix l m α) (b : n → β) : kroneckerMap f A (diagonal b) = blockDiagonal fun i => A.map fun a => f a (b i) := by - ext (⟨i₁, i₂⟩⟨j₁, j₂⟩) + ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf] #align matrix.kronecker_map_diagonal_right Matrix.kroneckerMap_diagonal_right @@ -144,7 +144,7 @@ theorem kroneckerMap_diagonal_left [Zero α] [Zero γ] [DecidableEq l] (f : α kroneckerMap f (diagonal a) B = Matrix.reindex (Equiv.prodComm _ _) (Equiv.prodComm _ _) (blockDiagonal fun i => B.map fun b => f (a i) b) := by - ext (⟨i₁, i₂⟩⟨j₁, j₂⟩) + ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ simp [diagonal, blockDiagonal, apply_ite f, ite_apply, hf] #align matrix.kronecker_map_diagonal_left Matrix.kroneckerMap_diagonal_left @@ -159,7 +159,7 @@ theorem kroneckerMap_reindex (f : α → β → γ) (el : l ≃ l') (em : m ≃ (M : Matrix l m α) (N : Matrix n p β) : kroneckerMap f (reindex el em M) (reindex en ep N) = reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N) := by - ext (⟨i, i'⟩⟨j, j'⟩) + ext ⟨i, i'⟩ ⟨j, j'⟩ rfl #align matrix.kronecker_map_reindex Matrix.kroneckerMap_reindex @@ -216,7 +216,7 @@ theorem kroneckerMapBilinear_mul_mul [CommSemiring R] [Fintype m] [Fintype m'] (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) : kroneckerMapBilinear f (A ⬝ B) (A' ⬝ B') = kroneckerMapBilinear f A A' ⬝ kroneckerMapBilinear f B B' := by - ext (⟨i, i'⟩⟨j, j'⟩) + ext ⟨i, i'⟩ ⟨j, j'⟩ simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply] simp_rw [f.map_sum, LinearMap.sum_apply, LinearMap.map_sum, h_comm] @@ -384,9 +384,9 @@ theorem det_kronecker [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [C det (A ⊗ₖ B) = det A ^ Fintype.card n * det B ^ Fintype.card m := by refine' (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans _ congr 3 - · ext (i j) + · ext i j exact mul_one _ - · ext (i j) + · ext i j exact one_mul _ #align matrix.det_kronecker Matrix.det_kronecker diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean index bac0c5540011f..ba335723a89b2 100644 --- a/Mathlib/Data/Matrix/Notation.lean +++ b/Mathlib/Data/Matrix/Notation.lean @@ -171,7 +171,7 @@ theorem col_empty (v : Fin 0 → α) : col v = vecEmpty := @[simp] theorem col_cons (x : α) (u : Fin m → α) : col (vecCons x u) = vecCons (fun _ => x) (col u) := by - ext (i j) + ext i j refine' Fin.cases _ _ i <;> simp [vecHead, vecTail] #align matrix.col_cons Matrix.col_cons @@ -204,7 +204,7 @@ theorem transpose_empty_cols (A : Matrix (Fin 0) m' α) : Aᵀ = of fun _ => ![] @[simp] theorem cons_transpose (v : n' → α) (A : Matrix (Fin m) n' α) : (of (vecCons v A))ᵀ = of fun i => vecCons (v i) (Aᵀ i) := by - ext (i j) + ext i j refine' Fin.cases _ _ j <;> simp #align matrix.cons_transpose Matrix.cons_transpose @@ -216,7 +216,7 @@ theorem head_transpose (A : Matrix m' (Fin n.succ) α) : @[simp] theorem tail_transpose (A : Matrix m' (Fin n.succ) α) : vecTail (of.symm Aᵀ) = (vecTail ∘ A)ᵀ := by - ext (i j) + ext i j rfl #align matrix.tail_transpose Matrix.tail_transpose @@ -250,7 +250,7 @@ theorem mul_val_succ [Fintype n'] (A : Matrix (Fin m.succ) n' α) (B : Matrix n' @[simp] theorem cons_mul [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α) : of (vecCons v A) ⬝ B = of (vecCons (vecMul v B) (of.symm (of A ⬝ B))) := by - ext (i j) + ext i j refine' Fin.cases _ _ i · rfl simp [mul_val_succ] @@ -347,7 +347,7 @@ theorem cons_vecMulVec (x : α) (v : Fin m → α) (w : n' → α) : @[simp] theorem vecMulVec_cons (v : m' → α) (x : α) (w : Fin n → α) : vecMulVec v (vecCons x w) = fun i => v i • vecCons x w := by - ext (i j) + ext i j rw [vecMulVec_apply, Pi.smul_apply, smul_eq_mul] #align matrix.vec_mul_vec_cons Matrix.vecMulVec_cons @@ -382,7 +382,7 @@ theorem submatrix_empty (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → @[simp] theorem submatrix_cons_row (A : Matrix m' n' α) (i : m') (row : Fin m → m') (col : o' → n') : submatrix A (vecCons i row) col = vecCons (fun j => A i (col j)) (submatrix A row col) := by - ext (i j) + ext i j refine' Fin.cases _ _ i <;> simp [submatrix] #align matrix.submatrix_cons_row Matrix.submatrix_cons_row @@ -409,19 +409,19 @@ section One variable [Zero α] [One α] theorem one_fin_two : (1 : Matrix (Fin 2) (Fin 2) α) = !![1, 0; 0, 1] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> rfl #align matrix.one_fin_two Matrix.one_fin_two theorem one_fin_three : (1 : Matrix (Fin 3) (Fin 3) α) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> rfl #align matrix.one_fin_three Matrix.one_fin_three end One theorem eta_fin_two (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> rfl #align matrix.eta_fin_two Matrix.eta_fin_two @@ -429,7 +429,7 @@ theorem eta_fin_three (A : Matrix (Fin 3) (Fin 3) α) : A = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> rfl #align matrix.eta_fin_three Matrix.eta_fin_three @@ -438,7 +438,7 @@ theorem mul_fin_two [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ a₂₁, a₂₂] ⬝ !![b₁₁, b₁₂; b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.mul, dotProduct, Fin.sum_univ_succ] #align matrix.mul_fin_two Matrix.mul_fin_two @@ -452,7 +452,7 @@ theorem mul_fin_three [AddCommMonoid α] [Mul α] !![a₁₁*b₁₁ + a₁₂*b₂₁ + a₁₃*b₃₁, a₁₁*b₁₂ + a₁₂*b₂₂ + a₁₃*b₃₂, a₁₁*b₁₃ + a₁₂*b₂₃ + a₁₃*b₃₃; a₂₁*b₁₁ + a₂₂*b₂₁ + a₂₃*b₃₁, a₂₁*b₁₂ + a₂₂*b₂₂ + a₂₃*b₃₂, a₂₁*b₁₃ + a₂₂*b₂₃ + a₂₃*b₃₃; a₃₁*b₁₁ + a₃₂*b₂₁ + a₃₃*b₃₁, a₃₁*b₁₂ + a₃₂*b₂₂ + a₃₃*b₃₂, a₃₁*b₁₃ + a₃₂*b₂₃ + a₃₃*b₃₃] := by - ext (i j) + ext i j fin_cases i <;> fin_cases j <;> simp [Matrix.mul, dotProduct, Fin.sum_univ_succ, ← add_assoc] #align matrix.mul_fin_three Matrix.mul_fin_three diff --git a/Mathlib/Data/Matrix/PEquiv.lean b/Mathlib/Data/Matrix/PEquiv.lean index 0e3fcee383812..1fffbb27c76e3 100644 --- a/Mathlib/Data/Matrix/PEquiv.lean +++ b/Mathlib/Data/Matrix/PEquiv.lean @@ -104,7 +104,7 @@ theorem matrix_mul_apply [Fintype m] [Semiring α] [DecidableEq n] (M : Matrix l theorem toPEquiv_mul_matrix [Fintype m] [DecidableEq m] [Semiring α] (f : m ≃ m) (M : Matrix m n α) : f.toPEquiv.toMatrix ⬝ M = fun i => M (f i) := by - ext (i j) + ext i j rw [mul_matrix_apply, Equiv.toPEquiv_apply] #align pequiv.to_pequiv_mul_matrix PEquiv.toPEquiv_mul_matrix @@ -117,7 +117,7 @@ theorem mul_toPEquiv_toMatrix {m n α : Type _} [Fintype n] [DecidableEq n] [Sem theorem toMatrix_trans [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring α] (f : l ≃. m) (g : m ≃. n) : ((f.trans g).toMatrix : Matrix l n α) = f.toMatrix ⬝ g.toMatrix := by - ext (i j) + ext i j rw [mul_matrix_apply] dsimp [toMatrix, PEquiv.trans] cases f i <;> simp diff --git a/Mathlib/Data/Multiset/Pi.lean b/Mathlib/Data/Multiset/Pi.lean index 9988bacdf39a4..3d97a44d93f88 100644 --- a/Mathlib/Data/Multiset/Pi.lean +++ b/Mathlib/Data/Multiset/Pi.lean @@ -64,7 +64,7 @@ theorem Pi.cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : @[simp, nolint simpNF] --Porting note: false positive, this lemma can prove itself theorem pi.cons_eta {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') : (Pi.cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f := by - ext (a' h') + ext a' h' by_cases h : a' = a · subst h rw [Pi.cons_same] diff --git a/Mathlib/Data/MvPolynomial/Equiv.lean b/Mathlib/Data/MvPolynomial/Equiv.lean index 134260cb12018..da9f96c47250f 100644 --- a/Mathlib/Data/MvPolynomial/Equiv.lean +++ b/Mathlib/Data/MvPolynomial/Equiv.lean @@ -221,7 +221,7 @@ def isEmptyAlgEquiv [he : IsEmpty σ] : MvPolynomial σ R ≃ₐ[R] R := ext simp [Algebra.ofId_apply, algebraMap_eq]) (by - ext (i m) + ext i m exact IsEmpty.elim' he i) #align mv_polynomial.is_empty_alg_equiv MvPolynomial.isEmptyAlgEquiv diff --git a/Mathlib/Data/Nat/Bits.lean b/Mathlib/Data/Nat/Bits.lean index 9ed5dcf6621af..ccb4af79d19d1 100644 --- a/Mathlib/Data/Nat/Bits.lean +++ b/Mathlib/Data/Nat/Bits.lean @@ -140,7 +140,7 @@ theorem bitCasesOn_bit1 {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (n : ℕ theorem bit_cases_on_injective {C : ℕ → Sort u} : Function.Injective fun H : ∀ b n, C (bit b n) => fun n => bitCasesOn n H := by intro H₁ H₂ h - ext (b n) + ext b n simpa only [bitCasesOn_bit] using congr_fun h (bit b n) #align nat.bit_cases_on_injective Nat.bit_cases_on_injective diff --git a/Mathlib/Data/Nat/Hyperoperation.lean b/Mathlib/Data/Nat/Hyperoperation.lean index c5c1ee642fddc..280a7a6582a15 100644 --- a/Mathlib/Data/Nat/Hyperoperation.lean +++ b/Mathlib/Data/Nat/Hyperoperation.lean @@ -63,7 +63,7 @@ theorem hyperoperation_recursion (n m k : ℕ) : -- Interesting hyperoperation lemmas @[simp] theorem hyperoperation_one : hyperoperation 1 = (· + ·) := by - ext (m k) + ext m k induction' k with bn bih · rw [Nat.add_zero m, hyperoperation] · rw [hyperoperation_recursion, bih, hyperoperation_zero] @@ -72,7 +72,7 @@ theorem hyperoperation_one : hyperoperation 1 = (· + ·) := by @[simp] theorem hyperoperation_two : hyperoperation 2 = (· * ·) := by - ext (m k) + ext m k induction' k with bn bih · rw [hyperoperation] exact (Nat.mul_zero m).symm @@ -85,7 +85,7 @@ theorem hyperoperation_two : hyperoperation 2 = (· * ·) := by @[simp] theorem hyperoperation_three : hyperoperation 3 = (· ^ ·) := by - ext (m k) + ext m k induction' k with bn bih · rw [hyperoperation_ge_three_eq_one] exact (pow_zero m).symm diff --git a/Mathlib/Data/Nat/Interval.lean b/Mathlib/Data/Nat/Interval.lean index ff33e3b8e5b81..30dd0f964366c 100644 --- a/Mathlib/Data/Nat/Interval.lean +++ b/Mathlib/Data/Nat/Interval.lean @@ -81,7 +81,7 @@ theorem Ioo_eq_range' : Ioo a b = ⟨List.range' (a + 1) (b - a - 1), List.nodup #align nat.Ioo_eq_range' Nat.Ioo_eq_range' theorem Iio_eq_range : Iio = range := by - ext (b x) + ext b x rw [mem_Iio, mem_range] #align nat.Iio_eq_range Nat.Iio_eq_range diff --git a/Mathlib/Data/Nat/Upto.lean b/Mathlib/Data/Nat/Upto.lean index 52363118ef143..902ad210de3ef 100644 --- a/Mathlib/Data/Nat/Upto.lean +++ b/Mathlib/Data/Nat/Upto.lean @@ -58,7 +58,7 @@ protected theorem wf : (∃ x, p x) → WellFounded (Upto.GT p) suffices Upto.GT p = Measure fun y : Nat.Upto p => x - y.val by rw [this] exact (measure _).wf - ext (⟨a, ha⟩⟨b, _⟩) + ext ⟨a, ha⟩ ⟨b, _⟩ dsimp [Measure, InvImage, Upto.GT] rw [tsub_lt_tsub_iff_left_of_le (le_of_not_lt fun h' => ha _ h' h)] #align nat.upto.wf Nat.Upto.wf diff --git a/Mathlib/Data/PEquiv.lean b/Mathlib/Data/PEquiv.lean index 953d3a56e880e..d4434d980303e 100644 --- a/Mathlib/Data/PEquiv.lean +++ b/Mathlib/Data/PEquiv.lean @@ -385,7 +385,7 @@ theorem single_trans_single (a : α) (b : β) (c : γ) : @[simp] theorem single_subsingleton_eq_refl [Subsingleton α] (a b : α) : single a b = PEquiv.refl α := by - ext (i j) + ext i j dsimp [single] rw [if_pos (Subsingleton.elim i a), Subsingleton.elim i j, Subsingleton.elim b j] #align pequiv.single_subsingleton_eq_refl PEquiv.single_subsingleton_eq_refl diff --git a/Mathlib/Data/PFunctor/Multivariate/W.lean b/Mathlib/Data/PFunctor/Multivariate/W.lean index b99c4d9db1e76..16619bbbf5141 100644 --- a/Mathlib/Data/PFunctor/Multivariate/W.lean +++ b/Mathlib/Data/PFunctor/Multivariate/W.lean @@ -111,14 +111,14 @@ set_option linter.uppercaseLean3 false in theorem wPathCasesOn_eta {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W} (h : P.WPath ⟨a, f⟩ ⟹ α) : P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h := by - ext (i x) ; cases x <;> rfl + ext i x ; cases x <;> rfl set_option linter.uppercaseLean3 false in #align mvpfunctor.W_path_cases_on_eta MvPFunctor.wPathCasesOn_eta theorem comp_wPathCasesOn {α β : TypeVec n} (h : α ⟹ β) {a : P.A} {f : P.last.B a → P.last.W} (g' : P.drop.B a ⟹ α) (g : ∀ j : P.last.B a, P.WPath (f j) ⟹ α) : h ⊚ P.wPathCasesOn g' g = P.wPathCasesOn (h ⊚ g') fun i => h ⊚ g i := by - ext (i x) ; cases x <;> rfl + ext i x ; cases x <;> rfl set_option linter.uppercaseLean3 false in #align mvpfunctor.comp_W_path_cases_on MvPFunctor.comp_wPathCasesOn diff --git a/Mathlib/Data/Polynomial/HasseDeriv.lean b/Mathlib/Data/Polynomial/HasseDeriv.lean index 915a30007c6f7..c3806ebc5c9ab 100644 --- a/Mathlib/Data/Polynomial/HasseDeriv.lean +++ b/Mathlib/Data/Polynomial/HasseDeriv.lean @@ -148,7 +148,7 @@ set_option linter.uppercaseLean3 false in theorem factorial_smul_hasseDeriv : ⇑(k ! • @hasseDeriv R _ k) = @derivative R _^[k] := by induction' k with k ih · rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe] - ext (f n) : 2 + ext f n : 2 rw [iterate_succ_apply', ← ih] simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative, hasseDeriv_coeff, ← @choose_symm_add _ k] @@ -242,7 +242,7 @@ theorem hasseDeriv_mul (f g : R[X]) : simp only [← finset_sum_apply] congr 2 clear f g - ext (m r n s) : 4 + ext m r n s : 4 simp only [finset_sum_apply, coe_mulLeft, coe_comp, flip_apply, Function.comp_apply, hasseDeriv_monomial, LinearMap.toAddMonoidHom_coe, compHom_apply_apply, coe_mul, monomial_mul_monomial] diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean index 3ffa8a7ab1e6b..98c4d97c18e88 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean @@ -305,7 +305,7 @@ theorem Fix.dest_mk (x : F (append1 α (Fix F α))) : Fix.dest (Fix.mk x) = x := rw [← MvFunctor.id_map x] rw [← appendFun_comp, id_comp] have : Fix.mk ∘ Fix.dest = _root_.id := by - ext (x: Fix F α) + ext (x : Fix F α) apply Fix.mk_dest rw [this, appendFun_id_id] #align mvqpf.fix.dest_mk MvQPF.Fix.dest_mk diff --git a/Mathlib/Data/Rel.lean b/Mathlib/Data/Rel.lean index b8011d15e0fd6..26e612ebcba9d 100644 --- a/Mathlib/Data/Rel.lean +++ b/Mathlib/Data/Rel.lean @@ -63,7 +63,7 @@ theorem inv_def (x : α) (y : β) : r.inv y x ↔ r x y := #align rel.inv_def Rel.inv_def theorem inv_inv : inv (inv r) = r := by - ext (x y) + ext x y rfl #align rel.inv_inv Rel.inv_inv @@ -118,12 +118,12 @@ theorem comp_left_id (r : Rel α β) : @Eq α • r = r := by #align rel.comp_left_id Rel.comp_left_id theorem inv_id : inv (@Eq α) = @Eq α := by - ext (x y) + ext x y constructor <;> apply Eq.symm #align rel.inv_id Rel.inv_id theorem inv_comp (r : Rel α β) (s : Rel β γ) : inv (r • s) = inv s • inv r := by - ext (x z) + ext x z simp [comp, inv, flip, and_comm] #align rel.inv_comp Rel.inv_comp diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean index 1b5bd6fffa1da..f069ae06b9a7d 100644 --- a/Mathlib/Data/TypeVec.lean +++ b/Mathlib/Data/TypeVec.lean @@ -665,7 +665,7 @@ theorem diag_sub_val {n} {α : TypeVec.{u} n} : subtypeVal (repeatEq α) ⊚ dia theorem prod_id : ∀ {n} {α β : TypeVec.{u} n}, (id ⊗' id) = (id : α ⊗ β ⟹ _) := by intros - ext (i a) + ext i a induction' i with _ _ _ i_ih · cases a rfl @@ -675,7 +675,7 @@ theorem prod_id : ∀ {n} {α β : TypeVec.{u} n}, (id ⊗' id) = (id : α ⊗ theorem append_prod_appendFun {n} {α α' β β' : TypeVec.{u} n} {φ φ' ψ ψ' : Type u} {f₀ : α ⟹ α'} {g₀ : β ⟹ β'} {f₁ : φ → φ'} {g₁ : ψ → ψ'} : ((f₀ ⊗' g₀) ::: (_root_.Prod.map f₁ g₁)) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) := by - ext (i a) + ext i a cases i . cases a rfl @@ -793,7 +793,7 @@ theorem subtypeVal_diagSub {α : TypeVec n} : subtypeVal (repeatEq α) ⊚ diagS @[simp] theorem toSubtype_of_subtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) : toSubtype p ⊚ ofSubtype p = id := by - ext (i x) + ext i x induction i <;> dsimp only [id, toSubtype, comp, ofSubtype] at * simp [*] #align typevec.to_subtype_of_subtype TypeVec.toSubtype_of_subtype @@ -801,7 +801,7 @@ theorem toSubtype_of_subtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) : @[simp] theorem subtypeVal_toSubtype {α : TypeVec n} (p : α ⟹ «repeat» n Prop) : subtypeVal p ⊚ toSubtype p = fun _ => Subtype.val := by - ext (i x) + ext i x induction i <;> dsimp only [toSubtype, comp, subtypeVal] at * simp [*] #align typevec.subtype_val_to_subtype TypeVec.subtypeVal_toSubtype @@ -817,7 +817,7 @@ theorem toSubtype_of_subtype_assoc {α β : TypeVec n} @[simp] theorem toSubtype'_of_subtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n Prop) : toSubtype' r ⊚ ofSubtype' r = id := by - ext (i x) + ext i x induction i <;> dsimp only [id, toSubtype', comp, ofSubtype'] at * <;> simp [Subtype.eta, *] @@ -825,7 +825,9 @@ theorem toSubtype'_of_subtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n theorem subtypeVal_toSubtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n Prop) : subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i x.1.fst x.1.snd := by - ext (i x); induction i <;> dsimp only [id, toSubtype', comp, subtypeVal, prod.mk] at *; simp [*] + ext i x + induction i <;> dsimp only [id, toSubtype', comp, subtypeVal, prod.mk] at * + simp [*] #align typevec.subtype_val_to_subtype' TypeVec.subtypeVal_toSubtype' end TypeVec diff --git a/Mathlib/GroupTheory/DoubleCoset.lean b/Mathlib/GroupTheory/DoubleCoset.lean index 879774fbd3837..774d7194a392a 100644 --- a/Mathlib/GroupTheory/DoubleCoset.lean +++ b/Mathlib/GroupTheory/DoubleCoset.lean @@ -93,7 +93,7 @@ theorem rel_iff {H K : Subgroup G} {x y : G} : theorem bot_rel_eq_leftRel (H : Subgroup G) : (setoid ↑(⊥ : Subgroup G) ↑H).Rel = (QuotientGroup.leftRel H).Rel := by - ext (a b) + ext a b rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply] constructor · rintro ⟨a, rfl : a = 1, b, hb, rfl⟩ @@ -105,7 +105,7 @@ theorem bot_rel_eq_leftRel (H : Subgroup G) : theorem rel_bot_eq_right_group_rel (H : Subgroup G) : (setoid ↑H ↑(⊥ : Subgroup G)).Rel = (QuotientGroup.rightRel H).Rel := by - ext (a b) + ext a b rw [rel_iff, Setoid.Rel, QuotientGroup.rightRel_apply] constructor · rintro ⟨b, hb, a, rfl : a = 1, rfl⟩ diff --git a/Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean b/Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean index 6f3e66df85a35..ba0aa7bfcbabc 100644 --- a/Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean +++ b/Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean @@ -60,7 +60,7 @@ theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom (x : X) : @[simp] theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup : toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ) := by - ext (x y); simp only [AddMonoidHom.id_comp] + ext x y; simp only [AddMonoidHom.id_comp] rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom] simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply, one_smul, lift.of, AddMonoidHom.flip_apply, smulAddHom_apply, AddMonoidHom.id_apply] diff --git a/Mathlib/GroupTheory/FreeProduct.lean b/Mathlib/GroupTheory/FreeProduct.lean index 678e028648e8c..c2e36f91e16b3 100644 --- a/Mathlib/GroupTheory/FreeProduct.lean +++ b/Mathlib/GroupTheory/FreeProduct.lean @@ -155,7 +155,7 @@ def lift : (∀ i, M i →* N) ≃ (FreeProduct M →* N) where invFun f i := f.comp of left_inv := by intro fi - ext (i x) + ext i x rw [MonoidHom.comp_apply, of_apply, Con.lift_mk', FreeMonoid.lift_eval_of] right_inv := by intro f diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean index 93991f3d292a9..10fd7b51248b5 100644 --- a/Mathlib/GroupTheory/Perm/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Basic.lean @@ -270,7 +270,7 @@ def sigmaCongrRightHom {α : Type _} (β : α → Type _) : (∀ a, Perm (β a)) theorem sigmaCongrRightHom_injective {α : Type _} {β : α → Type _} : Function.Injective (sigmaCongrRightHom β) := by intro x y h - ext (a b) + ext a b simpa using Equiv.congr_fun h ⟨a, b⟩ #align equiv.perm.sigma_congr_right_hom_injective Equiv.Perm.sigmaCongrRightHom_injective diff --git a/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean b/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean index 018e433c7a732..0191caf23d701 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean @@ -50,7 +50,7 @@ theorem toMatrix_apply {ι' : Type _} (q : ι' → P) (i : ι') (j : ι) : @[simp] theorem toMatrix_self [DecidableEq ι] : b.toMatrix b = (1 : Matrix ι ι k) := by - ext (i j) + ext i j rw [toMatrix_apply, coord_apply, Matrix.one_eq_pi_single, Pi.single_apply] #align affine_basis.to_matrix_self AffineBasis.toMatrix_self @@ -121,7 +121,7 @@ theorem toMatrix_vecMul_coords (x : P) : (b.toMatrix b₂).vecMul (b₂.coords x variable [DecidableEq ι] theorem toMatrix_mul_toMatrix : b.toMatrix b₂ ⬝ b₂.toMatrix b = 1 := by - ext (l m) + ext l m change (b₂.toMatrix b).vecMul (b.coords (b₂ l)) m = _ rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self] #align affine_basis.to_matrix_mul_to_matrix AffineBasis.toMatrix_mul_toMatrix diff --git a/Mathlib/LinearAlgebra/AffineSpace/Slope.lean b/Mathlib/LinearAlgebra/AffineSpace/Slope.lean index 2c8dbd21185ed..8c82fe1090ed2 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Slope.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Slope.lean @@ -68,7 +68,7 @@ theorem sub_smul_slope_vadd (f : k → PE) (a b : k) : (b - a) • slope f a b + @[simp] theorem slope_vadd_const (f : k → E) (c : PE) : (slope fun x => f x +ᵥ c) = slope f := by - ext (a b) + ext a b simp only [slope, vadd_vsub_vadd_cancel_right, vsub_eq_sub] #align slope_vadd_const slope_vadd_const diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean index 66c9ee2ae0dd8..baf9a8e5263ac 100644 --- a/Mathlib/LinearAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/Basic.lean @@ -2387,7 +2387,7 @@ theorem conj_comp (e : M ≃ₗ[R] M₂) (f g : Module.End R M) : theorem conj_trans (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : e₁.conj.trans e₂.conj = (e₁.trans e₂).conj := by - ext (f x) + ext f x rfl #align linear_equiv.conj_trans LinearEquiv.conj_trans diff --git a/Mathlib/LinearAlgebra/BilinearMap.lean b/Mathlib/LinearAlgebra/BilinearMap.lean index 87a4493b15a56..f26ba67ae4890 100644 --- a/Mathlib/LinearAlgebra/BilinearMap.lean +++ b/Mathlib/LinearAlgebra/BilinearMap.lean @@ -363,7 +363,7 @@ theorem compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Q f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂ := by constructor <;> intro h · -- B₁.comp l r = B₂.comp l r → B₁ = B₂ - ext (x y) + ext x y cases' hₗ x with x' hx subst hx cases' hᵣ y with y' hy diff --git a/Mathlib/LinearAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/Contraction.lean index af4018d73e7a4..1bc9c26ecebe1 100644 --- a/Mathlib/LinearAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/Contraction.lean @@ -89,7 +89,7 @@ theorem dualTensorHom_apply (f : Module.Dual R M) (m : M) (n : N) : theorem transpose_dualTensorHom (f : Module.Dual R M) (m : M) : Dual.transpose (R := R) (dualTensorHom R M M (f ⊗ₜ m)) = dualTensorHom R _ _ (Dual.eval R M m ⊗ₜ f) := by - ext (f' m') + ext f' m' simp only [Dual.transpose_apply, coe_comp, Function.comp_apply, dualTensorHom_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, Algebra.id.smul_eq_mul, Dual.eval_apply, LinearMap.smul_apply] @@ -117,7 +117,7 @@ theorem zero_prodMap_dualTensorHom (g : Module.Dual R N) (q : Q) : theorem map_dualTensorHom (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) : TensorProduct.map (dualTensorHom R M P (f ⊗ₜ[R] p)) (dualTensorHom R N Q (g ⊗ₜ[R] q)) = dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) (dualDistrib R M N (f ⊗ₜ g) ⊗ₜ[R] p ⊗ₜ[R] q) := by - ext (m n) + ext m n simp only [compr₂_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply, ← smul_tmul_smul] #align map_dual_tensor_hom map_dualTensorHom @@ -137,7 +137,7 @@ single one and zeros elsewhere -/ theorem toMatrix_dualTensorHom {m : Type _} {n : Type _} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (bM : Basis m R M) (bN : Basis n R N) (j : m) (i : n) : toMatrix bM bN (dualTensorHom R M N (bM.coord j ⊗ₜ bN i)) = stdBasisMatrix i j 1 := by - ext (i' j') + ext i' j' by_cases hij : i = i' ∧ j = j' <;> simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij] rw [and_iff_not_or_not, Classical.not_not] at hij @@ -165,12 +165,12 @@ noncomputable def dualTensorHomEquivOfBasis : Module.Dual R M ⊗[R] N ≃ₗ[R] LinearEquiv.ofLinear (dualTensorHom R M N) (∑ i, TensorProduct.mk R _ N (b.dualBasis i) ∘ₗ (LinearMap.applyₗ (R := R) (b i))) (by - ext (f m) + ext f m simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, id.def, Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, Basis.coord_apply, ← f.map_smul, (dualTensorHom R M N).map_sum, ← f.map_sum, b.sum_repr]) (by - ext (f m) + ext f m simp only [applyₗ_apply_apply, coeFn_sum, dualTensorHom_apply, mk_apply, id_coe, id.def, Fintype.sum_apply, Function.comp_apply, Basis.coe_dualBasis, coe_comp, compr₂_apply, tmul_smul, smul_tmul', ← sum_tmul, Basis.sum_dual_apply_smul_coord]) @@ -262,7 +262,7 @@ theorem lTensorHomEquivHomLTensor_toLinearMap : let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q) have h : Function.Surjective e.toLinearMap := e.surjective refine' (cancel_right h).1 _ - ext (f q m) + ext f q m dsimp [lTensorHomEquivHomLTensor] simp only [lTensorHomEquivHomLTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_tmul, LinearEquiv.coe_coe, @@ -277,7 +277,7 @@ theorem rTensorHomEquivHomRTensor_toLinearMap : let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q) have h : Function.Surjective e.toLinearMap := e.surjective refine' (cancel_right h).1 _ - ext (f p q m) + ext f p q m simp only [rTensorHomEquivHomRTensor, dualTensorHomEquiv, compr₂_apply, mk_apply, coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply, map_tmul, LinearEquiv.coe_coe, dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply, congr_tmul, @@ -314,7 +314,7 @@ noncomputable def homTensorHomEquiv : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) ≃ @[simp] theorem homTensorHomEquiv_toLinearMap : (homTensorHomEquiv R M N P Q).toLinearMap = homTensorHomMap R M N P Q := by - ext (m n) + ext m n simp only [homTensorHomEquiv, compr₂_apply, mk_apply, LinearEquiv.coe_toLinearMap, LinearEquiv.trans_apply, lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm, LinearEquiv.refl_apply, rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply, diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index 467829dede75d..3e9a1af14d721 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -555,7 +555,7 @@ theorem is_basis_iff_det {v : ι → M} : set v' := Basis.mk hli hspan.ge rw [e.det_apply] convert LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2 - ext (i j) + ext i j simp · intro h rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h @@ -610,7 +610,7 @@ theorem Basis.det_comp_basis [Module A M'] (b : Basis ι A M) (b' : Basis ι A M b'.det (f ∘ b) = LinearMap.det (f ∘ₗ (b'.equiv b (Equiv.refl ι) : M' →ₗ[A] M)) := by rw [Basis.det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul, LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one] - congr 1; ext (i j) + congr 1; ext i j rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply] #align basis.det_comp_basis Basis.det_comp_basis diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean index d5d4e76d53c43..95b64d61bb379 100644 --- a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean @@ -91,7 +91,7 @@ protected def directSum : DirectSum.lof R (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)) (DirectSum.toModule R _ _ fun i => map (DirectSum.lof R _ _ _) (DirectSum.lof R _ _ _)) _ _ <;> - [ext (⟨i₁, i₂⟩x₁ x₂) : 4, ext (i₁ i₂ x₁ x₂) : 5] + [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5] repeat' first |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof] @@ -114,7 +114,7 @@ protected def directSum : (N := (⨁ i₁, M₁ i₁) ⊗[R] ⨁ i₂, M₂ i₂) (φ := fun i : ι₁ × ι₂ => map (DirectSum.lof R _ M₁ i.1) (DirectSum.lof R _ M₂ i.2))) _ _ <;> - [ext (⟨i₁, i₂⟩x₁ x₂) : 4, ext (i₁ i₂ x₁ x₂) : 5] + [ext ⟨i₁, i₂⟩ x₁ x₂ : 4, ext i₁ i₂ x₁ x₂ : 5] repeat' first |rw [compr₂_apply]|rw [comp_apply]|rw [id_apply]|rw [mk_apply]|rw [DirectSum.toModule_lof] diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index d722e82aef680..8bbbed813031f 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -445,7 +445,7 @@ theorem dualBasis_apply (i : ι) (m : M) : b.dualBasis i m = b.repr m i := @[simp] theorem coe_dualBasis : ⇑b.dualBasis = b.coord := by - ext (i x) + ext i x apply dualBasis_apply #align basis.coe_dual_basis Basis.coe_dualBasis @@ -1028,7 +1028,7 @@ theorem dualLift_of_mem {φ : Module.Dual K W} {w : V} (hw : w ∈ W) : W.dualLi @[simp] theorem dualRestrict_comp_dualLift (W : Subspace K V) : W.dualRestrict.comp W.dualLift = 1 := by - ext (φ x) + ext φ x simp #align subspace.dual_restrict_comp_dual_lift Subspace.dualRestrict_comp_dualLift @@ -1303,7 +1303,7 @@ theorem range_dualMap_eq_dualAnnihilator_ker_of_surjective (f : M →ₗ[R] M') · rw [LinearMap.range_comp_of_range_eq_top] apply LinearEquiv.range · apply congr_arg - ext (φ x) + ext φ x simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, LinearMap.dualMap_apply, LinearEquiv.dualMap_apply, mkQ_apply, LinearMap.quotKerEquivOfSurjective, LinearEquiv.trans_symm, LinearEquiv.trans_apply, LinearEquiv.ofTop_symm_apply, diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index b0bb60d83b9ba..68af8a98f8de1 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -197,7 +197,7 @@ theorem eigenspaces_independent (f : End K V) : CompleteLattice.Independent f.ei _ = 0 := by rw [hl, g.map_zero] · exact Dfinsupp.sum_mapRange_index.linearMap · congr - ext (μ v) + ext μ v simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.smul_apply, LinearMap.id_coe, id.def, sub_smul, Submodule.subtype_apply, Submodule.coe_sub, Submodule.coe_smul_of_tower, LinearMap.sub_apply, mem_eigenspace_iff.1 v.prop, algebraMap_end_apply] diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 85298cefd60e5..368a3cf555278 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -254,7 +254,7 @@ end theorem restrictDom_comp_subtype (s : Set α) : (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id := by - ext (l a) + ext l a by_cases h : a ∈ s <;> simp [h] exact ((mem_supported' R l.1).1 l.2 a h).symm #align finsupp.restrict_dom_comp_subtype Finsupp.restrictDom_comp_subtype diff --git a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean index 313571fe6bffd..c8c913e67f105 100644 --- a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean +++ b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean @@ -147,7 +147,7 @@ theorem cramer_subsingleton_apply [Subsingleton n] (A : Matrix n n α) (b : n #align matrix.cramer_subsingleton_apply Matrix.cramer_subsingleton_apply theorem cramer_zero [Nontrivial n] : cramer (0 : Matrix n n α) = 0 := by - ext (i j) + ext i j obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j apply det_eq_zero_of_column_eq_zero j' intro j'' @@ -220,7 +220,7 @@ theorem adjugate_apply (A : Matrix n n α) (i j : n) : #align matrix.adjugate_apply Matrix.adjugate_apply theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ := by - ext (i j) + ext i j rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose] rw [det_apply', det_apply'] apply Finset.sum_congr rfl @@ -252,7 +252,7 @@ theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ @[simp] theorem adjugate_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m α) : adjugate (A.submatrix e e) = (adjugate A).submatrix e e := by - ext (i j) + ext i j rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e, updateRow_submatrix_equiv] -- Porting note: added @@ -290,7 +290,7 @@ theorem mul_adjugate_apply (A : Matrix n n α) (i j k) : #align matrix.mul_adjugate_apply Matrix.mul_adjugate_apply theorem mul_adjugate (A : Matrix n n α) : A ⬝ adjugate A = A.det • (1 : Matrix n n α) := by - ext (i j) + ext i j rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole] simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm] #align matrix.mul_adjugate Matrix.mul_adjugate @@ -317,7 +317,7 @@ theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A.mulVec (cramer A b) #align matrix.mul_vec_cramer Matrix.mulVec_cramer theorem adjugate_subsingleton [Subsingleton n] (A : Matrix n n α) : adjugate A = 1 := by - ext (i j) + ext i j simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i] #align matrix.adjugate_subsingleton Matrix.adjugate_subsingleton @@ -329,7 +329,7 @@ theorem adjugate_eq_one_of_card_eq_one {A : Matrix n n α} (h : Fintype.card n = @[simp] theorem adjugate_zero [Nontrivial n] : adjugate (0 : Matrix n n α) = 0 := by - ext (i j) + ext i j obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j apply det_eq_zero_of_column_eq_zero j' intro j'' @@ -360,7 +360,7 @@ theorem adjugate_diagonal (v : n → α) : theorem _root_.RingHom.map_adjugate {R S : Type _} [CommRing R] [CommRing S] (f : R →+* S) (M : Matrix n n R) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) := by - ext (i k) + ext i k have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by rw [← f.map_one] exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R) @@ -405,7 +405,7 @@ theorem adjugate_fin_one (A : Matrix (Fin 1) (Fin 1) α) : adjugate A = 1 := theorem adjugate_fin_two (A : Matrix (Fin 2) (Fin 2) α) : adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0] := by - ext (i j) + ext i j rw [adjugate_apply, det_fin_two] fin_cases i <;> fin_cases j <;> simp [one_mul, Fin.one_eq_zero_iff, Pi.single_eq_same, MulZeroClass.mul_zero, sub_zero, diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean index 0389739703436..5a9ed03f0825e 100644 --- a/Mathlib/LinearAlgebra/Matrix/Basis.lean +++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean @@ -79,20 +79,20 @@ theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) -- TODO (maybe) Adjust the definition of `Basis.toMatrix` to eliminate the transpose. theorem coePiBasisFun.toMatrix_eq_transpose [Fintype ι] : ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose := by - ext (M i j) + ext M i j rfl #align basis.coe_pi_basis_fun.to_matrix_eq_transpose Basis.coePiBasisFun.toMatrix_eq_transpose @[simp] theorem toMatrix_self [DecidableEq ι] : e.toMatrix e = 1 := by unfold Basis.toMatrix - ext (i j) + ext i j simp [Basis.equivFun, Matrix.one_apply, Finsupp.single_apply, eq_comm] #align basis.to_matrix_self Basis.toMatrix_self theorem toMatrix_update [DecidableEq ι'] (x : M) : e.toMatrix (Function.update v j x) = Matrix.updateColumn (e.toMatrix v) j (e.repr x) := by - ext (i' k) + ext i' k rw [Basis.toMatrix, Matrix.updateColumn_apply, e.toMatrix_apply] split_ifs with h · rw [h, update_same j x v] @@ -103,7 +103,7 @@ theorem toMatrix_update [DecidableEq ι'] (x : M) : @[simp] theorem toMatrix_unitsSMul [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ι → R₂ˣ) : e.toMatrix (e.unitsSMul w) = diagonal ((↑) ∘ w) := by - ext (i j) + ext i j by_cases h : i = j · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def] · simp [h, toMatrix_apply, unitsSMul_apply, Units.smul_def, Ne.symm h] @@ -139,13 +139,13 @@ and matrices, making the matrix whose columns are the vectors `v i` written in t def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix ι ι R where toFun := e.toMatrix map_add' v w := by - ext (i j) + ext i j change _ = _ + _ rw [e.toMatrix_apply, Pi.add_apply, LinearEquiv.map_add] rfl map_smul' := by intro c v - ext (i j) + ext i j dsimp only [] rw [e.toMatrix_apply, Pi.smul_apply, LinearEquiv.map_smul] rfl @@ -156,7 +156,7 @@ def toMatrixEquiv [Fintype ι] (e : Basis ι R M) : (ι → M) ≃ₗ[R] Matrix exact e.sum_toMatrix_smul_self v j right_inv := by intro m - ext (k l) + ext k l simp only [e.toMatrix_apply, ← e.equivFun_apply, ← e.equivFun_symm_apply, LinearEquiv.apply_symm_apply] #align basis.to_matrix_equiv Basis.toMatrixEquiv @@ -217,7 +217,7 @@ theorem basis_toMatrix_basisFun_mul (b : Basis ι R (ι → R)) (A : Matrix ι b.toMatrix (Pi.basisFun R ι) ⬝ A = of fun i j => b.repr (Aᵀ j) i := by classical simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin'] - ext (i j) + ext i j rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply, Matrix.mulVec_stdBasis_apply, Matrix.of_apply] #align basis_to_matrix_basis_fun_mul basis_toMatrix_basisFun_mul @@ -248,7 +248,7 @@ theorem Basis.toMatrix_mul_toMatrix {ι'' : Type _} [Fintype ι'] (b'' : ι'' haveI := Classical.decEq ι haveI := Classical.decEq ι' haveI := Classical.decEq ι'' - ext (i j) + ext i j simp only [Matrix.mul_apply, Basis.toMatrix_apply, Basis.sum_repr_mul_repr] #align basis.to_matrix_mul_to_matrix Basis.toMatrix_mul_toMatrix diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean index c2b227d41aa46..cefcde4119bfc 100644 --- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean @@ -145,7 +145,7 @@ def BilinForm.toMatrix' : BilinForm R₂ (n → R₂) ≃ₗ[R₂] Matrix n n R invFun := Matrix.toBilin'Aux left_inv := fun B ↦ by convert toBilin'Aux_toMatrixAux B right_inv := fun M => by - ext (i j) + ext i j simp only [toFun_eq_coe, BilinForm.toMatrixAux_apply, Matrix.toBilin'Aux_stdBasis] } #align bilin_form.to_matrix' BilinForm.toMatrix' @@ -224,7 +224,7 @@ theorem BilinForm.toMatrix'_apply (B : BilinForm R₂ (n → R₂)) (i j : n) : theorem BilinForm.toMatrix'_comp (B : BilinForm R₂ (n → R₂)) (l r : (o → R₂) →ₗ[R₂] n → R₂) : BilinForm.toMatrix' (B.comp l r) = (LinearMap.toMatrix' l)ᵀ ⬝ BilinForm.toMatrix' B ⬝ LinearMap.toMatrix' r := by - ext (i j) + ext i j simp only [BilinForm.toMatrix'_apply, BilinForm.comp_apply, transpose_apply, Matrix.mul_apply, LinearMap.toMatrix', LinearEquiv.coe_mk, sum_mul] rw [sum_comm] @@ -365,7 +365,7 @@ variable [DecidableEq o] theorem BilinForm.toMatrix_comp (B : BilinForm R₂ M₂) (l r : M₂' →ₗ[R₂] M₂) : BilinForm.toMatrix c (B.comp l r) = (LinearMap.toMatrix c b l)ᵀ ⬝ BilinForm.toMatrix b B ⬝ LinearMap.toMatrix c b r := by - ext (i j) + ext i j simp only [BilinForm.toMatrix_apply, BilinForm.comp_apply, transpose_apply, Matrix.mul_apply, LinearMap.toMatrix', LinearEquiv.coe_mk, sum_mul] rw [sum_comm] diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean index 111e6d05d79f4..437b293514d68 100644 --- a/Mathlib/LinearAlgebra/Matrix/Block.lean +++ b/Mathlib/LinearAlgebra/Matrix/Block.lean @@ -263,7 +263,7 @@ theorem BlockTriangular.toBlock_inverse_mul_toBlock_eq_one [LinearOrder α] [Inv 1 := by rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self] have h_zero : M.toBlock (fun i => ¬p i) p = 0 := by - ext (i j) + ext i j simpa using hM (lt_of_lt_of_le j.2 (le_of_not_lt i.2)) simpa [h_zero] using h_sum #align matrix.block_triangular.to_block_inverse_mul_to_block_eq_one Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one @@ -295,7 +295,7 @@ theorem toBlock_inverse_eq_zero [LinearOrder α] [Invertible M] (hM : BlockTrian rw [disjoint_iff_inf_le] exact fun i h => h.1 h.2 have h_zero : M.toBlock q p = 0 := by - ext (i j) + ext i j simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_lt i.2) have h_mul_eq_zero : M⁻¹.toBlock q p ⬝ M.toBlock p p = 0 := by simpa [h_zero] using h_sum haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k diff --git a/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean index 262dada71e35b..e5252dc36ef51 100644 --- a/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean @@ -71,7 +71,7 @@ theorem charmatrix_apply_ne (M : Matrix n n R) (i j : n) (h : i ≠ j) : #align charmatrix_apply_ne charmatrix_apply_ne theorem matPolyEquiv_charmatrix (M : Matrix n n R) : matPolyEquiv (charmatrix M) = X - C M := by - ext (k i j) + ext k i j simp only [matPolyEquiv_coeff_apply, coeff_sub, Pi.sub_apply] by_cases h : i = j · subst h @@ -84,7 +84,7 @@ theorem matPolyEquiv_charmatrix (M : Matrix n n R) : matPolyEquiv (charmatrix M) theorem charmatrix_reindex {m : Type v} [DecidableEq m] [Fintype m] (e : n ≃ m) (M : Matrix n n R) : charmatrix (reindex e e M) = reindex e e (charmatrix M) := by - ext (i j x) + ext i j x by_cases h : i = j all_goals simp [h] #align charmatrix_reindex charmatrix_reindex diff --git a/Mathlib/LinearAlgebra/Matrix/Circulant.lean b/Mathlib/LinearAlgebra/Matrix/Circulant.lean index 65ded26472d4b..669cb2f7b11ff 100644 --- a/Mathlib/LinearAlgebra/Matrix/Circulant.lean +++ b/Mathlib/LinearAlgebra/Matrix/Circulant.lean @@ -127,7 +127,7 @@ theorem circulant_sub [Sub α] [Sub n] (v w : n → α) : the circulant matrix generated by `mulVec (circulant v) w`. -/ theorem circulant_mul [Semiring α] [Fintype n] [AddGroup n] (v w : n → α) : circulant v ⬝ circulant w = circulant (mulVec (circulant v) w) := by - ext (i j) + ext i j simp only [mul_apply, mulVec, circulant_apply, dotProduct] refine' Fintype.sum_equiv (Equiv.subRight j) _ _ _ intro x @@ -143,7 +143,7 @@ theorem Fin.circulant_mul [Semiring α] : /-- Multiplication of circulant matrices commutes when the elements do. -/ theorem circulant_mul_comm [CommSemigroup α] [AddCommMonoid α] [Fintype n] [AddCommGroup n] (v w : n → α) : circulant v ⬝ circulant w = circulant w ⬝ circulant v := by - ext (i j) + ext i j simp only [mul_apply, circulant_apply, mul_comm] refine' Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ _ intro x @@ -166,14 +166,14 @@ theorem circulant_smul [Sub n] [SMul R α] (k : R) (v : n → α) : @[simp] theorem circulant_single_one (α n) [Zero α] [One α] [DecidableEq n] [AddGroup n] : circulant (Pi.single 0 1 : n → α) = (1 : Matrix n n α) := by - ext (i j) + ext i j simp [one_apply, Pi.single_apply, sub_eq_zero] #align matrix.circulant_single_one Matrix.circulant_single_one @[simp] theorem circulant_single (n) [Semiring α] [DecidableEq n] [AddGroup n] [Fintype n] (a : α) : circulant (Pi.single 0 a : n → α) = scalar n a := by - ext (i j) + ext i j simp [Pi.single_apply, one_apply, sub_eq_zero] #align matrix.circulant_single Matrix.circulant_single diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant.lean b/Mathlib/LinearAlgebra/Matrix/Determinant.lean index 7dbaf1bac2f12..7c691556a4358 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant.lean @@ -481,7 +481,7 @@ theorem det_eq_of_forall_row_eq_smul_add_const_aux {A B : Matrix n n R} {s : Fin contrapose! hs simp [hs] congr - ext (i j) + ext i j rw [A_eq, this, MulZeroClass.zero_mul, add_zero] | @insert i s _hi ih => intro c hs k hk A_eq @@ -520,12 +520,12 @@ theorem det_eq_of_forall_row_eq_smul_add_pred_aux {n : ℕ} (k : Fin (n + 1)) : det M = det N := by refine' Fin.induction _ (fun k ih => _) k <;> intro c hc M N h0 hsucc · congr - ext (i j) + ext i j refine' Fin.cases (h0 j) (fun i => _) i rw [hsucc, hc i (Fin.succ_pos _), MulZeroClass.zero_mul, add_zero] set M' := updateRow M k.succ (N k.succ) with hM' have hM : M = updateRow M' k.succ (M' k.succ + c k • M (Fin.castSucc k)) := by - ext (i j) + ext i j by_cases hi : i = k.succ · simp [hi, hM', hsucc, updateRow_self] rw [updateRow_ne hi, hM', updateRow_ne hi] @@ -601,7 +601,7 @@ theorem det_blockDiagonal {o : Type _} [Fintype o] [DecidableEq o] (M : o → Ma simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq, prodCongrLeft_apply] · intro σ σ' _ _ eq - ext (x hx k) + ext x hx k simp only at eq have : ∀ k x, @@ -768,7 +768,7 @@ theorem det_succ_row {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin rw [mul_assoc, Matrix.submatrix, Matrix.submatrix] congr · rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_zero] - · ext (i' j') + · ext i' j' rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_succ] #align matrix.det_succ_row Matrix.det_succ_row diff --git a/Mathlib/LinearAlgebra/Matrix/Dual.lean b/Mathlib/LinearAlgebra/Matrix/Dual.lean index 8996e637478be..daf34a88ad1e3 100644 --- a/Mathlib/LinearAlgebra/Matrix/Dual.lean +++ b/Mathlib/LinearAlgebra/Matrix/Dual.lean @@ -35,7 +35,7 @@ variable {K V₁ V₂ ι₁ ι₂ : Type _} [Field K] [AddCommGroup V₁] [Modul theorem LinearMap.toMatrix_transpose (u : V₁ →ₗ[K] V₂) : LinearMap.toMatrix B₂.dualBasis B₁.dualBasis (Module.Dual.transpose (R := K) u) = (LinearMap.toMatrix B₁ B₂ u)ᵀ := by - ext (i j) + ext i j simp only [LinearMap.toMatrix_apply, Module.Dual.transpose_apply, B₁.dualBasis_repr, B₂.dualBasis_apply, Matrix.transpose_apply, LinearMap.comp_apply] #align linear_map.to_matrix_transpose LinearMap.toMatrix_transpose diff --git a/Mathlib/LinearAlgebra/Matrix/Hermitian.lean b/Mathlib/LinearAlgebra/Matrix/Hermitian.lean index f1b3319b3a1ee..22a0b7f2dc8ec 100644 --- a/Mathlib/LinearAlgebra/Matrix/Hermitian.lean +++ b/Mathlib/LinearAlgebra/Matrix/Hermitian.lean @@ -54,7 +54,7 @@ protected theorem IsHermitian.isSelfAdjoint {A : Matrix n n α} (h : A.IsHermiti -- @[ext] -- Porting note: incorrect ext, not a structure or a lemma proving x = y theorem IsHermitian.ext {A : Matrix n n α} : (∀ i j, star (A j i) = A i j) → A.IsHermitian := by - intro h; ext (i j); exact h i j + intro h; ext i j; exact h i j #align matrix.is_hermitian.ext Matrix.IsHermitian.ext theorem IsHermitian.apply {A : Matrix n n α} (h : A.IsHermitian) (i j : n) : star (A j i) = A i j := @@ -280,7 +280,7 @@ theorem isHermitian_iff_isSymmetric [Fintype n] [DecidableEq n] {A : Matrix n n · rintro (h : Aᴴ = A) x y rw [h] · intro h - ext (i j) + ext i j simpa only [(Pi.single_star i 1).symm, ← star_mulVec, mul_one, dotProduct_single, single_vecMul, star_one, one_mul] using h (Pi.single i 1) (Pi.single j 1) #align matrix.is_hermitian_iff_is_symmetric Matrix.isHermitian_iff_isSymmetric diff --git a/Mathlib/LinearAlgebra/Matrix/IsDiag.lean b/Mathlib/LinearAlgebra/Matrix/IsDiag.lean index 6bc65b9734601..9a38b5044de1b 100644 --- a/Mathlib/LinearAlgebra/Matrix/IsDiag.lean +++ b/Mathlib/LinearAlgebra/Matrix/IsDiag.lean @@ -153,7 +153,7 @@ theorem IsDiag.kronecker [MulZeroClass α] {A : Matrix m m α} {B : Matrix n n #align matrix.is_diag.kronecker Matrix.IsDiag.kronecker theorem IsDiag.isSymm [Zero α] {A : Matrix n n α} (h : A.IsDiag) : A.IsSymm := by - ext (i j) + ext i j by_cases g : i = j; · rw [g, transpose_apply] simp [h g, h (Ne.symm g)] #align matrix.is_diag.is_symm Matrix.IsDiag.isSymm diff --git a/Mathlib/LinearAlgebra/Matrix/LDL.lean b/Mathlib/LinearAlgebra/Matrix/LDL.lean index eb173b83f1262..77ec1d0fe509d 100644 --- a/Mathlib/LinearAlgebra/Matrix/LDL.lean +++ b/Mathlib/LinearAlgebra/Matrix/LDL.lean @@ -64,7 +64,7 @@ theorem LDL.lowerInv_eq_gramSchmidtBasis : (Pi.basisFun 𝕜 n)))ᵀ := by letI := NormedAddCommGroup.ofMatrix hS.transpose letI := InnerProductSpace.ofMatrix hS.transpose - ext (i j) + ext i j rw [LDL.lowerInv, Basis.coePiBasisFun.toMatrix_eq_transpose, coe_gramSchmidtBasis] rfl #align LDL.lower_inv_eq_gram_schmidt_basis LDL.lowerInv_eq_gramSchmidtBasis @@ -103,7 +103,7 @@ theorem LDL.lowerInv_triangular {i j : n} (hij : i < j) : LDL.lowerInv hS i j = /-- Inverse statement of **LDL decomposition**: we can conjugate a positive definite matrix by some lower triangular matrix and get a diagonal matrix. -/ theorem LDL.diag_eq_lowerInv_conj : LDL.diag hS = LDL.lowerInv hS ⬝ S ⬝ (LDL.lowerInv hS)ᴴ := by - ext (i j) + ext i j by_cases hij : i = j · simp only [diag, diagEntries, EuclideanSpace.inner_piLp_equiv_symm, star_star, hij, diagonal_apply_eq, Matrix.mul_assoc] diff --git a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean index 4ac3532d447f8..37eb30ce08779 100644 --- a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean +++ b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean @@ -136,7 +136,7 @@ theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux (f : Matrix n m R) : LinearMap.toMatrix₂Aux (fun i => LinearMap.stdBasis R₁ (fun _ => R₁) i 1) (fun j => LinearMap.stdBasis R₂ (fun _ => R₂) j 1) (f.toLinearMap₂'Aux σ₁ σ₂) = f := by - ext (i j) + ext i j simp_rw [LinearMap.toMatrix₂Aux_apply, Matrix.toLinearMap₂'Aux_stdBasis] #align matrix.to_matrix₂_aux_to_linear_map₂'_aux Matrix.toMatrix₂Aux_toLinearMap₂'Aux @@ -286,7 +286,7 @@ variable [DecidableEq n'] [DecidableEq m'] theorem LinearMap.toMatrix₂'_compl₁₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (l : (n' → R) →ₗ[R] n → R) (r : (m' → R) →ₗ[R] m → R) : toMatrix₂' (B.compl₁₂ l r) = (toMatrix' l)ᵀ ⬝ toMatrix₂' B ⬝ toMatrix' r := by - ext (i j) + ext i j simp only [LinearMap.toMatrix₂'_apply, LinearMap.compl₁₂_apply, transpose_apply, Matrix.mul_apply, LinearMap.toMatrix', LinearEquiv.coe_mk, sum_mul] rw [sum_comm] @@ -446,7 +446,7 @@ theorem LinearMap.toMatrix₂_compl₁₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (r : M₂' →ₗ[R] M₂) : LinearMap.toMatrix₂ b₁' b₂' (B.compl₁₂ l r) = (toMatrix b₁' b₁ l)ᵀ ⬝ LinearMap.toMatrix₂ b₁ b₂ B ⬝ toMatrix b₂' b₂ r := by - ext (i j) + ext i j simp only [LinearMap.toMatrix₂_apply, compl₁₂_apply, transpose_apply, Matrix.mul_apply, LinearMap.toMatrix_apply, LinearEquiv.coe_mk, sum_mul] rw [sum_comm] diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean index 662c14a476e6e..84cdf1c21ca69 100644 --- a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean @@ -309,7 +309,7 @@ theorem fin_two_induction (P : SL(2, R) → Prop) (g : SL(2, R)) : P g := by obtain ⟨m, hm⟩ := g convert h (m 0 0) (m 0 1) (m 1 0) (m 1 1) (by rwa [det_fin_two] at hm) - ext (i j); fin_cases i <;> fin_cases j <;> rfl + ext i j; fin_cases i <;> fin_cases j <;> rfl #align matrix.special_linear_group.fin_two_induction Matrix.SpecialLinearGroup.fin_two_induction theorem fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type _} [Field R] (g : SL(2, R)) diff --git a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean index 5aadc67b59a32..aed32437a639c 100644 --- a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean +++ b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean @@ -87,7 +87,7 @@ theorem eigenvectorMatrixInv_apply (i j : n) : #align matrix.is_hermitian.eigenvector_matrix_inv_apply Matrix.IsHermitian.eigenvectorMatrixInv_apply theorem conjTranspose_eigenvectorMatrixInv : hA.eigenvectorMatrixInvᴴ = hA.eigenvectorMatrix := by - ext (i j) + ext i j rw [conjTranspose_apply, eigenvectorMatrixInv_apply, eigenvectorMatrix_apply, star_star] #align matrix.is_hermitian.conj_transpose_eigenvector_matrix_inv Matrix.IsHermitian.conjTranspose_eigenvectorMatrixInv @@ -103,7 +103,7 @@ For the spectral theorem on linear maps, see theorem spectral_theorem : hA.eigenvectorMatrixInv ⬝ A = diagonal ((↑) ∘ hA.eigenvalues) ⬝ hA.eigenvectorMatrixInv := by rw [eigenvectorMatrixInv, PiLp.basis_toMatrix_basisFun_mul] - ext (i j) + ext i j have := isHermitian_iff_isSymmetric.1 hA convert this.eigenvectorBasis_apply_self_apply finrank_euclideanSpace (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i) using 1 diff --git a/Mathlib/LinearAlgebra/Matrix/ToLin.lean b/Mathlib/LinearAlgebra/Matrix/ToLin.lean index 61b3b913a02da..e1e180b946d55 100644 --- a/Mathlib/LinearAlgebra/Matrix/ToLin.lean +++ b/Mathlib/LinearAlgebra/Matrix/ToLin.lean @@ -115,17 +115,17 @@ def LinearMap.toMatrixRight' : ((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] toFun f i j := f (stdBasis R (fun _ => R) i 1) j invFun := Matrix.vecMulLinear right_inv M := by - ext (i j) + ext i j simp only [Matrix.vecMul_stdBasis, Matrix.vecMulLinear_apply] left_inv f := by apply (Pi.basisFun R m).ext intro j; ext i simp only [Pi.basisFun_apply, Matrix.vecMul_stdBasis, Matrix.vecMulLinear_apply] map_add' f g := by - ext (i j) + ext i j simp only [Pi.add_apply, LinearMap.add_apply, Matrix.add_apply] map_smul' c f := by - ext (i j) + ext i j simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply] #align linear_map.to_matrix_right' LinearMap.toMatrixRight' @@ -288,17 +288,17 @@ def LinearMap.toMatrix' : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R w toFun f := of fun i j => f (stdBasis R (fun _ => R) j 1) i invFun := Matrix.mulVecLin right_inv M := by - ext (i j) + ext i j simp only [Matrix.mulVec_stdBasis, Matrix.mulVecLin_apply, of_apply] left_inv f := by apply (Pi.basisFun R n).ext intro j; ext i simp only [Pi.basisFun_apply, Matrix.mulVec_stdBasis, Matrix.mulVecLin_apply, of_apply] map_add' f g := by - ext (i j) + ext i j simp only [Pi.add_apply, LinearMap.add_apply, of_apply, Matrix.add_apply] map_smul' c f := by - ext (i j) + ext i j simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, of_apply, Matrix.smul_apply] #align linear_map.to_matrix' LinearMap.toMatrix' @@ -620,7 +620,7 @@ theorem Matrix.toLin_self (M : Matrix m n R) (i : n) : /-- This will be a special case of `LinearMap.toMatrix_id_eq_basis_toMatrix`. -/ theorem LinearMap.toMatrix_id : LinearMap.toMatrix v₁ v₁ id = 1 := by - ext (i j) + ext i j simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm] #align linear_map.to_matrix_id LinearMap.toMatrix_id @@ -674,7 +674,7 @@ theorem LinearMap.toMatrix_mulVec_repr (f : M₁ →ₗ[R] M₂) (x : M₁) : theorem LinearMap.toMatrix_basis_equiv [Fintype l] [DecidableEq l] (b : Basis l R M₁) (b' : Basis l R M₂) : LinearMap.toMatrix b' b (b'.equiv b (Equiv.refl l) : M₂ →ₗ[R] M₁) = 1 := by - ext (i j) + ext i j simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm] #align linear_map.to_matrix_basis_equiv LinearMap.toMatrix_basis_equiv @@ -934,7 +934,7 @@ theorem smul_leftMulMatrix (x) (ik jk) : theorem smul_leftMulMatrix_algebraMap (x : S) : leftMulMatrix (b.smul c) (algebraMap _ _ x) = blockDiagonal fun _ => leftMulMatrix b x := by - ext (⟨i, k⟩⟨j, k'⟩) + ext ⟨i, k⟩ ⟨j, k'⟩ rw [smul_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply] split_ifs with h <;> simp only at h <;> simp [h] #align algebra.smul_left_mul_matrix_algebra_map Algebra.smul_leftMulMatrix_algebraMap diff --git a/Mathlib/LinearAlgebra/Matrix/Transvection.lean b/Mathlib/LinearAlgebra/Matrix/Transvection.lean index 9ca5c85396cb8..6b77ebab239ac 100644 --- a/Mathlib/LinearAlgebra/Matrix/Transvection.lean +++ b/Mathlib/LinearAlgebra/Matrix/Transvection.lean @@ -100,7 +100,7 @@ theorem updateRow_eq_transvection [Finite n] (c : R) : updateRow (1 : Matrix n n R) i ((1 : Matrix n n R) i + c • (1 : Matrix n n R) j) = transvection i j c := by cases nonempty_fintype n - ext (a b) + ext a b by_cases ha : i = a; by_cases hb : j = b · simp only [updateRow_self, transvection, ha, hb, Pi.add_apply, StdBasisMatrix.apply_same, one_apply_eq, Pi.smul_apply, mul_one, Algebra.id.smul_eq_mul, add_apply] @@ -255,7 +255,7 @@ def sumInl (t : TransvectionStruct n R) : TransvectionStruct (Sum n p) R where theorem toMatrix_sumInl (t : TransvectionStruct n R) : (t.sumInl p).toMatrix = fromBlocks t.toMatrix 0 0 1 := by cases t - ext (a b) + ext a b cases' a with a a <;> cases' b with b b · by_cases h : a = b <;> simp [TransvectionStruct.sumInl, transvection, h, stdBasisMatrix] · simp [TransvectionStruct.sumInl, transvection] @@ -299,7 +299,7 @@ variable [Fintype n] [Fintype p] theorem toMatrix_reindexEquiv (e : n ≃ p) (t : TransvectionStruct n R) : (t.reindexEquiv e).toMatrix = reindexAlgEquiv R e t.toMatrix := by rcases t with ⟨t_i, t_j, _⟩ - ext (a b) + ext a b simp only [reindexEquiv, transvection, mul_boole, Algebra.id.smul_eq_mul, toMatrix_mk, submatrix_apply, reindex_apply, DMatrix.add_apply, Pi.smul_apply, reindexAlgEquiv_apply] by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b <;> @@ -525,10 +525,10 @@ theorem isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow (hM : M (inr unit) (inr unit) ≠ 0) : IsTwoBlockDiagonal ((listTransvecCol M).prod ⬝ M ⬝ (listTransvecRow M).prod) := by constructor - · ext (i j) + · ext i j have : j = unit := by simp only [eq_iff_true_of_subsingleton] simp [toBlocks₁₂, this, listTransvecCol_mul_mul_listTransvecRow_last_row M hM] - · ext (i j) + · ext i j have : i = unit := by simp only [eq_iff_true_of_subsingleton] simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM] #align matrix.pivot.is_two_block_diagonal_list_transvec_col_mul_mul_list_transvec_row Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow @@ -654,7 +654,7 @@ theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux (n : Type) [F (L.map toMatrix).prod ⬝ M ⬝ (L'.map toMatrix).prod = diagonal D := by induction' hn : Fintype.card n with r IH generalizing n M · refine' ⟨List.nil, List.nil, fun _ => 1, _⟩ - ext (i j) + ext i j rw [Fintype.card_eq_zero_iff] at hn exact hn.elim' i · have e : n ≃ Sum (Fin r) Unit := by diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 9a95eb3471f99..c20b95869d3af 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -1273,7 +1273,7 @@ theorem MultilinearMap.curryLeft_apply (f : MultilinearMap R M M₂) (x : M 0) @[simp] theorem LinearMap.curry_uncurryLeft (f : M 0 →ₗ[R] MultilinearMap R (fun i : Fin n => M i.succ) M₂) : f.uncurryLeft.curryLeft = f := by - ext (m x) + ext m x simp only [tail_cons, LinearMap.uncurryLeft_apply, MultilinearMap.curryLeft_apply] rw [cons_zero] #align linear_map.curry_uncurry_left LinearMap.curry_uncurryLeft @@ -1390,7 +1390,7 @@ theorem MultilinearMap.curryRight_apply (f : MultilinearMap R M M₂) theorem MultilinearMap.curry_uncurryRight (f : MultilinearMap R (fun i : Fin n => M (castSucc i)) (M (last n) →ₗ[R] M₂)) : f.uncurryRight.curryRight = f := by - ext (m x) + ext m x simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply] rw [init_snoc] #align multilinear_map.curry_uncurry_right MultilinearMap.curry_uncurryRight diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean index adc0e141c6a43..ab79c4221e1a6 100644 --- a/Mathlib/LinearAlgebra/Pi.lean +++ b/Mathlib/LinearAlgebra/Pi.lean @@ -148,7 +148,7 @@ def lsum (S) [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] [Semir map_add' f g := by simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib] map_smul' c f := by simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply] left_inv f := by - ext (i x) + ext i x simp [apply_single] right_inv f := by ext x @@ -217,7 +217,7 @@ def iInfKerProjEquiv {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjo have : j ∉ I := fun hjI => hd.le_bot ⟨hjI, hjJ⟩ rw [dif_neg this, zero_apply] · simp only [pi_comp, comp_assoc, subtype_comp_codRestrict, proj_pi, Subtype.coe_prop] - ext (b⟨j, hj⟩) + ext b ⟨j, hj⟩ simp only [dif_pos, Function.comp_apply, Function.eval_apply, LinearMap.codRestrict_apply, LinearMap.coe_comp, LinearMap.coe_proj, LinearMap.pi_apply, Submodule.subtype_apply, Subtype.coe_prop] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 6d2b0e6071c89..90f95374938ad 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -998,7 +998,7 @@ theorem QuadraticForm.toMatrix'_smul (a : R₁) (Q : QuadraticForm R₁ (n → R #align quadratic_form.to_matrix'_smul QuadraticForm.toMatrix'_smul theorem QuadraticForm.isSymm_toMatrix' (Q : QuadraticForm R₁ (n → R₁)) : Q.toMatrix'.IsSymm := by - ext (i j) + ext i j rw [toMatrix', Matrix.transpose_apply, BilinForm.toMatrix'_apply, BilinForm.toMatrix'_apply, associated_isSymm] #align quadratic_form.is_symm_to_matrix' QuadraticForm.isSymm_toMatrix' diff --git a/Mathlib/LinearAlgebra/SesquilinearForm.lean b/Mathlib/LinearAlgebra/SesquilinearForm.lean index ff4ec9f407687..f8221810db6ba 100644 --- a/Mathlib/LinearAlgebra/SesquilinearForm.lean +++ b/Mathlib/LinearAlgebra/SesquilinearForm.lean @@ -437,7 +437,7 @@ variable {B B' f g} theorem isAdjointPair_iff_comp_eq_compl₂ : IsAdjointPair B B' f g ↔ B'.comp f = B.compl₂ g := by constructor <;> intro h - · ext (x y) + · ext x y rw [comp_apply, compl₂_apply] exact h x y · intro _ _ @@ -662,7 +662,7 @@ theorem separatingLeft_congr_iff : (e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R R)) B).SeparatingLeft ↔ B.SeparatingLeft := ⟨fun h ↦ by convert h.congr e₁.symm e₂.symm - ext (x y) + ext x y simp, SeparatingLeft.congr e₁ e₂⟩ #align linear_map.separating_left_congr_iff LinearMap.separatingLeft_congr_iff diff --git a/Mathlib/LinearAlgebra/StdBasis.lean b/Mathlib/LinearAlgebra/StdBasis.lean index 516b8ba4c4ea1..c7fc4c9024680 100644 --- a/Mathlib/LinearAlgebra/StdBasis.lean +++ b/Mathlib/LinearAlgebra/StdBasis.lean @@ -76,7 +76,7 @@ theorem stdBasis_ne (i j : ι) (h : j ≠ i) (b : φ i) : stdBasis R φ i b j = #align linear_map.std_basis_ne LinearMap.stdBasis_ne theorem stdBasis_eq_pi_diag (i : ι) : stdBasis R φ i = pi (diag i) := by - ext (x j) + ext x j -- Porting note: made types explicit convert (update_apply (R := R) (φ := φ) (ι := ι) 0 x i j _).symm rfl @@ -314,7 +314,7 @@ variable {n m} theorem stdBasis_eq_stdBasisMatrix (i : n) (j : m) [DecidableEq n] [DecidableEq m] : stdBasis R n m (i, j) = stdBasisMatrix i j (1 : R) := by -- Porting note: `simp` fails to apply `Pi.basis_apply` - ext (a b) + ext a b by_cases hi : i = a <;> by_cases hj : j = b · simp [stdBasis, hi, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, StdBasisMatrix.apply_same] diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean index ec6dedfe9c1aa..c4b7f20a7fb3a 100644 --- a/Mathlib/LinearAlgebra/TensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorPower.lean @@ -210,7 +210,7 @@ theorem mul_assoc {na nb nc} (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R have rhs_eq : ∀ a b c, rhs a b c = a ₜ* (b ₜ* c) := fun _ _ _ => rfl suffices : lhs = rhs exact LinearMap.congr_fun (LinearMap.congr_fun (LinearMap.congr_fun this a) b) c - ext (a b c) + ext a b c -- clean up simp only [LinearMap.compMultilinearMap_apply, lhs_eq, rhs_eq, tprod_mul_tprod, cast_tprod] congr with j diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean index bd6fb02947bb5..3a14bcc02bf93 100644 --- a/Mathlib/LinearAlgebra/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/TensorProduct.lean @@ -1015,11 +1015,11 @@ def lTensorHom : (N →ₗ[R] P) →ₗ[R] M ⊗[R] N →ₗ[R] M ⊗[R] P where def rTensorHom : (N →ₗ[R] P) →ₗ[R] N ⊗[R] M →ₗ[R] P ⊗[R] M where toFun f := f.rTensor M map_add' f g := by - ext (x y) + ext x y simp only [compr₂_apply, mk_apply, add_apply, rTensor_tmul, add_tmul] map_smul' r f := by dsimp - ext (x y) + ext x y simp only [compr₂_apply, mk_apply, smul_tmul, tmul_smul, smul_apply, rTensor_tmul] #align linear_map.rtensor_hom LinearMap.rTensorHom @@ -1064,7 +1064,7 @@ theorem rTensor_smul (r : R) (f : N →ₗ[R] P) : (r • f).rTensor M = r • f #align linear_map.rtensor_smul LinearMap.rTensor_smul theorem lTensor_comp : (g.comp f).lTensor M = (g.lTensor M).comp (f.lTensor M) := by - ext (m n) + ext m n simp only [compr₂_apply, mk_apply, comp_apply, lTensor_tmul] #align linear_map.ltensor_comp LinearMap.lTensor_comp @@ -1073,7 +1073,7 @@ theorem lTensor_comp_apply (x : M ⊗[R] N) : #align linear_map.ltensor_comp_apply LinearMap.lTensor_comp_apply theorem rTensor_comp : (g.comp f).rTensor M = (g.rTensor M).comp (f.rTensor M) := by - ext (m n) + ext m n simp only [compr₂_apply, mk_apply, comp_apply, rTensor_tmul] #align linear_map.rtensor_comp LinearMap.rTensor_comp diff --git a/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean index 59c9b36992068..cebfbbdae635e 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean @@ -50,7 +50,7 @@ open Matrix LinearMap theorem TensorProduct.toMatrix_map (f : M →ₗ[R] M') (g : N →ₗ[R] N') : toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') (TensorProduct.map f g) = toMatrix bM bM' f ⊗ₖ toMatrix bN bN' g := by - ext (⟨i, j⟩⟨i', j'⟩) + ext ⟨i, j⟩ ⟨i', j'⟩ simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply, TensorProduct.map_tmul, Basis.tensorProduct_repr_tmul_apply] #align tensor_product.to_matrix_map TensorProduct.toMatrix_map @@ -68,7 +68,7 @@ theorem Matrix.toLin_kronecker (A : Matrix ι' ι R) (B : Matrix κ' κ R) : theorem TensorProduct.toMatrix_comm : toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) (TensorProduct.comm R M N) = (1 : Matrix (ι × κ) (ι × κ) R).submatrix Prod.swap _root_.id := by - ext (⟨i, j⟩⟨i', j'⟩) + ext ⟨i, j⟩ ⟨i', j'⟩ simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul, Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Prod.swap_prod_mk, id.def, Basis.repr_self_apply, Matrix.one_apply, Prod.ext_iff, ite_and, @eq_comm _ i', @eq_comm _ j'] @@ -80,7 +80,7 @@ theorem TensorProduct.toMatrix_assoc : toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)) (TensorProduct.assoc R M N P) = (1 : Matrix (ι × κ × τ) (ι × κ × τ) R).submatrix _root_.id (Equiv.prodAssoc _ _ _) := by - ext (⟨i, j, k⟩⟨⟨i', j'⟩, k'⟩) + ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩ simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.assoc_tmul, Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Equiv.prodAssoc_apply, id.def, Basis.repr_self_apply, Matrix.one_apply, Prod.ext_iff, ite_and, diff --git a/Mathlib/LinearAlgebra/Trace.lean b/Mathlib/LinearAlgebra/Trace.lean index 5dc0299b75929..ac2fec0a6d66c 100644 --- a/Mathlib/LinearAlgebra/Trace.lean +++ b/Mathlib/LinearAlgebra/Trace.lean @@ -202,7 +202,7 @@ theorem trace_transpose : trace R (Module.Dual R M) ∘ₗ Module.Dual.transpose let e := dualTensorHomEquiv R M M have h : Function.Surjective e.toLinearMap := e.surjective refine' (cancel_right h).1 _ - ext (f m); simp + ext f m; simp #align linear_map.trace_transpose LinearMap.trace_transpose theorem trace_prodMap : @@ -241,7 +241,7 @@ theorem trace_tensorProduct : compr₂ (mapBilinear R M N M N) (trace R (M ⊗ N apply (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective) (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1 - ext (f m g n) + ext f m g n simp only [AlgebraTensorModule.curry_apply, toFun_eq_coe, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply, compr₂_apply, mapBilinear_apply, trace_eq_contract_apply, contractLeft_apply, lsmul_apply, Algebra.id.smul_eq_mul, @@ -253,7 +253,7 @@ theorem trace_comp_comm : apply (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective) (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1 - ext (g m f n) + ext g m f n simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, coe_restrictScalars, compl₁₂_apply, compr₂_apply, llcomp_apply', comp_dualTensorHom, map_smulₛₗ, RingHom.id_apply, trace_eq_contract_apply, contractLeft_apply, smul_eq_mul, mul_comm, flip_apply] diff --git a/Mathlib/LinearAlgebra/Vandermonde.lean b/Mathlib/LinearAlgebra/Vandermonde.lean index f1796b0bb26d6..c4787d0b2d574 100644 --- a/Mathlib/LinearAlgebra/Vandermonde.lean +++ b/Mathlib/LinearAlgebra/Vandermonde.lean @@ -52,7 +52,7 @@ theorem vandermonde_cons {n : ℕ} (v0 : R) (v : Fin n → R) : vandermonde (Fin.cons v0 v : Fin n.succ → R) = Fin.cons (fun (j : Fin n.succ) => v0 ^ (j : ℕ)) fun i => Fin.cons 1 fun j => v i * vandermonde v i j := by - ext (i j) + ext i j refine' Fin.cases (by simp) (fun i => _) i refine' Fin.cases (by simp) (fun j => _) j simp [pow_succ] @@ -102,7 +102,7 @@ theorem det_vandermonde {n : ℕ} (v : Fin n → R) : ∑ k in Finset.range (j + 1 : ℕ), v i.succ ^ k * v 0 ^ (j - k : ℕ) : Matrix _ _ R) := by congr - ext (i j) + ext i j rw [Fin.succAbove_zero, Matrix.cons_val_succ, Fin.val_succ, mul_comm] exact (geom_sum₂_mul (v i.succ) (v 0) (j + 1 : ℕ)).symm _ = diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean index 147841d148f00..0785976f6c0e9 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean @@ -392,7 +392,7 @@ theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionS let e : (ι → ℝ) ≃ᵐ (α → ℝ) × (β → ℝ) := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => ℝ) p have : (toLin' t.toMatrix : (ι → ℝ) → ι → ℝ) = e.symm ∘ F ∘ e := by cases t with | mk t_i t_j t_hij t_c => - ext (f k) + ext f k simp only [LinearEquiv.map_smul, dite_eq_ite, LinearMap.id_coe, ite_not, Algebra.id.smul_eq_mul, one_mul, dotProduct, stdBasisMatrix, MeasurableEquiv.piEquivPiSubtypeProd_symm_apply, id.def, transvection, Pi.add_apply, diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean index 73ac7d9d8e888..e11f6de195ce3 100644 --- a/Mathlib/Order/Hom/Basic.lean +++ b/Mathlib/Order/Hom/Basic.lean @@ -335,7 +335,7 @@ def curry : (α × β →o γ) ≃o (α →o β →o γ) where ext ⟨x, y⟩ rfl right_inv f := by - ext (x y) + ext x y rfl map_rel_iff' := by simp [le_def] #align order_hom.curry OrderHom.curry @@ -531,10 +531,10 @@ def piIso : (α →o ∀ i, π i) ≃o ∀ i, α →o π i where toFun f i := (Pi.evalOrderHom i).comp f invFun := pi left_inv f := by - ext (x i) + ext x i rfl right_inv f := by - ext (x i) + ext x i rfl map_rel_iff' := forall_swap #align order_hom.pi_iso OrderHom.piIso diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 9c6598e3a0a11..e2bd09fd57249 100644 --- a/Mathlib/Order/Lattice.lean +++ b/Mathlib/Order/Lattice.lean @@ -899,7 +899,7 @@ end LinearOrder theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableRel ((· ≤ ·) : α → α → Prop)] [IsTotal α (· ≤ ·)] : (· ⊔ ·) = (maxDefault : α → α → α) := by - ext (x y) + ext x y unfold maxDefault split_ifs with h' exacts [sup_of_le_right h', sup_of_le_left $ (total_of (· ≤ ·) x y).resolve_left h'] @@ -908,7 +908,7 @@ theorem sup_eq_maxDefault [SemilatticeSup α] [DecidableRel ((· ≤ ·) : α theorem inf_eq_minDefault [SemilatticeInf α] [DecidableRel ((· ≤ ·) : α → α → Prop)] [IsTotal α (· ≤ ·)] : (· ⊓ ·) = (minDefault : α → α → α) := by - ext (x y) + ext x y unfold minDefault split_ifs with h' exacts [inf_of_le_left h', inf_of_le_right $ (total_of (· ≤ ·) x y).resolve_left h'] diff --git a/Mathlib/Order/LocallyFinite.lean b/Mathlib/Order/LocallyFinite.lean index b8d724d82be22..b7b0be7256e4d 100644 --- a/Mathlib/Order/LocallyFinite.lean +++ b/Mathlib/Order/LocallyFinite.lean @@ -750,16 +750,16 @@ instance : Subsingleton (LocallyFiniteOrder α) := cases' h₁ with h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo h₁_finset_mem_Icc h₁_finset_mem_Ico h₁_finset_mem_Ioc h₁_finset_mem_Ioo have hIcc : h₀_finset_Icc = h₁_finset_Icc := by - ext (a b x) + ext a b x rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc] have hIco : h₀_finset_Ico = h₁_finset_Ico := by - ext (a b x) + ext a b x rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico] have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by - ext (a b x) + ext a b x rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc] have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by - ext (a b x) + ext a b x rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo] simp_rw [hIcc, hIco, hIoc, hIoo] diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean index 76f3e26ffae93..018eb8cc79ff5 100644 --- a/Mathlib/Order/RelIso/Basic.lean +++ b/Mathlib/Order/RelIso/Basic.lean @@ -331,7 +331,7 @@ def preimage (f : α ↪ β) (s : β → β → Prop) : f ⁻¹'o s ↪r s := #align rel_embedding.preimage RelEmbedding.preimage theorem eq_preimage (f : r ↪r s) : r = f ⁻¹'o s := by - ext (a b) + ext a b exact f.map_rel_iff.symm #align rel_embedding.eq_preimage RelEmbedding.eq_preimage diff --git a/Mathlib/Probability/Kernel/WithDensity.lean b/Mathlib/Probability/Kernel/WithDensity.lean index fb0563fee158a..df128d26072e0 100644 --- a/Mathlib/Probability/Kernel/WithDensity.lean +++ b/Mathlib/Probability/Kernel/WithDensity.lean @@ -187,7 +187,7 @@ theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : kernel α β) [IsFin intro n hn_not_mem rw [Finset.mem_range, not_lt] at hn_not_mem exact h_zero a b n hn_not_mem - ext (a b) : 2 + ext a b : 2 rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a), ENNReal.tsum_eq_liminf_sum_nat] have h_finset_sum : ∀ n, ∑ i in Finset.range n, fs i a b = min (f a b) n := by diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean index 446e9eea9d200..b1b4dccdb1894 100644 --- a/Mathlib/RepresentationTheory/Basic.lean +++ b/Mathlib/RepresentationTheory/Basic.lean @@ -262,11 +262,11 @@ variable (k : Type _) [CommSemiring k] (G : Type _) [Monoid G] (H : Type _) [Mul noncomputable def ofMulAction : Representation k G (H →₀ k) where toFun g := Finsupp.lmapDomain k k ((· • ·) g) map_one' := by - ext (x y) + ext x y dsimp simp map_mul' x y := by - ext (z w) + ext z w simp [mul_smul] #align representation.of_mul_action Representation.ofMulAction @@ -468,4 +468,3 @@ theorem dualTensorHom_comm (g : G) : end LinearHom end Representation - diff --git a/Mathlib/RingTheory/GradedAlgebra/Basic.lean b/Mathlib/RingTheory/GradedAlgebra/Basic.lean index 910e63e2f23ff..bce1e74cfdfa3 100644 --- a/Mathlib/RingTheory/GradedAlgebra/Basic.lean +++ b/Mathlib/RingTheory/GradedAlgebra/Basic.lean @@ -194,7 +194,7 @@ def GradedAlgebra.ofAlgHom [SetLike.GradedMonoid 𝒜] (decompose : A →ₐ[R] left_inv := AlgHom.congr_fun right_inv right_inv := by suffices decompose.comp (DirectSum.coeAlgHom 𝒜) = AlgHom.id _ _ from AlgHom.congr_fun this - -- Porting note: was ext (i x) : 2 + -- Porting note: was ext i x : 2 refine DirectSum.algHom_ext' _ _ fun i => ?_ ext x exact (decompose.congr_arg <| DirectSum.coeAlgHom_of _ _ _).trans (left_inv i x) diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean index bda79d482bad5..f8d2a52836f9a 100644 --- a/Mathlib/RingTheory/IsTensorProduct.lean +++ b/Mathlib/RingTheory/IsTensorProduct.lean @@ -225,7 +225,7 @@ variable (R M N S) theorem TensorProduct.isBaseChange : IsBaseChange S (TensorProduct.mk R S M 1) := by delta IsBaseChange convert TensorProduct.isTensorProduct R S M using 1 - ext (s x) + ext s x change s • (1 : S) ⊗ₜ[R] x = s ⊗ₜ[R] x rw [TensorProduct.smul_tmul'] congr 1 diff --git a/Mathlib/RingTheory/PolynomialAlgebra.lean b/Mathlib/RingTheory/PolynomialAlgebra.lean index c3ab8f2a15f8d..b8e0652559316 100644 --- a/Mathlib/RingTheory/PolynomialAlgebra.lean +++ b/Mathlib/RingTheory/PolynomialAlgebra.lean @@ -283,7 +283,7 @@ theorem matPolyEquiv_symm_apply_coeff (p : (Matrix n n R)[X]) (i j : n) (k : ℕ theorem matPolyEquiv_smul_one (p : R[X]) : matPolyEquiv (p • (1 : Matrix n n R[X])) = p.map (algebraMap R (Matrix n n R)) := by - ext (m i j) + ext m i j simp only [coeff_map, one_apply, algebraMap_matrix_apply, mul_boole, Pi.smul_apply, matPolyEquiv_coeff_apply] split_ifs <;> simp <;> rename_i h <;> simp [h] diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 7d6731381fd22..04694b4dcb9cd 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -1094,7 +1094,7 @@ def endTensorEndAlgHom : End R M ⊗[R] End R N →ₐ[R] End R (M ⊗[R] N) := simp only [homTensorHomMap_apply, TensorProduct.map_mul] · intro r simp only [homTensorHomMap_apply] - ext (m n) + ext m n simp [smul_tmul] #align module.End_tensor_End_alg_hom Module.endTensorEndAlgHom diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index 92ad461db0258..55d01e540b488 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -1996,7 +1996,7 @@ theorem IsNormal.eq_iff_zero_and_succ {f g : Ordinal.{u} → Ordinal.{u}} (hf : intro o ho H rw [← IsNormal.bsup_eq.{u, u} hf ho, ← IsNormal.bsup_eq.{u, u} hg ho] congr - ext (b hb) + ext b hb exact H b hb⟩ #align ordinal.is_normal.eq_iff_zero_and_succ Ordinal.IsNormal.eq_iff_zero_and_succ diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean index c4d2691a80de3..b7092bda5d312 100644 --- a/Mathlib/Topology/MetricSpace/Basic.lean +++ b/Mathlib/Topology/MetricSpace/Basic.lean @@ -144,7 +144,7 @@ theorem PseudoMetricSpace.ext {α : Type _} {m m' : PseudoMetricSpace α} cases' m' with d' _ _ _ ed' hed' U' hU' B' hB' obtain rfl : d = d' := h congr - · ext (x y) : 2 + · ext x y : 2 rw [hed, hed'] · exact uniformSpace_eq (hU.trans hU'.symm) · ext : 2 diff --git a/Mathlib/Topology/PathConnected.lean b/Mathlib/Topology/PathConnected.lean index ba8ffa3110f93..cbe782ff22c98 100644 --- a/Mathlib/Topology/PathConnected.lean +++ b/Mathlib/Topology/PathConnected.lean @@ -591,7 +591,7 @@ theorem pi_coe (γ : ∀ i, Path (as i) (bs i)) : ⇑(Path.pi γ) = fun t i => /-- Path composition commutes with products -/ theorem trans_pi_eq_pi_trans (γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i, Path (bs i) (cs i)) : (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i) := by - ext (t i) + ext t i unfold Path.trans simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe] split_ifs <;> rfl