Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โCtrl+โto navigate, Ctrl+๐ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl.
```import Std.Data.Int.Lemmas
import Std.Data.Rat.Basic

namespace Rat

@[simp] theorem maybeNormalize_eq: โ {num : Int} {den g : Nat} (den_nz : den / g โ  0) (reduced : Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)),
maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)maybeNormalize_eq {num: ?m.2num den: ?m.5den g: ?m.8g} (den_nz: ?m.11den_nz reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)reduced) :
maybeNormalize: (num : Int) โ (den g : Nat) โ den / g โ  0 โ Nat.coprime (Int.natAbs (Int.div num โg)) (den / g) โ RatmaybeNormalize num: ?m.2num den: ?m.5den g: ?m.8g den_nz: ?m.11den_nz reduced: ?m.14reduced =
{ num := num: ?m.2num.div: Int โ Int โ Intdiv g: ?m.8g, den := den: ?m.5den / g: ?m.8g, den_nz: ?m.11den_nz, reduced } := byGoals accomplished! ๐
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)unfold maybeNormalize: (num : Int) โ (den g : Nat) โ den / g โ  0 โ Nat.coprime (Int.natAbs (Int.div num โg)) (den / g) โ RatmaybeNormalizenum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)(if hg : g = 1 then mk' num den else mk' (Int.div num โg) (den / g)) = mk' (Int.div num โg) (den / g);num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)(if hg : g = 1 then mk' num den else mk' (Int.div num โg) (den / g)) = mk' (Int.div num โg) (den / g) num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)splitnum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: g = 1inlmk' num den = mk' (Int.div num โg) (den / g)num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: ยฌg = 1inrmk' (Int.div num โg) (den / g) = mk' (Int.div num โg) (den / g)
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)ยทnum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: g = 1inlmk' num den = mk' (Int.div num โg) (den / g) num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: g = 1inlmk' num den = mk' (Int.div num โg) (den / g)num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: ยฌg = 1inrmk' (Int.div num โg) (den / g) = mk' (Int.div num โg) (den / g)subst g: Natgnum: Intden: Natden_nz: den / 1 โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โ1)) (den / 1)inlmk' num den = mk' (Int.div num โ1) (den / 1);num: Intden: Natden_nz: den / 1 โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โ1)) (den / 1)inlmk' num den = mk' (Int.div num โ1) (den / 1) num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: g = 1inlmk' num den = mk' (Int.div num โg) (den / g)simpGoals accomplished! ๐
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)ยทnum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: ยฌg = 1inrmk' (Int.div num โg) (den / g) = mk' (Int.div num โg) (den / g) num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hโ: ยฌg = 1inrmk' (Int.div num โg) (den / g) = mk' (Int.div num โg) (den / g)rflGoals accomplished! ๐

theorem normalize.reduced': โ {num : Int} {den g : Nat}, den โ  0 โ g = Nat.gcd (Int.natAbs num) den โ Nat.coprime (Int.natAbs (num / โg)) (den / g)normalize.reduced' {num: Intnum : Int: TypeInt} {den: Natden g: Natg : Nat: TypeNat} (den_nz: den โ  0den_nz : den: Natden โ  0: ?m.6840)
(e: g = Nat.gcd (Int.natAbs num) dene : g: Natg = num: Intnum.natAbs: Int โ NatnatAbs.gcd: Nat โ Nat โ Natgcd den: Natden) : (num: Intnum / g: Natg).natAbs: Int โ NatnatAbs.coprime: Nat โ Nat โ Propcoprime (den: Natden / g: Natg) := byGoals accomplished! ๐
num: Intden, g: Natden_nz: den โ  0e: g = Nat.gcd (Int.natAbs num) denNat.coprime (Int.natAbs (num / โg)) (den / g)rw [num: Intden, g: Natden_nz: den โ  0e: g = Nat.gcd (Int.natAbs num) denNat.coprime (Int.natAbs (num / โg)) (den / g)โ Int.div_eq_ediv_of_dvd: โ {a b : Int}, b โฃ a โ Int.div a b = a / bInt.div_eq_ediv_of_dvd (e: g = Nat.gcd (Int.natAbs num) dene โธ Int.ofNat_dvd_left: โ {n : Nat} {z : Int}, โn โฃ z โ n โฃ Int.natAbs zInt.ofNat_dvd_left.2: โ {a b : Prop}, (a โ b) โ b โ a2 (Nat.gcd_dvd_left: โ (m n : Nat), Nat.gcd m n โฃ mNat.gcd_dvd_left ..))num: Intden, g: Natden_nz: den โ  0e: g = Nat.gcd (Int.natAbs num) denNat.coprime (Int.natAbs (Int.div num โg)) (den / g)]num: Intden, g: Natden_nz: den โ  0e: g = Nat.gcd (Int.natAbs num) denNat.coprime (Int.natAbs (Int.div num โg)) (den / g)
num: Intden, g: Natden_nz: den โ  0e: g = Nat.gcd (Int.natAbs num) denNat.coprime (Int.natAbs (num / โg)) (den / g)exact normalize.reduced: โ {num : Int} {den g : Nat},
den โ  0 โ g = Nat.gcd (Int.natAbs num) den โ Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)normalize.reduced den_nz: den โ  0den_nz e: g = Nat.gcd (Int.natAbs num) deneGoals accomplished! ๐

theorem normalize_eq: โ {num : Int} {den : Nat} (den_nz : den โ  0),
normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)normalize_eq {num: ?m.905num den: Natden} (den_nz: ?m.911den_nz) : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: ?m.905num den: ?m.908den den_nz: ?m.911den_nz =
{ num := num: ?m.905num / num: ?m.905num.natAbs: Int โ NatnatAbs.gcd: Nat โ Nat โ Natgcd den: ?m.908den
den := den: ?m.908den / num: ?m.905num.natAbs: Int โ NatnatAbs.gcd: Nat โ Nat โ Natgcd den: ?m.908den
den_nz := normalize.den_nz: โ {num : Int} {den g : Nat}, den โ  0 โ g = Nat.gcd (Int.natAbs num) den โ den / g โ  0normalize.den_nz den_nz: ?m.911den_nz rfl: โ {ฮฑ : Sort ?u.1057} {a : ฮฑ}, a = arfl
reduced := normalize.reduced': โ {num : Int} {den g : Nat}, den โ  0 โ g = Nat.gcd (Int.natAbs num) den โ Nat.coprime (Int.natAbs (num / โg)) (den / g)normalize.reduced' den_nz: ?m.911den_nz rfl: โ {ฮฑ : Sort ?u.1076} {a : ฮฑ}, a = arfl } := byGoals accomplished! ๐
num: Intden: Natden_nz: den โ  0normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)simp only [normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize, maybeNormalize_eq: โ {num : Int} {den g : Nat} (den_nz : den / g โ  0) (reduced : Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)),
maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)maybeNormalize_eq,
Int.div_eq_ediv_of_dvd: โ {a b : Int}, b โฃ a โ Int.div a b = a / bInt.div_eq_ediv_of_dvd (Int.ofNat_dvd_left: โ {n : Nat} {z : Int}, โn โฃ z โ n โฃ Int.natAbs zInt.ofNat_dvd_left.2: โ {a b : Prop}, (a โ b) โ b โ a2 (Nat.gcd_dvd_left: โ (m n : Nat), Nat.gcd m n โฃ mNat.gcd_dvd_left ..))]Goals accomplished! ๐

@[simp] theorem normalize_zero: โ {d : Nat} (nz : d โ  0), normalize 0 d = 0normalize_zero (nz: d โ  0nz) : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize 0: ?m.13780 d: ?m.1370d nz: ?m.1373nz = 0: ?m.13810 := byGoals accomplished! ๐
d: Natnz: d โ  0normalize 0 d = 0simp [normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize, Int.zero_div: โ (b : Int), Int.div 0 b = 0Int.zero_div, Int.natAbs_zero: Int.natAbs 0 = 0Int.natAbs_zero, Nat.div_self: โ {n : Nat}, 0 < n โ n / n = 1Nat.div_self (Nat.pos_of_ne_zero: โ {n : Nat}, n โ  0 โ 0 < nNat.pos_of_ne_zero nz: d โ  0nz)]d: Natnz: d โ  0mk' 0 1 = 0;d: Natnz: d โ  0mk' 0 1 = 0 d: Natnz: d โ  0normalize 0 d = 0rflGoals accomplished! ๐

theorem mk_eq_normalize: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num denmk_eq_normalize (num: ?m.1668num den: Natden nz: den โ  0nz c: Nat.coprime (Int.natAbs num) denc) : โจnum: ?m.1668num, den: ?m.1671den, nz: ?m.1674nz, c: ?m.1677cโฉ = normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: ?m.1668num den: ?m.1671den nz: ?m.1674nz := byGoals accomplished! ๐
num: Intden: Natnz: den โ  0c: Nat.coprime (Int.natAbs num) denmk' num den = normalize num densimp [normalize_eq: โ {num : Int} {den : Nat} (den_nz : den โ  0),
normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)normalize_eq, c: Nat.coprime (Int.natAbs num) denc.gcd_eq_one: โ {m n : Nat}, Nat.coprime m n โ Nat.gcd m n = 1gcd_eq_one]Goals accomplished! ๐

theorem normalize_self: โ (r : Rat), normalize r.num r.den = rnormalize_self (r: Ratr : Rat: TypeRat) : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize r: Ratr.num: Rat โ Intnum r: Ratr.den: Rat โ Natden r: Ratr.den_nz: โ (self : Rat), self.den โ  0den_nz = r: Ratr := (mk_eq_normalize: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num denmk_eq_normalize ..).symm: โ {ฮฑ : Sort ?u.2002} {a b : ฮฑ}, a = b โ b = asymm

theorem normalize_mul_left: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (โa * n) (a * d) = normalize n dnormalize_mul_left {a: Nata : Nat: TypeNat} (d0: d โ  0d0 : d: ?m.2026d โ  0: ?m.20740) (a0: a โ  0a0 : a: Nata โ  0: ?m.20880) :
normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize (โa: Nata * n: ?m.2066n) (a: Nata * d: ?m.2026d) (Nat.mul_ne_zero: โ {n m : Nat}, n โ  0 โ m โ  0 โ n * m โ  0Nat.mul_ne_zero a0: a โ  0a0 d0: d โ  0d0) = normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize n: ?m.2066n d: ?m.2026d d0: d โ  0d0 := byGoals accomplished! ๐
d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (โa * n) (a * d) = normalize n dsimp [normalize_eq: โ {num : Int} {den : Nat} (den_nz : den โ  0),
normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)normalize_eq, mk'.injEq: โ (num : Int) (den : Nat) (den_nz : autoParam (den โ  0) _autoโ)
(reduced : autoParam (Nat.coprime (Int.natAbs num) den) _autoโยน) (num_1 : Int) (den_1 : Nat)
(den_nz_1 : autoParam (den_1 โ  0) _autoโ) (reduced_1 : autoParam (Nat.coprime (Int.natAbs num_1) den_1) _autoโยน),
(mk' num den = mk' num_1 den_1) = (num = num_1 โง den = den_1)mk'.injEq, Int.natAbs_mul: โ (a b : Int), Int.natAbs (a * b) = Int.natAbs a * Int.natAbs bInt.natAbs_mul, Nat.gcd_mul_left: โ (m n k : Nat), Nat.gcd (m * n) (m * k) = m * Nat.gcd n kNat.gcd_mul_left,
Nat.mul_div_mul_left: โ {m : Nat} (n k : Nat), 0 < m โ m * n / (m * k) = n / kNat.mul_div_mul_left _: Nat_ _: Nat_ (Nat.pos_of_ne_zero: โ {n : Nat}, n โ  0 โ 0 < nNat.pos_of_ne_zero a0: a โ  0a0), Int.ofNat_mul: โ (n m : Nat), โ(n * m) = โn * โmInt.ofNat_mul,
Int.mul_ediv_mul_of_pos: โ {a : Int} (b c : Int), 0 < a โ a * b / (a * c) = b / cInt.mul_ediv_mul_of_pos _: Int_ _: Int_ (Int.ofNat_pos: โ {n : Nat}, 0 < โn โ 0 < nInt.ofNat_pos.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.pos_of_ne_zero: โ {n : Nat}, n โ  0 โ 0 < nNat.pos_of_ne_zero a0: a โ  0a0)]Goals accomplished! ๐

theorem normalize_mul_right: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (n * โa) (d * a) = normalize n dnormalize_mul_right {a: Nata : Nat: TypeNat} (d0: d โ  0d0 : d: ?m.2780d โ  0: ?m.28250) (a0: a โ  0a0 : a: Nata โ  0: ?m.28390) :
normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize (n: ?m.2817n * a: Nata) (d: ?m.2780d * a: Nata) (Nat.mul_ne_zero: โ {n m : Nat}, n โ  0 โ m โ  0 โ n * m โ  0Nat.mul_ne_zero d0: d โ  0d0 a0: a โ  0a0) = normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize n: ?m.2817n d: ?m.2780d d0: d โ  0d0 := byGoals accomplished! ๐
d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize n drw [d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize n dโ normalize_mul_left: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (โa * n) (a * d) = normalize n dnormalize_mul_left (d0 := d0: d โ  0d0) a0: a โ  0a0d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize (โa * n) (a * d)]d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize (โa * n) (a * d);d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize (โa * n) (a * d) d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize n dcongr 1d: Natn: Inta: Natd0: d โ  0a0: a โ  0e_numn * โa = โa * nd: Natn: Inta: Natd0: d โ  0a0: a โ  0e_dend * a = a * d <;> [d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize (โa * n) (a * d)apply Int.mul_comm: โ (a b : Int), a * b = b * aInt.mul_commGoals accomplished! ๐; d: Natn: Inta: Natd0: d โ  0a0: a โ  0normalize (n * โa) (d * a) = normalize (โa * n) (a * d)apply Nat.mul_comm: โ (n m : Nat), n * m = m * nNat.mul_commGoals accomplished! ๐]Goals accomplished! ๐

theorem normalize_eq_iff: โ {dโ dโ : Nat} {nโ nโ : Int} (zโ : dโ โ  0) (zโ : dโ โ  0), normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโnormalize_eq_iff (zโ: dโ โ  0zโ : dโ: ?m.3267dโ โ  0: unknown metavariable '?_uniq.3326'0) (zโ: dโ โ  0zโ : dโ: ?m.3287dโ โ  0: ?m.33820) :
normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize nโ: ?m.3320nโ dโ: ?m.3267dโ zโ: dโ โ  0zโ = normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize nโ: ?m.3362nโ dโ: ?m.3287dโ zโ: dโ โ  0zโ โ nโ: ?m.3320nโ * dโ: ?m.3287dโ = nโ: ?m.3362nโ * dโ: ?m.3267dโ := byGoals accomplished! ๐
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโconstructordโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mpnormalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mprnโ * โdโ = nโ * โdโ โ normalize nโ dโ = normalize nโ dโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโ<;>dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mpnormalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mprnโ * โdโ = nโ * โdโ โ normalize nโ dโ = normalize nโ dโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโintro h: ?ahdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโยทdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโsimp only [normalize_eq: โ {num : Int} {den : Nat} (den_nz : den โ  0),
normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)normalize_eq, mk'.injEq: โ (num : Int) (den : Nat) (den_nz : autoParam (den โ  0) _autoโ)
(reduced : autoParam (Nat.coprime (Int.natAbs num) den) _autoโยน) (num_1 : Int) (den_1 : Nat)
(den_nz_1 : autoParam (den_1 โ  0) _autoโ) (reduced_1 : autoParam (Nat.coprime (Int.natAbs num_1) den_1) _autoโยน),
(mk' num den = mk' num_1 den_1) = (num = num_1 โง den = den_1)mk'.injEq] at h: ?ahdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโmpnโ * โdโ = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโhave' hnโ: ?m.3810hnโ := Int.ofNat_dvd_left: โ {n : Nat} {z : Int}, โn โฃ z โ n โฃ Int.natAbs zInt.ofNat_dvd_left.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.gcd_dvd_left: โ (m n : Nat), Nat.gcd m n โฃ mNat.gcd_dvd_left nโ: Intnโ.natAbs: Int โ NatnatAbs dโ: Natdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโmpnโ * โdโ = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโhave' hnโ: ?m.3826hnโ := Int.ofNat_dvd_left: โ {n : Nat} {z : Int}, โn โฃ z โ n โฃ Int.natAbs zInt.ofNat_dvd_left.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.gcd_dvd_left: โ (m n : Nat), Nat.gcd m n โฃ mNat.gcd_dvd_left nโ: Intnโ.natAbs: Int โ NatnatAbs dโ: Natdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโmpnโ * โdโ = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโhave' hdโ: ?m.3837hdโ := Int.ofNat_dvd: โ {m n : Nat}, โm โฃ โn โ m โฃ nInt.ofNat_dvd.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.gcd_dvd_right: โ (m n : Nat), Nat.gcd m n โฃ nNat.gcd_dvd_right nโ: Intnโ.natAbs: Int โ NatnatAbs dโ: Natdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโhave' hdโ: ?m.3848hdโ := Int.ofNat_dvd: โ {m n : Nat}, โm โฃ โn โ m โฃ nInt.ofNat_dvd.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.gcd_dvd_right: โ (m n : Nat), Nat.gcd m n โฃ nNat.gcd_dvd_right nโ: Intnโ.natAbs: Int โ NatnatAbs dโ: Natdโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: normalize nโ dโ = normalize nโ dโmpnโ * โdโ = nโ * โdโrw [dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโโ Int.ediv_mul_cancel: โ {a b : Int}, b โฃ a โ a / b * b = aInt.ediv_mul_cancel (Int.dvd_trans: โ {a b c : Int}, a โฃ b โ b โฃ c โ a โฃ cInt.dvd_trans hdโ: ?m.3848hdโ (Int.dvd_mul_left: โ (a b : Int), b โฃ a * bInt.dvd_mul_left ..)),dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ / โ(Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโInt.mul_ediv_assoc: โ (a : Int) {b c : Int}, c โฃ b โ a * b / c = a * (b / c)Int.mul_ediv_assoc _: Int_ hdโ: ?m.3848hdโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * (โdโ / โ(Nat.gcd (Int.natAbs nโ) dโ)) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโโ Int.ofNat_ediv: โ (m n : Nat), โ(m / n) = โm / โnInt.ofNat_ediv,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โ(dโ / Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโโ h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโh.2: โ {a b : Prop}, a โง b โ b2,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โ(dโ / Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโInt.ofNat_ediv: โ (m n : Nat), โ(m / n) = โm / โnInt.ofNat_ediv,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * (โdโ / โ(Nat.gcd (Int.natAbs nโ) dโ)) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโโ Int.mul_ediv_assoc: โ (a : Int) {b c : Int}, c โฃ b โ a * b / c = a * (b / c)Int.mul_ediv_assoc _: Int_ hdโ: ?m.3837hdโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ / โ(Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโInt.mul_ediv_assoc': โ (b : Int) {a c : Int}, c โฃ a โ a * b / c = a / c * bInt.mul_ediv_assoc' _: Int_ hnโ: ?m.3810hnโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ / โ(Nat.gcd (Int.natAbs nโ) dโ) * โdโ * โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ * โdโ
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโInt.mul_right_comm: โ (a b c : Int), a * b * c = a * c * bInt.mul_right_comm,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ / โ(Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) * โdโ = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโh: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโh.1: โ {a b : Prop}, a โง b โ a1,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ / โ(Nat.gcd (Int.natAbs nโ) dโ) * โ(Nat.gcd (Int.natAbs nโ) dโ) * โdโ = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโInt.ediv_mul_cancel: โ {a b : Int}, b โฃ a โ a / b * b = aInt.ediv_mul_cancel hnโ: ?m.3826hnโdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) = nโ / โ(Nat.gcd (Int.natAbs nโ) dโ) โง   dโ / Nat.gcd (Int.natAbs nโ) dโ = dโ / Nat.gcd (Int.natAbs nโ) dโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhnโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ nโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโhdโ: โ(Nat.gcd (Int.natAbs nโ) dโ) โฃ โdโmpnโ * โdโ = nโ * โdโ]Goals accomplished! ๐
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโยทdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโrw [dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโโ normalize_mul_right: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (n * โa) (d * a) = normalize n dnormalize_mul_right _: ?m.3954 โ  0_ zโ: dโ โ  0zโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize (nโ * โdโ) (dโ * dโ) = normalize nโ dโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโโ normalize_mul_left: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (โa * n) (a * d) = normalize n dnormalize_mul_left zโ: dโ โ  0zโ zโ: dโ โ  0zโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize (nโ * โdโ) (dโ * dโ) = normalize (โdโ * nโ) (dโ * dโ) dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโInt.mul_comm: โ (a b : Int), a * b = b * aInt.mul_comm dโ: Natdโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize (nโ * โdโ) (dโ * dโ) = normalize (nโ * โdโ) (dโ * dโ) dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize nโ dโ = normalize nโ dโh: ?bhdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0h: nโ * โdโ = nโ * โdโmprnormalize (nโ * โdโ) (dโ * dโ) = normalize (nโ * โdโ) (dโ * dโ)]Goals accomplished! ๐

theorem maybeNormalize_eq_normalize: โ {num : Int} {den g : Nat} (den_nz : den / g โ  0) (reduced : Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)),
โg โฃ num โ g โฃ den โ maybeNormalize num den g den_nz reduced = normalize num denmaybeNormalize_eq_normalize {num: Intnum : Int: TypeInt} {den: Natden g: Natg : Nat: TypeNat} (den_nz: den / g โ  0den_nz reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)reduced)
(hn: ?m.4055 โฃ numhn : โg: Natg โฃ num: Intnum) (hd: g โฃ denhd : g: Natg โฃ den: Natden) :
maybeNormalize: (num : Int) โ (den g : Nat) โ den / g โ  0 โ Nat.coprime (Int.natAbs (Int.div num โg)) (den / g) โ RatmaybeNormalize num: Intnum den: Natden g: Natg den_nz: ?m.4044den_nz reduced: ?m.4047reduced = normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: Intnum den: Natden (mt: โ {a b : Prop}, (a โ b) โ ยฌb โ ยฌamt (: den = 0 โ den / g = 0(by: den = 0 โ den / g = 0byGoals accomplished! ๐ simp [ยท]): den = 0 โ den / g = 0  simp [ยท]): den = 0 โ den / g = 0simp simp [ยท]): den = 0 โ den / g = 0 [ยท]) den_nz: ?m.4044den_nz) := byGoals accomplished! ๐
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denmaybeNormalize num den g den_nz reduced = normalize num densimp only [maybeNormalize_eq: โ {num : Int} {den g : Nat} (den_nz : den / g โ  0) (reduced : Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)),
maybeNormalize num den g den_nz reduced = mk' (Int.div num โg) (den / g)maybeNormalize_eq, mk_eq_normalize: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num denmk_eq_normalize, Int.div_eq_ediv_of_dvd: โ {a b : Int}, b โฃ a โ Int.div a b = a / bInt.div_eq_ediv_of_dvd hn: โg โฃ numhn]num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ dennormalize (num / โg) (den / g) = normalize num den
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denmaybeNormalize num den g den_nz reduced = normalize num denhave : g: Natg โ  0: ?m.44130 := mt: โ {a b : Prop}, (a โ b) โ ยฌb โ ยฌamt (: g = 0 โ den / g = 0(num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ dennormalize (num / โg) (den / g) = normalize num denby: g = 0 โ den / g = 0byGoals accomplished! ๐ simp [ยท]): g = 0 โ den / g = 0  simp [ยท]): g = 0 โ den / g = 0simp simp [ยท]): g = 0 โ den / g = 0 [ยท]) den_nz: den / g โ  0den_nznum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize (num / โg) (den / g) = normalize num den
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denmaybeNormalize num den g den_nz reduced = normalize num denrw [num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize (num / โg) (den / g) = normalize num denโ normalize_mul_right: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (n * โa) (d * a) = normalize n dnormalize_mul_right _: ?m.4446 โ  0_ this: g โ  0this,num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize (num / โg * โg) (den / g * g) = normalize num den num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize (num / โg) (den / g) = normalize num denInt.ediv_mul_cancel: โ {a b : Int}, b โฃ a โ a / b * b = aInt.ediv_mul_cancel hn: โg โฃ numhnnum: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize num (den / g * g) = normalize num den]num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0normalize num (den / g * g) = normalize num den
num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denmaybeNormalize num den g den_nz reduced = normalize num dencongr 1num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0e_denden / g * g = den;num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denthis: g โ  0e_denden / g * g = den num: Intden, g: Natden_nz: den / g โ  0reduced: Nat.coprime (Int.natAbs (Int.div num โg)) (den / g)hn: โg โฃ numhd: g โฃ denmaybeNormalize num den g den_nz reduced = normalize num denexact Nat.div_mul_cancel: โ {n m : Nat}, n โฃ m โ m / n * n = mNat.div_mul_cancel hd: g โฃ denhdGoals accomplished! ๐

@[simp] theorem normalize_eq_zero: โ {d : Nat} {n : Int} (d0 : d โ  0), normalize n d = 0 โ n = 0normalize_eq_zero (d0: d โ  0d0 : d: ?m.4799d โ  0: unknown metavariable '?_uniq.4805'0) : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize n: ?m.4818n d: ?m.4799d d0: d โ  0d0 = 0: ?m.48460 โ n: ?m.4818n = 0: ?m.48640 := byGoals accomplished! ๐
d: Natn: Intd0: d โ  0normalize n d = 0 โ n = 0have' := normalize_eq_iff: โ {dโ dโ : Nat} {nโ nโ : Int} (zโ : dโ โ  0) (zโ : dโ โ  0), normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโnormalize_eq_iff d0: d โ  0d0 Nat.one_ne_zero: 1 โ  0Nat.one_ne_zerod: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = normalize ?refine'_2 1 โ ?refine'_1 * โ1 = ?refine'_2 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_2Int
d: Natn: Intd0: d โ  0normalize n d = 0 โ n = 0rw [d: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = normalize ?refine'_2 1 โ ?refine'_1 * โ1 = ?refine'_2 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_2Intnormalize_zero: โ {d : Nat} (nz : d โ  0), normalize 0 d = 0normalize_zero (d := 1: ?m.49011)d: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_1Int]d: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_1Int at this: ?m.4887thisd: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_1Int;d: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_1Int d: Natn: Intd0: d โ  0normalize n d = 0 โ n = 0rw [d: Natn: Intd0: d โ  0this: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdrefine'_3normalize n d = 0 โ n = 0d: Natn: Intd0: d โ  0refine'_1Intd: Natn: Intd0: d โ  0refine'_1Intthis: normalize ?refine'_1 d = 0 โ ?refine'_1 * โ1 = 0 * โdthisd: Natn: Intd0: d โ  0this: normalize n d = 0 โ n * โ1 = 0 * โdrefine'_3n * โ1 = 0 * โd โ n = 0]d: Natn: Intd0: d โ  0this: normalize n d = 0 โ n * โ1 = 0 * โdrefine'_3n * โ1 = 0 * โd โ n = 0;d: Natn: Intd0: d โ  0this: normalize n d = 0 โ n * โ1 = 0 * โdrefine'_3n * โ1 = 0 * โd โ n = 0 d: Natn: Intd0: d โ  0normalize n d = 0 โ n = 0simpGoals accomplished! ๐

theorem normalize_num_den': โ (num : Int) (den : Nat) (nz : den โ  0),
โ d, d โ  0 โง num = (normalize num den).num * โd โง den = (normalize num den).den * dnormalize_num_den' (num: Intnum den: ?m.5050den nz: ?m.5053nz) : โ d: Natd : Nat: TypeNat, d: Natd โ  0: ?m.50630 โง
num: ?m.5047num = (normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: ?m.5047num den: ?m.5050den nz: ?m.5053nz).num: Rat โ Intnum * d: Natd โง den: ?m.5050den = (normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: ?m.5047num den: ?m.5050den nz: ?m.5053nz).den: Rat โ Natden * d: Natd := byGoals accomplished! ๐
num: Intden: Natnz: den โ  0โ d, d โ  0 โง num = (normalize num den).num * โd โง den = (normalize num den).den * drefine โจnum: Intnum.natAbs: Int โ NatnatAbs.gcd: Nat โ Nat โ Natgcd den: Natden, Nat.gcd_ne_zero_right: โ {n m : Nat}, n โ  0 โ Nat.gcd m n โ  0Nat.gcd_ne_zero_right nz: den โ  0nz, ?_: ?m.5223?_โฉnum: Intden: Natnz: den โ  0num = (normalize num den).num * โ(Nat.gcd (Int.natAbs num) den) โง   den = (normalize num den).den * Nat.gcd (Int.natAbs num) den
num: Intden: Natnz: den โ  0โ d, d โ  0 โง num = (normalize num den).num * โd โง den = (normalize num den).den * dsimp [normalize_eq: โ {num : Int} {den : Nat} (den_nz : den โ  0),
normalize num den = mk' (num / โ(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)normalize_eq, Int.ediv_mul_cancel: โ {a b : Int}, b โฃ a โ a / b * b = aInt.ediv_mul_cancel (Int.ofNat_dvd_left: โ {n : Nat} {z : Int}, โn โฃ z โ n โฃ Int.natAbs zInt.ofNat_dvd_left.2: โ {a b : Prop}, (a โ b) โ b โ a2 <| Nat.gcd_dvd_left: โ (m n : Nat), Nat.gcd m n โฃ mNat.gcd_dvd_left ..),
Nat.div_mul_cancel: โ {n m : Nat}, n โฃ m โ m / n * n = mNat.div_mul_cancel (Nat.gcd_dvd_right: โ (m n : Nat), Nat.gcd m n โฃ nNat.gcd_dvd_right ..)]Goals accomplished! ๐

theorem normalize_num_den: โ {n : Int} {d : Nat} {z : d โ  0} {n' : Int} {d' : Nat} {z' : d' โ  0} {c : Nat.coprime (Int.natAbs n') d'},
normalize n d = mk' n' d' โ โ m, m โ  0 โง n = n' * โm โง d = d' * mnormalize_num_den (h: normalize n d = mk' n' d'h : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize n: ?m.5692n d: ?m.5697d z: ?m.5702z = โจn': ?m.5715n', d': ?m.5728d', z': ?m.5741z', c: ?m.5754cโฉ) :
โ m: Natm : Nat: TypeNat, m: Natm โ  0: ?m.57750 โง n: ?m.5692n = n': ?m.5715n' * m: Natm โง d: ?m.5697d = d': ?m.5728d' * m: Natm := byGoals accomplished! ๐
n: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'โ m, m โ  0 โง n = n' * โm โง d = d' * mhave := normalize_num_den': โ (num : Int) (den : Nat) (nz : den โ  0),
โ d, d โ  0 โง num = (normalize num den).num * โd โง den = (normalize num den).den * dnormalize_num_den' n: Intn d: Natd z: d โ  0zn: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'this: โ d_1, d_1 โ  0 โง n = (normalize n d).num * โd_1 โง d = (normalize n d).den * d_1โ m, m โ  0 โง n = n' * โm โง d = d' * m;n: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'this: โ d_1, d_1 โ  0 โง n = (normalize n d).num * โd_1 โง d = (normalize n d).den * d_1โ m, m โ  0 โง n = n' * โm โง d = d' * m n: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'โ m, m โ  0 โง n = n' * โm โง d = d' * mrwa [n: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'this: โ d_1, d_1 โ  0 โง n = (normalize n d).num * โd_1 โง d = (normalize n d).den * d_1โ m, m โ  0 โง n = n' * โm โง d = d' * mh: normalize n d = mk' n' d'hn: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'this: โ d_1, d_1 โ  0 โง n = (mk' n' d').num * โd_1 โง d = (mk' n' d').den * d_1โ m, m โ  0 โง n = n' * โm โง d = d' * m]n: Intd: Natz: d โ  0n': Intd': Natz': d' โ  0c: Nat.coprime (Int.natAbs n') d'h: normalize n d = mk' n' d'this: โ d_1, d_1 โ  0 โง n = (mk' n' d').num * โd_1 โง d = (mk' n' d').den * d_1โ m, m โ  0 โง n = n' * โm โง d = d' * m at this: ?m.5921thisGoals accomplished! ๐

theorem normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat {num: ?m.5975num den: Natden} (den_nz: den โ  0den_nz) : normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize num: ?m.5975num den: ?m.5978den den_nz: ?m.5981den_nz = mkRat: Int โ Nat โ RatmkRat num: ?m.5975num den: ?m.5978den := byGoals accomplished! ๐
num: Intden: Natden_nz: den โ  0normalize num den = mkRat num densimp [mkRat: Int โ Nat โ RatmkRat, den_nz: den โ  0den_nz]Goals accomplished! ๐

theorem mkRat_num_den: โ {d : Nat} {n n' : Int} {d' : Nat} {z' : d' โ  0} {c : Nat.coprime (Int.natAbs n') d'},
d โ  0 โ mkRat n d = mk' n' d' โ โ m, m โ  0 โง n = n' * โm โง d = d' * mmkRat_num_den (z: d โ  0z : d: ?m.6164d โ  0: ?m.62970) (h: mkRat n d = mk' n' d'h : mkRat: Int โ Nat โ RatmkRat n: ?m.6183n d: ?m.6164d = โจn': ?m.6210n', d': ?m.6237d', z': ?m.6264z', c: ?m.6291cโฉ) :
โ m: Natm : Nat: TypeNat, m: Natm โ  0: ?m.63260 โง n: ?m.6183n = n': ?m.6210n' * m: Natm โง d: ?m.6164d = d': ?m.6237d' * m: Natm :=
normalize_num_den: โ {n : Int} {d : Nat} {z : d โ  0} {n' : Int} {d' : Nat} {z' : d' โ  0} {c : Nat.coprime (Int.natAbs n') d'},
normalize n d = mk' n' d' โ โ m, m โ  0 โง n = n' * โm โง d = d' * mnormalize_num_den ((normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat z: d โ  0z).symm: โ {ฮฑ : Sort ?u.6502} {a b : ฮฑ}, a = b โ b = asymm โธ h: mkRat n d = mk' n' d'h)

theorem mkRat_def: โ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n dmkRat_def (n: ?m.6570n d: ?m.6573d) : mkRat: Int โ Nat โ RatmkRat n: ?m.6570n d: ?m.6573d = if d0: ?m.6618d0 : d: ?m.6573d = 0: ?m.65790 then 0: ?m.66050 else normalize: Int โ (den : optParam Nat 1) โ autoParam (den โ  0) _autoโ โ Ratnormalize n: ?m.6570n d: ?m.6573d d0: ?m.6618d0 := rfl: โ {ฮฑ : Sort ?u.6643} {a : ฮฑ}, a = arfl

theorem mkRat_self: โ (a : Rat), mkRat a.num a.den = amkRat_self (a: Rata : Rat: TypeRat) : mkRat: Int โ Nat โ RatmkRat a: Rata.num: Rat โ Intnum a: Rata.den: Rat โ Natden = a: Rata := byGoals accomplished! ๐
a: RatmkRat a.num a.den = arw [a: RatmkRat a.num a.den = aโ normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat a: Rata.den_nz: โ (self : Rat), self.den โ  0den_nz,a: Ratnormalize a.num a.den = a a: RatmkRat a.num a.den = anormalize_self: โ (r : Rat), normalize r.num r.den = rnormalize_selfa: Rata = a]Goals accomplished! ๐

theorem mk_eq_mkRat: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = mkRat num denmk_eq_mkRat (num: ?m.6801num den: Natden nz: ?m.6807nz c: ?m.6810c) : โจnum: ?m.6801num, den: ?m.6804den, nz: ?m.6807nz, c: ?m.6810cโฉ = mkRat: Int โ Nat โ RatmkRat num: ?m.6801num den: ?m.6804den := byGoals accomplished! ๐
num: Intden: Natnz: den โ  0c: Nat.coprime (Int.natAbs num) denmk' num den = mkRat num densimp [mk_eq_normalize: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num denmk_eq_normalize, normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat]Goals accomplished! ๐

@[simp] theorem zero_mkRat: โ (n : Nat), mkRat 0 n = 0zero_mkRat (n: Natn) : mkRat: Int โ Nat โ RatmkRat 0: ?m.69750 n: ?m.6970n = 0: ?m.69840 := byGoals accomplished! ๐ n: NatmkRat 0 n = 0simp [mkRat_def: โ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n dmkRat_def]n: Nat(if h : n = 0 then 0 else 0) = 0;n: Nat(if h : n = 0 then 0 else 0) = 0 n: NatmkRat 0 n = 0apply ite_self: โ {ฮฑ : Sort ?u.7318} {c : Prop} {d : Decidable c} (a : ฮฑ), (if c then a else a) = aite_selfGoals accomplished! ๐

@[simp] theorem mkRat_zero: โ (n : Int), mkRat n 0 = 0mkRat_zero (n: ?m.7382n) : mkRat: Int โ Nat โ RatmkRat n: ?m.7382n 0: ?m.73870 = 0: ?m.73960 := byGoals accomplished! ๐ n: IntmkRat n 0 = 0simp [mkRat_def: โ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n dmkRat_def]Goals accomplished! ๐

theorem mkRat_eq_zero: โ {d : Nat} {n : Int}, d โ  0 โ (mkRat n d = 0 โ n = 0)mkRat_eq_zero (d0: d โ  0d0 : d: ?m.7564d โ  0: ?m.75890) : mkRat: Int โ Nat โ RatmkRat n: ?m.7583n d: ?m.7564d = 0: ?m.76020 โ n: ?m.7583n = 0: ?m.76220 := byGoals accomplished! ๐ d: Natn: Intd0: d โ  0mkRat n d = 0 โ n = 0simp [mkRat_def: โ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n dmkRat_def, d0: d โ  0d0]Goals accomplished! ๐

theorem mkRat_ne_zero: โ {d : Nat} {n : Int}, d โ  0 โ (mkRat n d โ  0 โ n โ  0)mkRat_ne_zero (d0: d โ  0d0 : d: ?m.7819d โ  0: ?m.78450) : mkRat: Int โ Nat โ RatmkRat n: ?m.7839n d: ?m.7819d โ  0: ?m.78590 โ n: ?m.7839n โ  0: ?m.78700 := not_congr: โ {a b : Prop}, (a โ b) โ (ยฌa โ ยฌb)not_congr (mkRat_eq_zero: โ {d : Nat} {n : Int}, d โ  0 โ (mkRat n d = 0 โ n = 0)mkRat_eq_zero d0: d โ  0d0)

theorem mkRat_mul_left: โ {n : Int} {d a : Nat}, a โ  0 โ mkRat (โa * n) (a * d) = mkRat n dmkRat_mul_left {a: Nata : Nat: TypeNat} (a0: a โ  0a0 : a: Nata โ  0: ?m.79850) : mkRat: Int โ Nat โ RatmkRat (โa: Nata * n: ?m.7923n) (a: Nata * d: ?m.7977d) = mkRat: Int โ Nat โ RatmkRat n: ?m.7923n d: ?m.7977d := byGoals accomplished! ๐
n: Intd, a: Nata0: a โ  0mkRat (โa * n) (a * d) = mkRat n dif d0: ?m.8122d0 : d: Natd = 0: ?m.80840 n: Intd, a: Nata0: a โ  0mkRat (โa * n) (a * d) = mkRat n dthenn: Intd, a: Nata0: a โ  0d0: d = 0mkRat (โa * n) (a * d) = mkRat n d n: Intd, a: Nata0: a โ  0mkRat (โa * n) (a * d) = mkRat n dsimp [d0: ?m.8115d0]Goals accomplished! ๐ n: Intd, a: Nata0: a โ  0mkRat (โa * n) (a * d) = mkRat n delsen: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = mkRat n d
n: Intd, a: Nata0: a โ  0mkRat (โa * n) (a * d) = mkRat n drw [n: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = mkRat n dโ normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat d0: ?m.8122d0,n: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = normalize n d n: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = mkRat n dโ normalize_mul_left: โ {d : Nat} {n : Int} {a : Nat} (d0 : d โ  0) (a0 : a โ  0), normalize (โa * n) (a * d) = normalize n dnormalize_mul_left d0: ?m.8122d0 a0: a โ  0a0,n: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = normalize (โa * n) (a * d) n: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = mkRat n dnormalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRatn: Intd, a: Nata0: a โ  0d0: ยฌd = 0mkRat (โa * n) (a * d) = mkRat (โa * n) (a * d)]Goals accomplished! ๐

theorem mkRat_mul_right: โ {n : Int} {d a : Nat}, a โ  0 โ mkRat (n * โa) (d * a) = mkRat n dmkRat_mul_right {a: Nata : Nat: TypeNat} (a0: a โ  0a0 : a: Nata โ  0: ?m.83810) : mkRat: Int โ Nat โ RatmkRat (n: ?m.8262n * a: Nata) (d: ?m.8373d * a: Nata) = mkRat: Int โ Nat โ RatmkRat n: ?m.8262n d: ?m.8373d := byGoals accomplished! ๐
n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat n drw [n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat n dโ mkRat_mul_left: โ {n : Int} {d a : Nat}, a โ  0 โ mkRat (โa * n) (a * d) = mkRat n dmkRat_mul_left (d := d: Natd) a0: a โ  0a0n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat (โa * n) (a * d)]n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat (โa * n) (a * d);n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat (โa * n) (a * d) n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat n dcongr 1n: Intd, a: Nata0: a โ  0e_numn * โa = โa * nn: Intd, a: Nata0: a โ  0e_dend * a = a * d <;> [n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat (โa * n) (a * d)apply Int.mul_comm: โ (a b : Int), a * b = b * aInt.mul_commGoals accomplished! ๐; n: Intd, a: Nata0: a โ  0mkRat (n * โa) (d * a) = mkRat (โa * n) (a * d)apply Nat.mul_comm: โ (n m : Nat), n * m = m * nNat.mul_commGoals accomplished! ๐]Goals accomplished! ๐

theorem mkRat_eq_iff: โ {dโ dโ : Nat} {nโ nโ : Int}, dโ โ  0 โ dโ โ  0 โ (mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโ)mkRat_eq_iff (zโ: dโ โ  0zโ : dโ: ?m.8746dโ โ  0: unknown metavariable '?_uniq.8805'0) (zโ: dโ โ  0zโ : dโ: ?m.8766dโ โ  0: ?m.88520) :
mkRat: Int โ Nat โ RatmkRat nโ: ?m.8799nโ dโ: ?m.8746dโ = mkRat: Int โ Nat โ RatmkRat nโ: ?m.8832nโ dโ: ?m.8766dโ โ nโ: ?m.8799nโ * dโ: ?m.8766dโ = nโ: ?m.8832nโ * dโ: ?m.8746dโ := byGoals accomplished! ๐
dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโrw [dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโโ normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat zโ: dโ โ  0zโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโโ normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat zโ: dโ โ  0zโ,dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโ dโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโnormalize_eq_iff: โ {dโ dโ : Nat} {nโ nโ : Int} (zโ : dโ โ  0) (zโ : dโ โ  0), normalize nโ dโ = normalize nโ dโ โ nโ * โdโ = nโ * โdโnormalize_eq_iffdโ, dโ: Natnโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ * โdโ = nโ * โdโ โ nโ * โdโ = nโ * โdโ]Goals accomplished! ๐

@[simp] theorem divInt_ofNat: โ (num : Int) (den : Nat), num /. โden = mkRat num dendivInt_ofNat (num: ?m.9108num den: ?m.9111den) : num: ?m.9108num /. (den: ?m.9111den : Nat: TypeNat) = mkRat: Int โ Nat โ RatmkRat num: ?m.9108num den: ?m.9111den := byGoals accomplished! ๐
num: Intden: Natnum /. โden = mkRat num densimp [divInt: Int โ Int โ RatdivInt, normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat]Goals accomplished! ๐

theorem mk_eq_divInt: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = num /. โdenmk_eq_divInt (num: ?m.9212num den: ?m.9215den nz: ?m.9218nz c: ?m.9221c) : โจnum: ?m.9212num, den: ?m.9215den, nz: ?m.9218nz, c: ?m.9221cโฉ = num: ?m.9212num /. (den: ?m.9215den : Nat: TypeNat) := byGoals accomplished! ๐
num: Intden: Natnz: den โ  0c: Nat.coprime (Int.natAbs num) denmk' num den = num /. โdensimp [mk_eq_mkRat: โ (num : Int) (den : Nat) (nz : den โ  0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = mkRat num denmk_eq_mkRat]Goals accomplished! ๐

theorem divInt_self: โ (a : Rat), a.num /. โa.den = adivInt_self (a: Rata : Rat: TypeRat) : a: Rata.num: Rat โ Intnum /. a: Rata.den: Rat โ Natden = a: Rata := byGoals accomplished! ๐ a: Rata.num /. โa.den = arw [a: Rata.num /. โa.den = adivInt_ofNat: โ (num : Int) (den : Nat), num /. โden = mkRat num dendivInt_ofNat,a: RatmkRat a.num a.den = a a: Rata.num /. โa.den = amkRat_self: โ (a : Rat), mkRat a.num a.den = amkRat_selfa: Rata = a]Goals accomplished! ๐

@[simp] theorem zero_divInt: โ (n : Int), 0 /. n = 0zero_divInt (n: ?m.9456n) : 0: ?m.94610 /. n: ?m.9456n = 0: ?m.94700 := byGoals accomplished! ๐ n: Int0 /. n = 0cases n: Intnaโ: NatofNat0 /. Int.ofNat aโ = 0aโ: NatnegSucc0 /. Int.negSucc aโ = 0 n: Int0 /. n = 0<;>aโ: NatofNat0 /. Int.ofNat aโ = 0aโ: NatnegSucc0 /. Int.negSucc aโ = 0 n: Int0 /. n = 0simp [divInt: Int โ Int โ RatdivInt]Goals accomplished! ๐

@[simp] theorem divInt_zero: โ (n : Int), n /. 0 = 0divInt_zero (n: Intn) : n: ?m.9758n /. 0: ?m.97630 = 0: ?m.97720 := mkRat_zero: โ (n : Int), mkRat n 0 = 0mkRat_zero n: Intn

theorem neg_divInt_neg: โ (num den : Int), -num /. -den = num /. denneg_divInt_neg (num: ?m.9818num den: ?m.9821den) : -num: ?m.9818num /. -den: ?m.9821den = num: ?m.9818num /. den: ?m.9821den := byGoals accomplished! ๐
num, den: Int-num /. -den = num /. denmatch den: Intden with
num, den: Int-num /. -den = num /. den| Nat.succ: Nat โ NatNat.succ n: Natn =>num, den: Intn: Nat-num /. -โ(Nat.succ n) = num /. โ(Nat.succ n) num, den: Int-num /. -den = num /. densimp [divInt: Int โ Int โ RatdivInt, Int.neg_ofNat_succ: โ (n : Nat), -โ(Nat.succ n) = Int.negSucc nInt.neg_ofNat_succ, normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat, Int.neg_neg: โ (a : Int), - -a = aInt.neg_neg]Goals accomplished! ๐
num, den: Int-num /. -den = num /. den| 0: Int0 =>num, den: Int-num /. -0 = num /. 0 num, den: Int-num /. -den = num /. denrflGoals accomplished! ๐
num, den: Int-num /. -den = num /. den| Int.negSucc: Nat โ IntInt.negSucc n: Natn =>num, den: Intn: Nat-num /. -Int.negSucc n = num /. Int.negSucc n num, den: Int-num /. -den = num /. densimp [divInt: Int โ Int โ RatdivInt, Int.neg_negSucc: โ (n : Nat), -Int.negSucc n = โ(Nat.succ n)Int.neg_negSucc, normalize_eq_mkRat: โ {num : Int} {den : Nat} (den_nz : den โ  0), normalize num den = mkRat num dennormalize_eq_mkRat, Int.neg_neg: โ (a : Int), - -a = aInt.neg_neg]Goals accomplished! ๐

theorem divInt_neg': โ (num den : Int), num /. -den = -num /. dendivInt_neg' (num: ?m.11657num den: ?m.11660den) : num: ?m.11657num /. -den: ?m.11660den = -num: ?m.11657num /. den: ?m.11660den := byGoals accomplished! ๐ num, den: Intnum /. -den = -num /. denrw [num, den: Intnum /. -den = -num /. denโ neg_divInt_neg: โ (num den : Int), -num /. -den = num /. denneg_divInt_neg,num, den: Int-num /. - -den = -num /. den num, den: Intnum /. -den = -num /. denInt.neg_neg: โ (a : Int), - -a = aInt.neg_negnum, den: Int-num /. den = -num /. den]Goals accomplished! ๐

theorem divInt_eq_iff: โ {dโ dโ nโ nโ : Int}, dโ โ  0 โ dโ โ  0 โ (nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโ)divInt_eq_iff (zโ: dโ โ  0zโ : dโ: ?m.11710dโ โ  0: unknown metavariable '?_uniq.11736'0) (zโ: dโ โ  0zโ : dโ: ?m.11730dโ โ  0: unknown metavariable '?_uniq.11750'0) :
nโ: ?m.11763nโ /. dโ: ?m.11710dโ = nโ: ?m.11796nโ /. dโ: ?m.11730dโ โ nโ: ?m.11763nโ * dโ: ?m.11730dโ = nโ: ?m.11796nโ * dโ: ?m.11710dโ := byGoals accomplished! ๐
dโ, dโ, nโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโrcases Int.eq_nat_or_neg: โ (a : Int), โ n, a = โn โจ a = -โnInt.eq_nat_or_neg dโ: Intdโ with โจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โnโจ_: Nat_โจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โn, rfl: dโ = โwโrflrfl | rfl: dโ = โwโ โจ dโ = -โwโ | rfl: dโ = -โwโrflโจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โnโฉdโ, nโ, nโ: Intzโ: dโ โ  0wโ: Natzโ: โwโ โ  0intro.inlnโ /. โwโ = nโ /. dโ โ nโ * dโ = nโ * โwโdโ, nโ, nโ: Intzโ: dโ โ  0wโ: Natzโ: -โwโ โ  0intro.inrnโ /. -โwโ = nโ /. dโ โ nโ * dโ = nโ * -โwโ dโ, dโ, nโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโ<;>dโ, nโ, nโ: Intzโ: dโ โ  0wโ: Natzโ: โwโ โ  0intro.inlnโ /. โwโ = nโ /. dโ โ nโ * dโ = nโ * โwโdโ, nโ, nโ: Intzโ: dโ โ  0wโ: Natzโ: -โwโ โ  0intro.inrnโ /. -โwโ = nโ /. dโ โ nโ * dโ = nโ * -โwโ
dโ, dโ, nโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโrcases Int.eq_nat_or_neg: โ (a : Int), โ n, a = โn โจ a = -โnInt.eq_nat_or_neg dโ: Intdโ with โจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โnโจ_: Nat_โจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โn, rfl: dโ = โwโrflrfl | rfl: dโ = โwโ โจ dโ = -โwโ | rfl: dโ = -โwโrflโจ_, rfl | rflโฉ: โ n, dโ = โn โจ dโ = -โnโฉnโ, nโ: Intwโยน: Natzโ: โwโยน โ  0wโ: Natzโ: โwโ โ  0intro.inl.intro.inlnโ /. โwโยน = nโ /. โwโ โ nโ * โwโ = nโ * โwโยนnโ, nโ: Intwโยน: Natzโ: โwโยน โ  0wโ: Natzโ: -โwโ โ  0intro.inl.intro.inrnโ /. โwโยน = nโ /. -โwโ โ nโ * -โwโ = nโ * โwโยน dโ, dโ, nโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโ<;>nโ, nโ: Intwโยน: Natzโ: โwโยน โ  0wโ: Natzโ: โwโ โ  0intro.inl.intro.inlnโ /. โwโยน = nโ /. โwโ โ nโ * โwโ = nโ * โwโยนnโ, nโ: Intwโยน: Natzโ: โwโยน โ  0wโ: Natzโ: -โwโ โ  0intro.inl.intro.inrnโ /. โwโยน = nโ /. -โwโ โ nโ * -โwโ = nโ * โwโยนnโ, nโ: Intwโยน: Natzโ: -โwโยน โ  0wโ: Natzโ: โwโ โ  0intro.inr.intro.inlnโ /. -โwโยน = nโ /. โwโ โ nโ * โwโ = nโ * -โwโยนnโ, nโ: Intwโยน: Natzโ: -โwโยน โ  0wโ: Natzโ: -โwโ โ  0intro.inr.intro.inrnโ /. -โwโยน = nโ /. -โwโ โ nโ * -โwโ = nโ * -โwโยน
dโ, dโ, nโ, nโ: Intzโ: dโ โ  0zโ: dโ โ  0nโ /. dโ = nโ /. dโ โ nโ * dโ = nโ * dโsimp_all [divInt_neg': โ (num den : Int), num /. -den = -num /. dendivInt_neg', Int.ofNat_eq_zero: โ {n : Nat}, โn = 0 โ n = 0Int.ofNat_eq_zero, Int.neg_eq_zero: โ {a : Int}, -a = 0 โ a = 0Int.neg_eq_zero,
mkRat_eq_iff: โ {dโ dโ : Nat} {nโ nโ : Int}, dโ โ  0 โ dโ โ  0 โ (mkRat nโ dโ = mkRat nโ dโ โ nโ * โdโ = nโ * โdโ)mkRat_eq_iff, Int.neg_mul: โ (a b : Int), -a * b = -(a * b)Int.neg_mul, Int.mul_neg: โ (a b : Int), a * -b = -(a * b)Int.mul_neg, Int.eq_neg_comm: โ {a b : Int}, a = -b โ b = -aInt.eq_neg_comm, eq_comm: โ {ฮฑ : Sort ?u.14102} {a b : ฮฑ}, a = b โ b = aeq_comm]Goals accomplished! ๐

theorem divInt_mul_left: โ {n d a : Int}, a โ  0 โ a * n /. (a * d) = n /. ddivInt_mul_left {a: Inta : Int: TypeInt} (a0: a โ  0a0 : a: Inta โ  0: ?m.151100) : (a: Inta * n: ?m.15051n) /. (a: Inta * d: ?m.15102d) = n: ?m.15051n /. d: ?m.15102d := ```