bump to nightly-2023-06-09-07

mathlib commit leanprover-community/mathlib@7e5137f

Archive/100-theorems-list/16AbelRuffini.lean

@@ -144,7 +144,6 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
           refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
         _ = -(a - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
-
     have ha' := neg_nonpos.mpr (hle.trans ha)
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Icc ha' (hc _) (set.mem_Icc.mpr ⟨hfa, hf0⟩)
     exact ⟨x, 1, (hx1.trans_lt zero_lt_one).Ne, hx2, hf1⟩

Archive/100-theorems-list/37SolutionOfCubic.lean

@@ -130,7 +130,6 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     calc
       b / a / 3 = b / (a * 3) := by field_simp [ha]
       _ = b / (3 * a) := by rw [mul_comm]
-
   rw [h₄]
 #align theorems_100.cubic_eq_zero_iff Theorems100.cubic_eq_zero_iff
 
@@ -157,7 +156,6 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
       _ = a * (x + b / (3 * a)) ^ 3 + (d - (9 * a * b * c - 2 * b ^ 3) * a / (3 * a) ^ 3) := by
         simp only [hb2, hb3]; field_simp; ring
       _ = a * ((x + b / (3 * a)) ^ 3 - s ^ 3) := by rw [hs3, hq]; field_simp [h54]; ring
-
   have h₃ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
   have h₄ : ∀ x : K, x ^ 3 - s ^ 3 = (x - s) * (x - s * ω) * (x - s * ω ^ 2) :=
     by
@@ -168,7 +166,6 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
       _ = (x - s) * (x ^ 2 - (ω + ω ^ 2) * x * s + ω ^ 3 * s ^ 2) := by
         rw [hω.pow_eq_one, cube_root_of_unity_sum hω]; simp
       _ = (x - s) * (x - s * ω) * (x - s * ω ^ 2) := by ring
-
   rw [h₁, h₂, h₃, h₄ (x + b / (3 * a))]
   ring_nf
 #align theorems_100.cubic_eq_zero_iff_of_p_eq_zero Theorems100.cubic_eq_zero_iff_of_p_eq_zero

Archive/100-theorems-list/45Partition.lean

@@ -542,7 +542,6 @@ theorem same_gf [Field α] (m : ℕ) :
     _ = π₁ * π₂ * (1 + X ^ (m + 1)) := by ring
     _ = π₃ * (1 + X ^ (m + 1)) := by rw [ih]
     _ = _ := by rw [prod_range_succ]
-
 #align theorems_100.same_gf Theorems100.same_gf
 
 theorem same_coeffs [Field α] (m n : ℕ) (h : n ≤ m) :

Archive/100-theorems-list/57HeronsFormula.lean

@@ -75,7 +75,6 @@ theorem heron {p1 p2 p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) :
     _ = 1 / 4 * √ (s * (s - a) * (s - b) * (s - c) * 4 ^ 2) := by simp only [s]; ring_nf
     _ = √ (s * (s - a) * (s - b) * (s - c)) := by
       rw [sqrt_mul', sqrt_sq, div_mul_eq_mul_div, one_mul, mul_div_cancel] <;> norm_num
-
 #align theorems_100.heron Theorems100.heron
 
 end Theorems100

Archive/100-theorems-list/81SumOfPrimeReciprocalsDiverges.lean

@@ -137,7 +137,6 @@ theorem card_le_mul_sum {x k : ℕ} : (card (u x k) : ℝ) ≤ x * ∑ p in p x
     (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 hp => _)
     _ = x * ∑ p in P, 1 / p := mul_sum.symm
-
   simp only [mul_one_div, N, sep_def, filter_congr_decidable, Nat.card_multiples, Nat.cast_div_le]
 #align theorems_100.card_le_mul_sum Theorems100.card_le_mul_sum
 
@@ -173,7 +172,6 @@ theorem card_le_two_pow {x k : ℕ} : card ({e ∈ m x k | Squarefree (e + 1)})
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [K, card_powerset]
     _ ≤ 2 ^ card (range k) := (pow_le_pow 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
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
@@ -206,7 +204,6 @@ theorem card_le_two_pow_mul_sqrt {x k : ℕ} : card (m x k) ≤ 2 ^ k * Nat.sqrt
         b < b + 1 := lt_add_one b
         _ ≤ (m + 1).sqrt := by simpa only [Nat.le_sqrt, pow_two] using Nat.le_of_dvd hm' hbm
         _ ≤ x.sqrt := Nat.sqrt_le_sqrt (nat.succ_le_iff.mpr hm.1)
-
     · exact hm.2 p ⟨hp.1, hp.2.trans (Nat.dvd_of_pow_dvd one_le_two hbm)⟩
   have h2 : card M₂ ≤ Nat.sqrt x := by rw [← card_range (Nat.sqrt x)]; apply card_le_of_subset;
     simp [M₂, M]
@@ -215,7 +212,6 @@ theorem card_le_two_pow_mul_sqrt {x k : ℕ} : card (m x k) ≤ 2 ^ k * Nat.sqrt
     _ ≤ card K := card_image_le
     _ = 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
 
 theorem Real.tendsto_sum_one_div_prime_atTop :
@@ -248,19 +244,16 @@ theorem Real.tendsto_sum_one_div_prime_atTop :
       (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 / 2 := mul_one_div x 2
-
   have h4 :=
     calc
       (card M : ℝ) ≤ 2 ^ k * x.sqrt := by exact_mod_cast card_le_two_pow_mul_sqrt
       _ = 2 ^ k * ↑(2 ^ (k + 1)) := by rw [Nat.sqrt_eq]
       _ = x / 2 := by field_simp [x, mul_right_comm, ← pow_succ']
-
   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 := add_halves ↑x
-
 #align theorems_100.real.tendsto_sum_one_div_prime_at_top Theorems100.Real.tendsto_sum_one_div_prime_atTop
 
 end Theorems100

Archive/100-theorems-list/9AreaOfACircle.lean

@@ -102,7 +102,6 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 :=
           neg_le_self (sqrt_nonneg _))
       _ = ENNReal.ofReal (∫ x in (-r : ℝ)..r, 2 * f x) := by simp [two_mul, integral_of_le]
       _ = NNReal.pi * r ^ 2 := by rw_mod_cast [this, ← ENNReal.coe_nnreal_eq]
-
   obtain ⟨hle, heq | hlt⟩ := NNReal.coe_nonneg r, hle.eq_or_lt; · simp [← HEq]
   have hderiv : ∀ x ∈ Ioo (-r : ℝ) r, HasDerivAt F (2 * f x) x :=
     by
@@ -124,20 +123,17 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 :=
       calc
         -(1 : ℝ) = r⁻¹ * -r := by simp [hlt.ne']
         _ < r⁻¹ * x := by nlinarith [inv_pos.mpr hlt]
-
     · suffices (r : ℝ)⁻¹ * x < 1 by exact this.ne
       calc
         (r : ℝ)⁻¹ * x < r⁻¹ * r := by nlinarith [inv_pos.mpr hlt]
         _ = 1 := inv_mul_cancel hlt.ne'
-
     · nlinarith
   have hcont := (by continuity : Continuous F).ContinuousOn
   calc
     (∫ x in -r..r, 2 * f x) = F r - F (-r) :=
       integral_eq_sub_of_has_deriv_at_of_le (neg_le_self r.2) hcont hderiv
         (continuous_const.mul hf).ContinuousOn.IntervalIntegrable
     _ = NNReal.pi * r ^ 2 := by norm_num [F, inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]
-
 #align theorems_100.area_disc Theorems100.area_disc
 
 end Theorems100

Archive/Arithcc.lean

@@ -331,7 +331,6 @@ theorem compiler_correctness :
     calc
       ζ₁ = outcome (compile map e_s₁ t) η := by cc
       _ ≃[t] { η with ac := ν₁ } := by apply e_ih_s₁ <;> assumption
-
     have hζ₁_ν₁ : ζ₁.ac = ν₁ := by finish [state_eq]
     have hζ₂ : ζ₂ ≃[t + 1]/ac write t ν₁ η
     calc
@@ -343,7 +342,6 @@ theorem compiler_correctness :
         by
         apply state_eq_rs_implies_write_eq_rs
         simp [state_eq_rs]
-
     have hζ₂_ν₂ : read t ζ₂ = ν₁ := by
       simp [state_eq_rs] at hζ₂ ⊢
       specialize hζ₂ t (register.lt_succ_self _)
@@ -358,13 +356,11 @@ theorem compiler_correctness :
         read (loc x map) ζ₂ = read (loc x map) (write t ν₁ η) := hζ₂ _ (ht' _)
         _ = read (loc x map) η := by simp only [loc] at ht ; simp [(ht _).Ne]
         _ = ξ x := hmap x
-
     have hζ₃ : ζ₃ ≃[t + 1] { write t ν₁ η with ac := ν₂ }
     calc
       ζ₃ = outcome (compile map e_s₂ (t + 1)) ζ₂ := by cc
       _ ≃[t + 1] { ζ₂ with ac := ν₂ } := by apply e_ih_s₂ <;> assumption
       _ ≃[t + 1] { write t ν₁ η with ac := ν₂ } := by simp [state_eq]; apply hζ₂
-
     have hζ₃_ν₂ : ζ₃.ac = ν₂ := by finish [state_eq]
     have hζ₃_ν₁ : read t ζ₃ = ν₁ :=
       by
@@ -380,7 +376,6 @@ theorem compiler_correctness :
       _ ≃[t + 1] { { write t ν₁ η with ac := ν₂ } with ac := ν } := by simp [state_eq] at hζ₃ ⊢;
         cases hζ₃; assumption
       _ ≃[t + 1] { write t ν₁ η with ac := ν } := by simp
-
     apply write_eq_implies_state_eq <;> assumption
 #align arithcc.compiler_correctness Arithcc.compiler_correctness
 

Archive/Imo/Imo1962Q1.lean

@@ -134,7 +134,6 @@ theorem case_more_digits {c n : ℕ} (h1 : (digits 10 c).length ≥ 6) (h2 : Pro
     _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c h6 h3)
     _ ≥ 10 ^ 6 := ((pow_le_iff_le_right h6).mpr h1)
     _ ≥ 153846 := by norm_num
-
 #align imo1962_q1.case_more_digits Imo1962Q1.case_more_digits
 
 /-!

Archive/Imo/Imo1962Q4.lean

@@ -125,7 +125,6 @@ theorem formula {R : Type _} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
     _ ↔ a * (2 * a ^ 2 - 1) * (4 * a ^ 2 - 3) = 0 := by simp [(by norm_num : (2 : R) ≠ 0)]
     _ ↔ (2 * a ^ 2 - 1) * (4 * a ^ 3 - 3 * a) = 0 := by
       constructor <;> intro h <;> convert h using 1 <;> ring
-
 #align imo1962_q4.formula imo1962_q4.formula
 
 /-
@@ -150,6 +149,5 @@ theorem imo1962_q4' {x : ℝ} : ProblemEquation x ↔ x ∈ solutionSet :=
     ProblemEquation x ↔ cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1 := by rfl
     _ ↔ cos (2 * x) = 0 ∨ cos (3 * x) = 0 := by simp [cos_two_mul, cos_three_mul, formula]
     _ ↔ x ∈ solutionSet := by rw [solve_cos2x_0, solve_cos3x_0, ← exists_or]; rfl
-
 #align imo1962_q4' imo1962_q4'
 

Archive/Imo/Imo1972Q5.lean

@@ -52,7 +52,6 @@ example (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x
       _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := (norm_add_le _ _)
       _ ≤ k + k := (add_le_add (hk₁ _) (hk₁ _))
       _ = 2 * k := (two_mul _).symm
-
   -- Suppose the conclusion does not hold.
   by_contra' hneg
   set k' := k / ‖g y‖
@@ -64,7 +63,6 @@ example (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x
       calc
         0 < ‖f x‖ := norm_pos_iff.mpr hx
         _ ≤ k := hk₁ x
-
     rw [div_lt_iff]
     apply lt_mul_of_one_lt_right h₁ hneg
     exact trans zero_lt_one hneg
@@ -85,7 +83,6 @@ example (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x
   calc
     k' < k := H₁
     _ ≤ k' := H₂
-
 
 /-- IMO 1972 Q5
 
@@ -115,7 +112,6 @@ example (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x
       _ = ‖f (x + y) + f (x - y)‖ := by rw [hf1]
       _ ≤ ‖f (x + y)‖ + ‖f (x - y)‖ := (abs_add _ _)
       _ ≤ 2 * k := by linarith [h (x + y), h (x - y)]
-
   linarith
 
 end Imo1972Q5

Archive/Imo/Imo1977Q6.lean

@@ -34,7 +34,6 @@ theorem imo1977_q6_nat (f : ℕ → ℕ) (h : ∀ n, f (f n) < f (n + 1)) : ∀
       calc
         k ≤ f (f (n - 1)) := h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))
         _ < f n := tsub_add_cancel_of_le (le_trans (Nat.succ_le_succ (Nat.zero_le _)) hk) ▸ h _
-
   have hf : ∀ n, n ≤ f n := fun n => h' n n rfl.le
   have hf_mono : StrictMono f := strictMono_nat_of_lt_succ fun _ => lt_of_le_of_lt (hf _) (h _)
   intro

Archive/Imo/Imo1981Q3.lean

@@ -61,7 +61,6 @@ theorem m_le_n {m n : ℤ} (h1 : ProblemPredicate N m n) : m ≤ n :=
     calc
       1 = (n ^ 2 - m * n - m ^ 2) ^ 2 := h1.eq_one.symm
       _ = (n * (n - m) - m ^ 2) ^ 2 := by ring
-
   have h4 : n * (n - m) - m ^ 2 < -1 := by nlinarith [h1.n_range.left]
   have h5 : 1 < (n * (n - m) - m ^ 2) ^ 2 := by nlinarith
   exact h5.ne h3
@@ -72,7 +71,6 @@ theorem eq_imp_1 {n : ℤ} (h1 : ProblemPredicate N n n) : n = 1 :=
     calc
       _ = (n ^ 2 - n * n - n ^ 2) ^ 2 := by simp [sq, mul_assoc]
       _ = 1 := h1.eq_one
-
   eq_one_of_mul_eq_one_right h1.m_range.left.le this
 #align imo1981_q3.problem_predicate.eq_imp_1 Imo1981Q3.ProblemPredicate.eq_imp_1
 
@@ -89,14 +87,12 @@ theorem reduction {m n : ℤ} (h1 : ProblemPredicate N m n) (h2 : 1 < n) :
       calc
         _ < n := sub_lt_self n h1.m_range.left
         _ ≤ N := h1.n_range.right
-
     exact ⟨h5, h6.le⟩
   -- eq_one:
   ·
     calc
       _ = (n ^ 2 - m * n - m ^ 2) ^ 2 := by ring
       _ = 1 := h1.eq_one
-
 #align imo1981_q3.problem_predicate.reduction Imo1981Q3.ProblemPredicate.reduction
 
 end ProblemPredicate
@@ -174,20 +170,17 @@ theorem m_n_bounds {m n : ℕ} (h1 : NatPredicate N m n) : m ≤ fib K ∧ n ≤
       calc
         m = fib k := hm
         _ ≤ fib K := fib_mono h3
-
     · have h6 : k + 1 ≤ K + 1 := succ_le_succ h3
       calc
         n = fib (k + 1) := hn
         _ ≤ fib (K + 1) := fib_mono h6
-
   · have h7 : N < n := by
       have h8 : K + 2 ≤ k + 1 := succ_le_succ (not_lt.mp h2)
       rw [← fib_add_two] at HK 
       calc
         N < fib (K + 2) := HK
         _ ≤ fib (k + 1) := (fib_mono h8)
         _ = n := hn.symm
-
     have h9 : n ≤ N := h1.n_le_N
     exact absurd h7 h9.not_lt
 #align imo1981_q3.m_n_bounds Imo1981Q3.m_n_bounds

Archive/Imo/Imo1987Q1.lean

@@ -49,7 +49,6 @@ def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x :
     _ ≃ Σ x : α, { σ : Perm α // ∀ y : ({x} : Set α), σ y = Equiv.refl (↥({x} : Set α)) y } :=
       (sigmaCongrRight fun x => Equiv.Set.ofEq <| by simp only [SetCoe.forall]; dsimp; simp)
     _ ≃ Σ x : α, Perm ({x}ᶜ : Set α) := sigmaCongrRight fun x => by apply Equiv.Set.compl
-
 #align imo1987_q1.fixed_points_equiv Imo1987Q1.fixedPointsEquiv
 
 theorem card_fixed_points : card { σx : α × Perm α // σx.2 σx.1 = σx.1 } = card α * (card α - 1)! :=

Archive/Imo/Imo1988Q6.lean

@@ -244,7 +244,6 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
       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 + 1) * k := by linarith
-
   · -- Show the descent step.
     intro x y hx x_lt_y hxky h z h_root hV₁ hV₀
     constructor
@@ -267,7 +266,6 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) :
       calc
         z * y > x * x := by apply mul_lt_mul' <;> linarith
         _ ≥ x * x - k := sub_le_self _ (Int.ofNat_zero_le k)
-
   ·-- There is no base case in this application of Vieta jumping.
     simp
 #align imo1988_q6 imo1988_q6
@@ -317,7 +315,6 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^
           rw [mul_add, mul_one]
           apply add_lt_add_left
           assumption_mod_cast
-
   · -- Show the base case.
     intro x y h h_base
     obtain rfl | rfl : x = 0 ∨ x = 1 := by rwa [Nat.le_add_one_iff, le_zero_iff] at h_base 

Archive/Imo/Imo1994Q1.lean

@@ -80,7 +80,6 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
     _ = ∑ i : Fin (m + 1), a i + a (rev i) := sum_add_distrib.symm
     _ ≥ ∑ 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 -
   by_contra' h : a k + a (rev k) < n + 1

Archive/Imo/Imo2001Q2.lean

@@ -60,7 +60,6 @@ theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
       by ring
     _ ≥ 0 :=
       add_nonneg (add_nonneg (mul_nonneg zero_le_two (sq_nonneg _)) (sq_nonneg _)) (sq_nonneg _)
-
 #align imo2001_q2.bound Imo2001Q2.bound
 
 theorem imo2001_q2' (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
@@ -73,7 +72,6 @@ theorem imo2001_q2' (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
   calc
     _ ≥ _ := add_le_add (add_le_add (bound ha hb hc) (bound hb hc ha)) (bound hc ha hb)
     _ = 1 := by rw [h₁, h₂, ← add_div, ← add_div, div_self <| ne_of_gt <| denom_pos ha hb hc]
-
 #align imo2001_q2.imo2001_q2' Imo2001Q2.imo2001_q2'
 
 end imo2001_q2
@@ -88,6 +86,5 @@ theorem imo2001_q2 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
   calc
     1 ≤ _ := imo2001_q2' (rpow_pos_of_pos ha _) (rpow_pos_of_pos hb _) (rpow_pos_of_pos hc _)
     _ = _ := by rw [h3 ha, h3 hb, h3 hc]
-
 #align imo2001_q2 imo2001_q2
 

Archive/Imo/Imo2005Q3.lean

@@ -55,7 +55,6 @@ theorem key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x
       refine' (div_le_div_right h₄).mpr _; simp
       exact (le_mul_iff_one_le_right (pow_pos hx 2)).mpr h
     _ = (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) := by field_simp [h₂.ne', h₃.ne']; ring
-
 #align imo2005_q3.key_insight Imo2005Q3.key_insight
 
 end imo2005_q3
@@ -83,6 +82,5 @@ theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x *
     _ ≥ 0 :=
       div_nonneg (by linarith [sq_nonneg (x - y), sq_nonneg (y - z), sq_nonneg (z - x)])
         (by linarith [sq_nonneg x, sq_nonneg y, sq_nonneg z])
-
 #align imo2005_q3 imo2005_q3
 

Archive/Imo/Imo2005Q4.lean

@@ -57,15 +57,13 @@ theorem find_specified_factor {p : ℕ} (hp : Nat.Prime p) (hp' : IsCoprime (6 :
       apply_rules [Int.ModEq.sub_right, Int.ModEq.add, Int.ModEq.mul_left,
         Int.ModEq.pow_card_sub_one_eq_one hp]
     _ = 0 := by norm_num
-
   -- Since `6` has an inverse mod `p`, `a (p - 2)` itself is a multiple of `p`
   calc
     (a (p - 2) : ℤ) = 1 * a (p - 2) := by ring
     _ ≡ 6 * b * a (p - 2) [ZMOD p] := (Int.ModEq.mul_right _ hb.symm)
     _ = b * (6 * a (p - 2)) := by ring
     _ ≡ b * 0 [ZMOD p] := (Int.ModEq.mul_left _ H)
     _ = 0 := by ring
-
 #align imo2005_q4.find_specified_factor Imo2005Q4.find_specified_factor
 
 end imo2005_q4