chore: remove superfluous parentheses in calls to ext (#5258)

Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp>
Co-authored-by: Jason Yuen <jason_yuen2007@hotmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

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 : ι → ℕ) :

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) :

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

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]

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

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₂ _ _⟩

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

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]

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₁₁,

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,

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) :

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]

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]

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]

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]

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

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σ

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 =>

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

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
 

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

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

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
 

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]

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