toRatCore

formal source

 196two `Rat` values are equal. -/
 197
 198/-- Map a `PreRat` to `Rat`. -/
 199def toRatCore : PreRat → ℚ :=
 200  fun p => (toInt p.num : ℚ) / (toInt p.den : ℚ)
 201
 202theorem toRatCore_respects :
 203    ∀ p q : PreRat, p ≈ q → toRatCore p = toRatCore q := by
 204  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ h
 205  show (toInt a : ℚ) / toInt b = (toInt c : ℚ) / toInt d
 206  have hb_int : (toInt b : ℚ) ≠ 0 := by
 207    intro habs
 208    apply hb
 209    rw [eq_iff_toInt_eq, toInt_zero]
 210    exact_mod_cast habs
 211  have hd_int : (toInt d : ℚ) ≠ 0 := by
 212    intro habs
 213    apply hd
 214    rw [eq_iff_toInt_eq, toInt_zero]
 215    exact_mod_cast habs
 216  have h' : toInt a * toInt d = toInt c * toInt b := by
 217    have := congrArg toInt (show a * d = c * b from h)
 218    rwa [toInt_mul, toInt_mul] at this
 219  rw [div_eq_div_iff hb_int hd_int]
 220  exact_mod_cast h'
 221
 222/-- The recovery map `LogicRat → Rat`. -/
 223def toRat : LogicRat → ℚ := Quotient.lift toRatCore toRatCore_respects
 224
 225/-- The inverse `Rat → LogicRat`. -/
 226noncomputable def fromRat (q : ℚ) : LogicRat :=
 227  let n : LogicInt := fromInt q.num
 228  let d : LogicInt := fromInt q.den
 229  mk n d (by