Remove some whitespace

FltRegular/CaseI/AuxLemmas.lean

@@ -17,8 +17,8 @@ local notation "P" => (⟨p, hpri.pos⟩ : ℕ+)
 local notation "K" => CyclotomicField P ℚ
 
 local notation "R" => 𝓞 K
- 
- 
+
+
 namespace CaseI
 
 theorem two_lt (hp5 : 5 ≤ p) : 2 < p := by linarith

FltRegular/FltThree/OddPrimeOrFour.lean

@@ -66,7 +66,7 @@ theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n 
     calc
       2 ^ k = 2 ^ 2 * 2 ^ (k - 2) := (pow_mul_pow_sub _ ?_).symm
       _ = 4 * 2 ^ (k - 2) := by norm_num
-      
+
     rcases k with (_ | _ | _)
     · exfalso
       norm_num at n2
@@ -319,4 +319,4 @@ theorem factorsOddPrimeOrFour.pow (z : ℤ) (n : ℕ) (hz : Even (evenFactorExp
     factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z := by
   simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow,
     Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow]
-#align factors_odd_prime_or_four.pow factorsOddPrimeOrFour.pow
+#align factors_odd_prime_or_four.pow factorsOddPrimeOrFour.pow

FltRegular/FltThree/Primes.lean

@@ -29,7 +29,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) :
   set c := a % x with hc
   by_cases H : 2 * c.natAbs < x.natAbs
   · exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩
-  · push_neg at H 
+  · push_neg at H
     refine' ⟨(a + abs x) / x, c - abs x, _, _⟩
     · have := self_dvd_abs x
       rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc,
@@ -40,7 +40,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) :
       rw [Int.ofNat_mul, ofNat_two] at H ⊢
       have hcnonneg := Int.emod_nonneg a h0'
       have := Int.emod_lt a h0'
-      rw [Int.natAbs_of_nonneg hcnonneg] at H 
+      rw [Int.natAbs_of_nonneg hcnonneg] at H
       rw [← Int.natAbs_neg, neg_sub, Int.natAbs_of_nonneg (sub_nonneg_of_le this.le), mul_sub,
         sub_lt_iff_lt_add, two_mul, Int.abs_eq_natAbs, add_lt_add_iff_left]
       apply lt_of_le_of_ne H
@@ -57,7 +57,7 @@ nonrec theorem Int.two_not_cube (r : ℤ) : r ^ 3 ≠ 2 :=by
   apply two_not_cube r.natAbs
   rw [← Int.natAbs_pow, H]
   norm_num; decide
-#align int.two_not_cube Int.two_not_cube  
+#align int.two_not_cube Int.two_not_cube
 
 -- todo square neg_square and neg_pow_bit0
 section
@@ -77,5 +77,4 @@ end
 theorem Int.dvd_mul_cancel_prime' {p k m n : ℤ} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) (hp : Prime p)
     (h : k ∣ p * n) : k ∣ n :=
   Irreducible.dvd_of_dvd_mul_left hdvd1 hdvd2 hp.irreducible h
-#align int.dvd_mul_cancel_prime' Int.dvd_mul_cancel_prime'  
-
+#align int.dvd_mul_cancel_prime' Int.dvd_mul_cancel_prime'

FltRegular/FltThree/Spts.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 import Mathlib.Data.Int.Order.Units
 import Mathlib.NumberTheory.Zsqrtd.Basic
 import Mathlib.RingTheory.Prime
-import FltRegular.FltThree.Primes 
+import FltRegular.FltThree.Primes
 
 theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) :
     ∃ c : ℤ√d, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 :=
@@ -55,7 +55,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime
       ring
     · rw [Zsqrtd.norm_def]
       ring
-  obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im := 
+  obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im :=
     by
     cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;>
       simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
@@ -65,7 +65,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime
       (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
       _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
       _ = 1 := Units.val_one
-      
+
   · set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX
     obtain ⟨U, HU⟩ : (p.norm : ℤ√(-3)) ∣ X :=
       by
@@ -206,7 +206,7 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) :
         ring
       _ < x ^ 2 + 3 * x ^ 2 := (add_lt_add ?_ ?_)
       _ = 4 * x ^ 2 := by ring
-      
+
     · rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow]
       norm_cast
       exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two
@@ -313,7 +313,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
         rw [hz, Int.natAbs_mul]
         exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
       _ < x.natAbs := h3
-      
+
   · rw [← h6]
     exact dvd_mul_of_dvd_right hwdvd x
 #align factors factors
@@ -411,7 +411,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs
         _ = p.norm := by
           rw [Zsqrtd.norm_def]
           ring
-        
+
     · rw [← Int.sub_one_lt_iff, sub_self]
       exact sq_pos_of_ne_zero _ hq
   refine' ⟨_, hq⟩
@@ -423,7 +423,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs
     _ = 1 := by
       rw [hfour]
       norm_num
-    
+
 #align spts.four Spts.four
 
 theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hfour : p.norm = 4) :
@@ -433,4 +433,4 @@ theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (
   rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
   rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
   norm_num at hfour
-#align spts.four_of_coprime Spts.four_of_coprime
+#align spts.four_of_coprime Spts.four_of_coprime