chore: superfluous parentheses part 2 (#12131)

Co-authored-by: Moritz Firsching <firsching@google.com>

Author: mo271

Archive/Imo/Imo1962Q1.lean

@@ -119,7 +119,7 @@ theorem case_more_digits {c n : ℕ} (h1 : (digits 10 c).length ≥ 6) (h2 : Pro
     exact case_0_digit h5 h2
   calc
     n ≥ 10 * c := le.intro h2.left.symm
-    _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c (by decide) h3)
+    _ ≥ 10 ^ (digits 10 c).length := base_pow_length_digits_le 10 c (by decide) h3
     _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) h1
     _ ≥ 153846 := by norm_num
 #align imo1962_q1.case_more_digits Imo1962Q1.case_more_digits

Archive/Imo/Imo1972Q5.lean

@@ -41,8 +41,8 @@ theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y
     calc
       2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [abs_mul, mul_assoc]
       _ = ‖f (x + y) + f (x - y)‖ := by rw [hf1]
-      _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := (norm_add_le _ _)
-      _ ≤ k + k := (add_le_add (hk₁ _) (hk₁ _))
+      _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := norm_add_le _ _
+      _ ≤ k + k := add_le_add (hk₁ _) (hk₁ _)
       _ = 2 * k := (two_mul _).symm
   set k' := k / ‖g y‖
   -- Demonstrate that `k' < k` using `hneg`.
@@ -98,6 +98,6 @@ theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x -
     calc
       2 * (‖f x‖ * ‖g y‖) = ‖2 * f x * g y‖ := by simp [abs_mul, mul_assoc]
       _ = ‖f (x + y) + f (x - y)‖ := by rw [hf1]
-      _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := (abs_add _ _)
+      _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := abs_add _ _
       _ ≤ 2 * k := by linarith [h (x + y), h (x - y)]
   linarith

Archive/Imo/Imo1981Q3.lean

@@ -163,7 +163,7 @@ theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤
       rw [← fib_add_two] at HK
       calc
         N < fib (K + 2) := HK
-        _ ≤ fib (k + 1) := (fib_mono h8)
+        _ ≤ fib (k + 1) := fib_mono h8
         _ = n := hn.symm
     have h9 : n ≤ N := h1.n_le_N
     exact absurd h7 h9.not_lt

Archive/Imo/Imo1988Q6.lean

@@ -227,7 +227,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
     apply ne_of_lt
     calc
       x * x + x * x = x * x * 2 := by rw [mul_two]
-      _ ≤ x * x * k := (Nat.mul_le_mul_left (x * x) k_lt_one)
+      _ ≤ x * x * k := Nat.mul_le_mul_left (x * x) k_lt_one
       _ < (x * x + 1) * k := by linarith
   · -- Show the descent step.
     intro x y hx x_lt_y _ _ z h_root _ hV₀

Archive/Imo/Imo1994Q1.lean

@@ -67,7 +67,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
     2 * ∑ i : Fin (m + 1), a i = ∑ i : Fin (m + 1), a i + ∑ i : Fin (m + 1), a i := two_mul _
     _ = ∑ i : Fin (m + 1), a i + ∑ i : Fin (m + 1), a (rev i) := by rw [Equiv.sum_comp rev]
     _ = ∑ i : Fin (m + 1), (a i + a (rev i)) := sum_add_distrib.symm
-    _ ≥ ∑ i : Fin (m + 1), (n + 1) := (sum_le_sum hpair)
+    _ ≥ ∑ i : Fin (m + 1), (n + 1) := sum_le_sum hpair
     _ = (m + 1) * (n + 1) := by rw [sum_const, card_fin, Nat.nsmul_eq_mul]
   -- It remains to prove the key inequality, by contradiction
   rintro k -

Archive/Imo/Imo2008Q2.lean

@@ -114,7 +114,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
       have h₂ : q < t * (t + 1) := by
         calc
           q < q + 1 := by linarith
-          _ ≤ t := (le_max_left (q + 1) 1)
+          _ ≤ t := le_max_left (q + 1) 1
           _ ≤ t + t ^ 2 := by linarith [sq_nonneg t]
           _ = t * (t + 1) := by ring
       exact ⟨h₁, h₂⟩

Archive/Imo/Imo2011Q3.lean

@@ -28,7 +28,7 @@ theorem imo2011_q3 (f : ℝ → ℝ) (hf : ∀ x y, f (x + y) ≤ y * f x + f (f
   have hxt : ∀ x t, f t ≤ t * f x - x * f x + f (f x) := fun x t =>
     calc
       f t = f (x + (t - x)) := by rw [add_eq_of_eq_sub' rfl]
-      _ ≤ (t - x) * f x + f (f x) := (hf x (t - x))
+      _ ≤ (t - x) * f x + f (f x) := hf x (t - x)
       _ = t * f x - x * f x + f (f x) := by rw [sub_mul]
   have h_ab_combined : ∀ a b, a * f a + b * f b ≤ 2 * f a * f b := fun a b => by
     linarith [hxt b (f a), hxt a (f b)]

Archive/Imo/Imo2011Q5.lean

@@ -36,8 +36,8 @@ theorem imo2011_q5 (f : ℤ → ℤ) (hpos : ∀ n : ℤ, 0 < f n) (hdvd : ∀ m
     have h_neg_d_lt_fn : -d < f n := by
       calc
         -d = f (m - n) - f m := neg_sub _ _
-        _ < f (m - n) := (sub_lt_self _ (hpos m))
-        _ ≤ f n - f m := (le_of_dvd (sub_pos.mpr h_fm_lt_fn) ?_)
+        _ < f (m - n) := sub_lt_self _ (hpos m)
+        _ ≤ f n - f m := le_of_dvd (sub_pos.mpr h_fm_lt_fn) ?_
         _ < f n := sub_lt_self _ (hpos m)
       -- ⊢ f (m - n) ∣ f n - f m
       rw [← dvd_neg, neg_sub]

Archive/Imo/Imo2013Q5.lean

@@ -95,7 +95,7 @@ theorem f_pos_of_pos {f : ℚ → ℝ} {q : ℚ} (hq : 0 < q)
   have hmul_pos :=
     calc
       (0 : ℝ) < q.num := Int.cast_pos.mpr num_pos
-      _ = ((q.num.natAbs : ℤ) : ℝ) := (congr_arg Int.cast (Int.natAbs_of_nonneg num_pos.le).symm)
+      _ = ((q.num.natAbs : ℤ) : ℝ) := congr_arg Int.cast (Int.natAbs_of_nonneg num_pos.le).symm
       _ ≤ f q.num.natAbs := (H4 q.num.natAbs ((@Int.natAbs_pos q.num).mpr num_pos.ne.symm))
       _ = f q.num := by rw [Nat.cast_natAbs, abs_of_nonneg num_pos.le]
       _ = f (q * q.den) := by rw [← Rat.mul_den_eq_num]
@@ -168,7 +168,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
     calc
       f x + f (a ^ N - x) ≤ f (x + (a ^ N - x)) := H2 x (a ^ N - x) hxp (by positivity)
       _ = f (a ^ N) := by ring_nf
-      _ = a ^ N := (fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae)
+      _ = a ^ N := fixed_point_of_pos_nat_pow hNp H1 H4 H5 ha1 hae
       _ = x + (a ^ N - x) := by ring
   have heq := h1.antisymm (mod_cast h2)
   linarith [H5 x hx, H5 _ h_big_enough]
@@ -204,12 +204,12 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
         ↑a * 1 = ↑a := mul_one (a : ℝ)
         _ = f a := hae.symm
         _ = f (a * 1) := by rw [mul_one]
-        _ ≤ f a * f 1 := ((H1 a 1) (zero_lt_one.trans ha1) zero_lt_one)
+        _ ≤ f a * f 1 := (H1 a 1) (zero_lt_one.trans ha1) zero_lt_one
         _ = ↑a * f 1 := by rw [hae]
     calc
       (n : ℝ) = (n : ℝ) * 1 := (mul_one _).symm
       _ ≤ (n : ℝ) * f 1 := by gcongr
-      _ ≤ f (n * 1) := (H3 1 zero_lt_one n hn)
+      _ ≤ f (n * 1) := H3 1 zero_lt_one n hn
       _ = f n := by rw [mul_one]
   have H5 : ∀ x : ℚ, 1 < x → (x : ℝ) ≤ f x := by
     intro x hx

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -132,7 +132,7 @@ theorem card_le_mul_sum {x k : ℕ} : (card (U x k) : ℝ) ≤ x * ∑ p in P x
   have h : card (Finset.biUnion P N) ≤ ∑ p in P, card (N p) := card_biUnion_le
   calc
     (card (Finset.biUnion P N) : ℝ) ≤ ∑ p in P, (card (N p) : ℝ) := by assumption_mod_cast
-    _ ≤ ∑ p in P, x * (1 / (p : ℝ)) := (sum_le_sum fun p _ => ?_)
+    _ ≤ ∑ p in P, x * (1 / (p : ℝ)) := sum_le_sum fun p _ => ?_
     _ = x * ∑ p in P, 1 / (p : ℝ) := by rw [mul_sum]
   simp only [N, mul_one_div, Nat.card_multiples, Nat.cast_div_le]
 #align theorems_100.card_le_mul_sum Theorems100.card_le_mul_sum
@@ -168,7 +168,7 @@ theorem card_le_two_pow {x k : ℕ} :
     card M₁ ≤ card (image f K) := card_le_card h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [K, card_powerset]; rfl
-    _ ≤ 2 ^ card (range k) := (pow_le_pow_right one_le_two card_image_le)
+    _ ≤ 2 ^ card (range k) := pow_le_pow_right one_le_two card_image_le
     _ = 2 ^ k := by rw [card_range k]
 #align theorems_100.card_le_two_pow Theorems100.card_le_two_pow
 
@@ -205,7 +205,7 @@ theorem card_le_two_pow_mul_sqrt {x k : ℕ} : card (M x k) ≤ 2 ^ k * Nat.sqrt
   calc
     card (M x k) ≤ card (image f K) := card_le_card h1
     _ ≤ card K := card_image_le
-    _ = card M₁ * card M₂ := (card_product M₁ M₂)
+    _ = card M₁ * card M₂ := card_product M₁ M₂
     _ ≤ 2 ^ k * x.sqrt := mul_le_mul' card_le_two_pow h2
 #align theorems_100.card_le_two_pow_mul_sqrt Theorems100.card_le_two_pow_mul_sqrt
 
@@ -236,7 +236,7 @@ theorem Real.tendsto_sum_one_div_prime_atTop :
   have h3 :=
     calc
       (card U' : ℝ) ≤ x * ∑ p in P, 1 / (p : ℝ) := card_le_mul_sum
-      _ < x * (1 / 2) := (mul_lt_mul_of_pos_left (h1 x) (by norm_num [x]))
+      _ < x * (1 / 2) := mul_lt_mul_of_pos_left (h1 x) (by norm_num [x])
       _ = x / 2 := mul_one_div (x : ℝ) 2
   have h4 :=
     calc
@@ -246,7 +246,7 @@ theorem Real.tendsto_sum_one_div_prime_atTop :
   refine' lt_irrefl (x : ℝ) _
   calc
     (x : ℝ) = (card U' : ℝ) + (card M' : ℝ) := by assumption_mod_cast
-    _ < x / 2 + x / 2 := (add_lt_add_of_lt_of_le h3 h4)
+    _ < x / 2 + x / 2 := add_lt_add_of_lt_of_le h3 h4
     _ = x := add_halves (x : ℝ)
 #align theorems_100.real.tendsto_sum_one_div_prime_at_top Theorems100.Real.tendsto_sum_one_div_prime_atTop