chore: remove some superfluous parens (#35921)

Found by manually auditing the output of regex-searching for '\([A-Za-z0-9_][A-Za-z0-9_]+\)'. Most results are false positives (such as, documentation or export statements), a few are more interesting.

Not exhaustive, I looked at perhaps a fifth or a tenth of all results.

Author: grunweg

Counterexamples/AharoniKorman.lean

@@ -235,7 +235,7 @@ lemma to prove that fact later: `no_infinite_antichain`.
 -/
 lemma no_infinite_antichain_level {n : ℕ} {A : Set Hollom} (hA : A ⊆ level n)
     (hA' : IsAntichain (· ≤ ·) A) : A.Finite :=
-  hA'.finite_of_partiallyWellOrderedOn ((level_isPWO).mono hA)
+  hA'.finite_of_partiallyWellOrderedOn (level_isPWO.mono hA)
 
 /--
 Each level is order-connected, i.e. for any `x ∈ level n` and `y ∈ level n` we have

Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

@@ -205,7 +205,7 @@ instance : CanonicallyOrderedAdd L where
   le_self_add := le_self_add
 
 instance : NoZeroDivisors L where
-  eq_zero_or_eq_zero_of_mul_eq_zero := @(eq_zero_or_eq_zero_of_mul_eq_zero)
+  eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero
 
 /-- The elements `(1,0)` and `(1,1)` of `L` are different, but their doubles coincide.
 -/

Mathlib/Algebra/Category/ModuleCat/Presheaf/Pullback.lean

@@ -70,7 +70,7 @@ this object shall be mapped to `(free R).obj (yoneda.obj (F.obj X))`. -/
 noncomputable def pushforwardCompCoyonedaFreeYonedaCorepresentableBy (X : C) :
     (pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).CorepresentableBy
       ((free R).obj (yoneda.obj (F.obj X))) where
-  homEquiv {M} := (freeYonedaEquiv).trans
+  homEquiv {M} := freeYonedaEquiv.trans
     (freeYonedaEquiv (M := (pushforward φ).obj M)).symm
   homEquiv_comp {M N} g f := freeYonedaEquiv.injective (by
     dsimp

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -42,7 +42,7 @@ initialize_simps_projections SemiRingCat (-semiring)
 
 namespace SemiRingCat
 
-instance : CoeSort (SemiRingCat) (Type u) :=
+instance : CoeSort SemiRingCat (Type u) :=
   ⟨SemiRingCat.carrier⟩
 
 attribute [coe] SemiRingCat.carrier
@@ -200,7 +200,7 @@ initialize_simps_projections RingCat (-ring)
 
 namespace RingCat
 
-instance : CoeSort (RingCat) (Type u) :=
+instance : CoeSort RingCat (Type u) :=
   ⟨RingCat.carrier⟩
 
 attribute [coe] RingCat.carrier
@@ -532,7 +532,7 @@ initialize_simps_projections CommRingCat (-commRing)
 
 namespace CommRingCat
 
-instance : CoeSort (CommRingCat) (Type u) :=
+instance : CoeSort CommRingCat (Type u) :=
   ⟨CommRingCat.carrier⟩
 
 attribute [coe] CommRingCat.carrier

Mathlib/Algebra/Group/Pointwise/Finset/BigOperators.lean

@@ -43,7 +43,7 @@ variable [DecidableEq α]
 @[to_additive (attr := simp, norm_cast)]
 theorem coe_prod (s : Finset ι) (f : ι → Finset α) :
     ↑(∏ i ∈ s, f i) = ∏ i ∈ s, (f i : Set α) :=
-  map_prod ((coeMonoidHom) : Finset α →* Set α) _ _
+  map_prod (coeMonoidHom : Finset α →* Set α) _ _
 
 omit [DecidableEq α]
 variable [DecidableEq ι]

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -830,14 +830,14 @@ theorem inf_subgroupOf_inf_normal_of_right (A B' B : Subgroup G)
     [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal := by
   rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
   rw [inf_inf_inf_comm, inf_idem]
-  exact le_trans (inf_le_inf A.le_normalizer hN) (inf_normalizer_le_normalizer_inf)
+  exact le_trans (inf_le_inf A.le_normalizer hN) inf_normalizer_le_normalizer_inf
 
 @[to_additive]
 theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G)
     [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal := by
   rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
   rw [inf_inf_inf_comm, inf_idem]
-  exact le_trans (inf_le_inf hN B.le_normalizer) (inf_normalizer_le_normalizer_inf)
+  exact le_trans (inf_le_inf hN B.le_normalizer) inf_normalizer_le_normalizer_inf
 
 @[to_additive]
 instance normal_inf_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal :=

Mathlib/Algebra/Lie/Semisimple/Lemmas.lean

@@ -67,7 +67,7 @@ lemma hasCentralRadical_and_of_isIrreducible_of_isFaithful :
 
 theorem hasTrivialRadical_of_isIrreducible_of_isFaithful
     (h : ∀ x, LinearMap.trace k _ (toEnd k L M x) = 0) : HasTrivialRadical k L := by
-  have : finrank k M ≠ 0 := ((finrank_pos_iff).mpr <| nontrivial_of_isIrreducible k L M).ne'
+  have : finrank k M ≠ 0 := (finrank_pos_iff.mpr <| nontrivial_of_isIrreducible k L M).ne'
   obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M
   rw [hasTrivialRadical_iff, (hasCentralRadical_iff k L).mp inferInstance, LieSubmodule.eq_bot_iff]
   intro x hx

Mathlib/Algebra/Order/Antidiag/Nat.lean

@@ -306,6 +306,6 @@ open scoped ArithmeticFunction.omega in -- access notation `ω`
 theorem card_pair_lcm_eq {n : ℕ} (hn : Squarefree n) :
     #{p ∈ (n.divisors ×ˢ n.divisors) | p.1.lcm p.2 = n} = 3 ^ ω n := by
   rw [← card_finMulAntidiag_of_squarefree hn, eq_comm]
-  apply Finset.card_bij f (f_img hn) (f_inj) (f_surj hn.ne_zero)
+  apply Finset.card_bij f (f_img hn) f_inj (f_surj hn.ne_zero)
 
 end Nat

Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -504,7 +504,7 @@ theorem mulArchimedean_of_mk_eq_mk (h : ∀ a ≠ (1 : M), ∀ b ≠ 1, mk a = m
     · use 0
       simpa using hx
     · have hxy : mk x = mk y := h x hx.ne.symm y hy.ne.symm
-      obtain ⟨_, ⟨m, hm⟩⟩ := (mk_eq_mk).mp hxy
+      obtain ⟨_, ⟨m, hm⟩⟩ := mk_eq_mk.mp hxy
       rw [mabs_eq_self.mpr hx.le, mabs_eq_self.mpr hy.le] at hm
       exact ⟨m, hm⟩
 

Mathlib/Algebra/Order/CompleteField.lean

@@ -269,7 +269,7 @@ def inducedOrderRingHom : α →+*o β :=
       refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_
       · exact le_inducedMap_mul_self_of_mem_cutMap hx
       · exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx)
-      (two_ne_zero) (inducedMap_one _ _) with
+          two_ne_zero (inducedMap_one _ _) with
     monotone' := inducedMap_mono _ _ }
 
 /-- The isomorphism of ordered rings between two conditionally complete linearly ordered fields. -/