From 99a915d31583e4538dd2ef0ece6b2cb463da4582 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 27 Jun 2024 08:49:13 -0400
Subject: [PATCH] style: Remove some extra spaces

---
 HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index 90dbf32..974f81d 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -224,7 +224,6 @@ lemma ubOnePhaseCond_shift_solution {V : CKMMatrix} (h1 : a + f = - arg [V]ub)
   subst hc
   ring
 
--- rename
 lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
     ∃ (U : CKMMatrix), V ≈ U ∧ FstRowThdColRealCond U:= by
   obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow
@@ -319,7 +318,6 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
     ring
   rw [hcs, hUV, cs_of_ud_us_zero hb]
 
-
 lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
     (hV : FstRowThdColRealCond V) :
     [V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +