Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Particles.FlavorPhysics.CKMMatrix.PhaseFreedom public import Physlib.Particles.FlavorPhysics.CKMMatrix.StandardParameterization.Basic

Standard parameters for the CKM Matrix

Given a CKM matrix V we can extract four real numbers θ₁₂, θ₁₃, θ₂₃ and δ₁₃. These, when used in the standard parameterization return V up to equivalence.

This leads to the theorem standParam.exists_for_CKMatrix which says that up to equivalence every CKM matrix can be written using the standard parameterization.

@[expose] public section

Given a CKM matrix V the real number corresponding to sin θ₁₂ in the standard parameterization. -

def S₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V / (√ (VudAbs V ^ 2 + VusAbs V ^ 2))

Given a CKM matrix V the real number corresponding to sin θ₁₃ in the standard parameterization. -

def S₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := VubAbs V

Given a CKM matrix V the real number corresponding to sin θ₂₃ in the standard parameterization. -

def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := if VubAbs V = 1 then VcdAbs V else VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2)

Given a CKM matrix V the real number corresponding to θ₁₂ in the standard parameterization. -

def θ₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₂ V)

Given a CKM matrix V the real number corresponding to θ₁₃ in the standard parameterization. -

def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V)

Given a CKM matrix V the real number corresponding to θ₂₃ in the standard parameterization. -

def θ₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₂₃ V)

Given a CKM matrix V the real number corresponding to cos θ₁₂ in the standard parameterization. -

def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V)

Given a CKM matrix V the real number corresponding to cos θ₁₃ in the standard parameterization. -

def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V)

Given a CKM matrix V the real number corresponding to sin θ₂₃ in the standard parameterization. -

def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V)

Given a CKM matrix V the real number corresponding to the phase δ₁₃ in the standard parameterization. -

def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := arg (Invariant.mulExpδ₁₃ V)

For a CKM matrix sin θ₁₂ is non-negative.

lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := div_nonneg (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg _)

For a CKM matrix sin θ₁₃ is non-negative.

lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V := VAbs_ge_zero 0 2 V

For a CKM matrix sin θ₂₃ is non-negative.

V:Quotient CKMMatrixSetoid⊢ 0 ≤ if VubAbs V = 1 then VcdAbs V else VcbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2) V:Quotient CKMMatrixSetoidh✝:VubAbs V = 1⊢ 0 ≤ VcdAbs VV:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 1⊢ 0 ≤ VcbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2) V:Quotient CKMMatrixSetoidh✝:VubAbs V = 1⊢ 0 ≤ VcdAbs V All goals completed! 🐙 V:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 1⊢ 0 ≤ VcbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2) All goals completed! 🐙

For a CKM matrix sin θ₁₂ is less than or equal to 1.

V:Quotient CKMMatrixSetoid⊢ VusAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2) ≤ 1 All goals completed! 🐙

For a CKM matrix sin θ₁₃ is less than or equal to 1.

lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 := VAbs_leq_one 0 2 V

For a CKM matrix sin θ₂₃ is less than or equal to 1.

V:Quotient CKMMatrixSetoidh✝:¬VubAbs V = 1⊢ VcbAbs V ≤ √(VcbAbs V ^ 2 + VtbAbs V ^ 2) All goals completed! 🐙
lemma S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₂ V) = S₁₂ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid⊢ -1 ≤ 0 All goals completed! 🐙) (S₁₂_nonneg V)) (S₁₂_leq_one V)lemma S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₃ V) = S₁₃ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid⊢ -1 ≤ 0 All goals completed! 🐙) (S₁₃_nonneg V)) (S₁₃_leq_one V)lemma S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₂₃ V) = S₂₃ V := Real.sin_arcsin (le_trans (V:Quotient CKMMatrixSetoid⊢ -1 ≤ 0 All goals completed! 🐙) (S₂₃_nonneg V)) (S₂₃_leq_one V)lemma S₁₂_eq_ℂsin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₂ V) = S₁₂ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₁₂_eq_sin_θ₁₂ V))lemma S₁₃_eq_ℂsin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₃ V) = S₁₃ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₁₃_eq_sin_θ₁₃ V))lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₂₃ V) = S₂₃ V := (ofReal_sin _).symm.trans (congrArg ofReal (S₂₃_eq_sin_θ₂₃ V))V:Quotient CKMMatrixSetoid⊢ ‖S₁₂ V‖ = S₁₂ V All goals completed! 🐙V:Quotient CKMMatrixSetoid⊢ ‖S₁₃ V‖ = S₁₃ V All goals completed! 🐙V:Quotient CKMMatrixSetoid⊢ ‖S₂₃ V‖ = S₂₃ V All goals completed! 🐙lemma S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₂ V = 0 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1⊢ S₁₂ V = 0 All goals completed! 🐙lemma S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₃ V = 1 := haAll goals completed! 🐙All goals completed! 🐙lemma C₁₂_eq_ℂcos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₂ V) = C₁₂ V := V:Quotient CKMMatrixSetoid⊢ cos ↑(θ₁₂ V) = ↑(C₁₂ V) All goals completed! 🐙lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₃ V) = C₁₃ V := V:Quotient CKMMatrixSetoid⊢ cos ↑(θ₁₃ V) = ↑(C₁₃ V) All goals completed! 🐙lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := V:Quotient CKMMatrixSetoid⊢ cos ↑(θ₂₃ V) = ↑(C₂₃ V) All goals completed! 🐙V:Quotient CKMMatrixSetoid⊢ ↑‖C₁₂ V‖ = ↑(C₁₂ V) All goals completed! 🐙V:Quotient CKMMatrixSetoid⊢ ↑‖C₁₃ V‖ = ↑(C₁₃ V) All goals completed! 🐙V:Quotient CKMMatrixSetoid⊢ ↑‖C₂₃ V‖ = ↑(C₂₃ V) All goals completed! 🐙lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := V:Quotient CKMMatrixSetoid⊢ S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 All goals completed! 🐙lemma S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) : S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 := V:Quotient CKMMatrixSetoid⊢ S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 All goals completed! 🐙lemma S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) : S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 := V:Quotient CKMMatrixSetoid⊢ S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 All goals completed! 🐙lemma C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₂ V = 1 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1⊢ C₁₂ V = 1 All goals completed! 🐙lemma C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₃ V = 0 := V:Quotient CKMMatrixSetoidha:VubAbs V = 1⊢ C₁₃ V = 0 All goals completed! 🐙All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙All goals completed! 🐙V:Quotient CKMMatrixSetoidha:VubAbs V ≠ 1⊢ VudAbs V ^ 2 + VusAbs V ^ 2 ≠ 0 All goals completed! 🐙 All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1⊢ VudAbs V = √(VudAbs V ^ 2 + VusAbs V ^ 2) * (VudAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1⊢ VusAbs V = √(VudAbs V ^ 2 + VusAbs V ^ 2) * (VusAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rflV:Quotient CKMMatrixSetoidha:¬VubAbs V = 1⊢ VcbAbs V = √(VudAbs V ^ 2 + VusAbs V ^ 2) * (VcbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidha:¬VubAbs V = 1⊢ VtbAbs V = √(VudAbs V ^ 2 + VusAbs V ^ 2) * (VtbAbs V / √(VudAbs V ^ 2 + VusAbs V ^ 2)) All goals completed! 🐙V:Quotient CKMMatrixSetoidh1:1 - S₁₃ V ^ 2 ≤ 0⊢ S₁₃ V = 1 V:Quotient CKMMatrixSetoidh1:1 - S₁₃ V ^ 2 ≤ 0⊢ 1 ≤ S₁₃ V All goals completed! 🐙V:CKMMatrix⊢ Real.cos (θ₁₂ ⟦V⟧) * Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ S₁₃ ⟦V⟧ = 0 ∨ S₁₂ ⟦V⟧ * Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ S₂₃ ⟦V⟧ * Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ Real.cos (θ₂₃ ⟦V⟧) * Real.cos (θ₁₃ ⟦V⟧) = 0 ↔ Real.cos (θ₁₂ ⟦V⟧) = 0 ∨ Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ Real.cos (θ₂₃ ⟦V⟧) = 0 ∨ S₁₂ ⟦V⟧ = 0 ∨ S₁₃ ⟦V⟧ = 0 ∨ S₂₃ ⟦V⟧ = 0 All goals completed! 🐙lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧) * cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := V:CKMMatrixδ₁₃:ℝ⊢ mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = sin ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) ^ 2 * sin ↑(θ₂₃ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) V:CKMMatrixδ₁₃:ℝ⊢ 0 ≤ Real.sin (θ₁₂ ⟦V⟧)V:CKMMatrixδ₁₃:ℝ⊢ 0 ≤ Real.sin (θ₂₃ ⟦V⟧) V:CKMMatrixδ₁₃:ℝ⊢ 0 ≤ Real.sin (θ₁₂ ⟦V⟧) All goals completed! 🐙 V:CKMMatrixδ₁₃:ℝ⊢ 0 ≤ Real.sin (θ₂₃ ⟦V⟧) All goals completed! 🐙V:CKMMatrixδ₁₃:ℝ⊢ sin ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) ^ 2 * sin ↑(θ₂₃ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = 0 ↔ cos ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = ↑0 ∨ sin ↑(θ₁₃ ⟦V⟧) = ↑0 ∨ sin ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = ↑0 ∨ sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = ↑0 ∨ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = ↑0 V:CKMMatrixδ₁₃:ℝ⊢ ((((sin ↑(θ₁₂ ⟦V⟧) = 0 ∨ cos ↑(θ₁₃ ⟦V⟧) = 0) ∨ sin ↑(θ₂₃ ⟦V⟧) = 0) ∨ sin ↑(θ₁₃ ⟦V⟧) = 0) ∨ cos ↑(θ₁₂ ⟦V⟧) = 0) ∨ cos ↑(θ₂₃ ⟦V⟧) = 0 ↔ (cos ↑(θ₁₂ ⟦V⟧) = 0 ∨ cos ↑(θ₁₃ ⟦V⟧) = 0) ∨ sin ↑(θ₁₃ ⟦V⟧) = 0 ∨ (sin ↑(θ₁₂ ⟦V⟧) = 0 ∨ cos ↑(θ₁₃ ⟦V⟧) = 0) ∨ (sin ↑(θ₂₃ ⟦V⟧) = 0 ∨ cos ↑(θ₁₃ ⟦V⟧) = 0) ∨ cos ↑(θ₂₃ ⟦V⟧) = 0 ∨ cos ↑(θ₁₃ ⟦V⟧) = 0 All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₃ ⟦V⟧) = 0hub:VubAbs ⟦V⟧ = 1⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift δ₁₃ 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift (-δ₁₃) 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙 V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.cos (θ₂₃ ⟦V⟧) = 0⊢ sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0 V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) i j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 0 * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 0) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₂ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) i j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 δ₁₃ δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 (-δ₁₃) (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (sin ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₂₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₁₂ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ All goals completed! 🐙lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) : standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ = phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0i:Fin 3j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) i j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) i j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) jV:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0j:Fin 3⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) j = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) j V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨0, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨1, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨0, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨1, ⋯⟩)V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ ↑(standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) = ↑(phaseShift 0 0 δ₁₃ * standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 * phaseShift 0 0 (-δ₁₃)) ((fun i => i) ⟨2, ⋯⟩) ((fun i => i) ⟨2, ⋯⟩) V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (cos ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧) * cexp (I * ↑δ₁₃) = cexp (I * ↑δ₁₃) * (sin ↑(θ₁₂ ⟦V⟧) * sin ↑(θ₁₃ ⟦V⟧) * cos ↑(θ₂₃ ⟦V⟧))V:CKMMatrixδ₁₃:ℝh:Real.sin (θ₂₃ ⟦V⟧) = 0⊢ cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧) = cexp (I * ↑δ₁₃) * (cos ↑(θ₂₃ ⟦V⟧) * cos ↑(θ₁₃ ⟦V⟧)) * (cexp (I * ↑δ₁₃))⁻¹ All goals completed! 🐙V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ ↑(VtbAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) + -↑(VubAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) * ↑(VcbAbs ⟦V⟧) / (↑(VudAbs ⟦V⟧) ^ 2 + ↑(VusAbs ⟦V⟧) ^ 2) * cexp (-↑(↑V 0 2).arg * I) = ↑(VudAbs ⟦V⟧ / √(VudAbs ⟦V⟧ ^ 2 + VusAbs ⟦V⟧ ^ 2)) * ↑(VtbAbs ⟦V⟧ / √(VudAbs ⟦V⟧ ^ 2 + VusAbs ⟦V⟧ ^ 2)) - ↑(VusAbs ⟦V⟧ / √(VudAbs ⟦V⟧ ^ 2 + VusAbs ⟦V⟧ ^ 2)) * ↑(VubAbs ⟦V⟧) * ↑(VcbAbs ⟦V⟧ / √(VudAbs ⟦V⟧ ^ 2 + VusAbs ⟦V⟧ ^ 2)) * cexp (-(I * ↑(↑V 0 2).arg)) V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ ↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) + -(↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧)) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) * cexp (-(↑(↑V 0 2).arg * I)) = ↑(VAbs 0 0 ⟦V⟧) / ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * (↑(VAbs 2 2 ⟦V⟧) / ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) - ↑(VAbs 0 1 ⟦V⟧) / ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑(VAbs 0 2 ⟦V⟧) * (↑(VAbs 1 2 ⟦V⟧) / ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) * cexp (-(I * ↑(↑V 0 2).arg)) V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + -(↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I)))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) = (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) - ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I))) / ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ^ 2 conv_rhs => V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0| (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) - ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + -(↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I)))) / (↑(VAbs 0 0 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧)) = (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) - ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I))) / (↑(VAbs 0 0 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 1 ⟦V⟧)) V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) + -(↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I)))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) = (↑(VAbs 2 2 ⟦V⟧) * ↑(VAbs 0 0 ⟦V⟧) - ↑(VAbs 0 1 ⟦V⟧) * ↑(VAbs 0 2 ⟦V⟧) * ↑(VAbs 1 2 ⟦V⟧) * cexp (-(↑(↑V 0 2).arg * I))) / (↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2) All goals completed! 🐙 V:CKMMatrixhb:↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0hV:V.FstRowThdColRealCondhb':VubAbs ⟦V⟧ ≠ 1h1:↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) * ↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) = ↑(VAbs 0 0 ⟦V⟧) ^ 2 + ↑(VAbs 0 1 ⟦V⟧) ^ 2hx:↑(VudAbs ⟦V⟧) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧) ≠ 0⊢ [V]c ((fun i => i) ⟨2, ⋯⟩) = [standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (-(↑V 0 2).arg)]c ((fun i => i) ⟨2, ⋯⟩) All goals completed! 🐙V:CKMMatrixhV:V.ubOnePhaseCondh1:VubAbs ⟦V⟧ = 1⊢ 0 = sin ↑(θ₂₃ ⟦V⟧) * ↑0 All goals completed! 🐙V:CKMMatrixU:CKMMatrixhU:V ≈ U ∧ U.FstRowThdColRealCondhUV:⟦U⟧ = ⟦V⟧ha:¬(↑V 0 0 ≠ 0 ∨ ↑V 0 1 ≠ 0)haU:¬(↑U 0 0 ≠ 0 ∨ ↑U 0 1 ≠ 0)U2:CKMMatrixhU2:U ≈ U2 ∧ U2.ubOnePhaseCondhUVa2:V ≈ U2hUV2:⟦U2⟧ = ⟦V⟧hx:U2 = standParam (θ₁₂ ⟦U2⟧) (θ₁₃ ⟦U2⟧) (θ₂₃ ⟦U2⟧) 0⊢ V ≈ U2 All goals completed! 🐙theorem exists_for_CKMatrix (V : CKMMatrix) : ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := V:CKMMatrix⊢ ∃ θ₁₂ θ₁₃ θ₂₃ δ₁₃, V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ V:CKMMatrix⊢ V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) All goals completed! 🐙