UnitsEquivalent

formal source

 135/-! Bridge Coherence and Categorical Structure -/
 136
 137/-- Units equivalence class: two units packs are equivalent if they have same c -/
 138def UnitsEquivalent (U1 U2 : RSUnits) : Prop :=
 139  U1.c = U2.c ∧ ∃ α : ℝ, α ≠ 0 ∧ U2.tau0 = α * U1.tau0 ∧ U2.ell0 = α * U1.ell0
 140
 141/-- Units equivalence is an equivalence relation -/
 142theorem UnitsEquivalent.refl (U : RSUnits) : UnitsEquivalent U U := by
 143  exact ⟨rfl, 1, by norm_num, by norm_num, by norm_num⟩
 144
 145theorem UnitsEquivalent.symm {U1 U2 : RSUnits} (h : UnitsEquivalent U1 U2) :
 146    UnitsEquivalent U2 U1 := by
 147  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 148  refine ⟨hc.symm, α⁻¹, inv_ne_zero hα, ?_, ?_⟩
 149  · calc U1.tau0 = α⁻¹ * (α * U1.tau0) := by field_simp [hα]
 150      _ = α⁻¹ * U2.tau0 := by rw [hτ]
 151  · calc U1.ell0 = α⁻¹ * (α * U1.ell0) := by field_simp [hα]
 152      _ = α⁻¹ * U2.ell0 := by rw [hℓ]
 153
 154theorem UnitsEquivalent.trans {U1 U2 U3 : RSUnits}
 155    (h12 : UnitsEquivalent U1 U2) (h23 : UnitsEquivalent U2 U3) :
 156    UnitsEquivalent U1 U3 := by
 157  obtain ⟨hc12, α, hα, hτ12, hℓ12⟩ := h12
 158  obtain ⟨hc23, β, hβ, hτ23, hℓ23⟩ := h23
 159  refine ⟨hc12.trans hc23, α * β, mul_ne_zero hα hβ, ?_, ?_⟩
 160  · calc U3.tau0 = β * U2.tau0 := hτ23
 161      _ = β * (α * U1.tau0) := by rw [hτ12]
 162      _ = (α * β) * U1.tau0 := by ring
 163  · calc U3.ell0 = β * U2.ell0 := hℓ23
 164      _ = β * (α * U1.ell0) := by rw [hℓ12]
 165      _ = (α * β) * U1.ell0 := by ring
 166
 167/-- Displays are invariant under units equivalence -/
 168theorem displays_invariant_under_equivalence {U1 U2 : RSUnits}