import Std.Data.Int.Lemmas
import Std.Data.Rat.Basic

/-! # Additional lemmas about the Rational Numbers -/

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.2
num 
den: ?m.5
den 
g: ?m.8
g} (
den_nz: ?m.11
den_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) → Rat
maybeNormalize 
num: ?m.2
num 
den: ?m.5
den 
g: ?m.8
g 
den_nz: ?m.11
den_nz 
reduced: ?m.14
reduced =
    { num := 
num: ?m.2
num.
div: Int → Int → Int
div 
g: ?m.8
g, den := 
den: ?m.5
den / 
g: ?m.8
g, 
den_nz: ?m.11
den_nz, reduced } := by
Goals accomplished! 🐙
  
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)unfold 
maybeNormalize: (num : Int) → (den g : Nat) → den / g ≠ 0 → Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g) → Rat
maybeNormalize
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: 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: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: 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: 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)split
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1

inl
mk' num den = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1

inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
  
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)·
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1

inl
mk' num den = mk' (Int.div num ↑g) (den / g) 
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1

inl
mk' num den = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1

inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)subst 
g: Nat
g
num: Int

den: Nat

den_nz: den / 1 ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)

inl
mk' num den = mk' (Int.div num ↑1) (den / 1);
num: Int

den: Nat

den_nz: den / 1 ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)

inl
mk' num den = mk' (Int.div num ↑1) (den / 1) 
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1

inl
mk' num den = mk' (Int.div num ↑g) (den / g)simp
Goals accomplished! 🐙
  
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)·
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1

inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g) 
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1

inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)rfl
Goals 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: Int
num : 
Int: Type
Int} {
den: Nat
den 
g: Nat
g : 
Nat: Type
Nat} (
den_nz: den ≠ 0
den_nz : 
den: Nat
den ≠ 
0: ?m.684
0)
    (
e: g = Nat.gcd (Int.natAbs num) den
e : 
g: Nat
g = 
num: Int
num.
natAbs: Int → Nat
natAbs.
gcd: Nat → Nat → Nat
gcd 
den: Nat
den) : (
num: Int
num / 
g: Nat
g).
natAbs: Int → Nat
natAbs.
coprime: Nat → Nat → Prop
coprime (
den: Nat
den / 
g: Nat
g) := by
Goals accomplished! 🐙
  
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den

Nat.coprime (Int.natAbs (num / ↑g)) (den / g)rw [
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den

Nat.coprime (Int.natAbs (num / ↑g)) (den / g)← 
Int.div_eq_ediv_of_dvd: ∀ {a b : Int}, b ∣ a → Int.div a b = a / b
Int.div_eq_ediv_of_dvd (
e: g = Nat.gcd (Int.natAbs num) den
e ▸ 
Int.ofNat_dvd_left: ∀ {n : Nat} {z : Int}, ↑n ∣ z ↔ n ∣ Int.natAbs z
Int.ofNat_dvd_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (
Nat.gcd_dvd_left: ∀ (m n : Nat), Nat.gcd m n ∣ m
Nat.gcd_dvd_left ..))
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den

Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)]
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den

Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
  
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den

Nat.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 ≠ 0
den_nz 
e: g = Nat.gcd (Int.natAbs num) den
e
Goals 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.905
num 
den: Nat
den} (
den_nz: ?m.911
den_nz) : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: ?m.905
num 
den: ?m.908
den 
den_nz: ?m.911
den_nz =
    { num := 
num: ?m.905
num / 
num: ?m.905
num.
natAbs: Int → Nat
natAbs.
gcd: Nat → Nat → Nat
gcd 
den: ?m.908
den
      den := 
den: ?m.908
den / 
num: ?m.905
num.
natAbs: Int → Nat
natAbs.
gcd: Nat → Nat → Nat
gcd 
den: ?m.908
den
      den_nz := 
normalize.den_nz: ∀ {num : Int} {den g : Nat}, den ≠ 0 → g = Nat.gcd (Int.natAbs num) den → den / g ≠ 0
normalize.den_nz 
den_nz: ?m.911
den_nz 
rfl: ∀ {α : Sort ?u.1057} {a : α}, a = a
rfl
      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.911
den_nz 
rfl: ∀ {α : Sort ?u.1076} {a : α}, a = a
rfl } := by
Goals accomplished! 🐙
  
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)simp only [
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize, 
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 / b
Int.div_eq_ediv_of_dvd (
Int.ofNat_dvd_left: ∀ {n : Nat} {z : Int}, ↑n ∣ z ↔ n ∣ Int.natAbs z
Int.ofNat_dvd_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (
Nat.gcd_dvd_left: ∀ (m n : Nat), Nat.gcd m n ∣ m
Nat.gcd_dvd_left ..))]
Goals accomplished! 🐙

@[simp] theorem 
normalize_zero: ∀ {d : Nat} (nz : d ≠ 0), normalize 0 d = 0
normalize_zero (
nz: d ≠ 0
nz) : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
0: ?m.1378
0 
d: ?m.1370
d 
nz: ?m.1373
nz = 
0: ?m.1381
0 := by
Goals accomplished! 🐙
  
d: Nat

nz: d ≠ 0

normalize 0 d = 0simp [
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize, 
Int.zero_div: ∀ (b : Int), Int.div 0 b = 0
Int.zero_div, 
Int.natAbs_zero: Int.natAbs 0 = 0
Int.natAbs_zero, 
Nat.div_self: ∀ {n : Nat}, 0 < n → n / n = 1
Nat.div_self (
Nat.pos_of_ne_zero: ∀ {n : Nat}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zero 
nz: d ≠ 0
nz)]
d: Nat

nz: d ≠ 0

mk' 0 1 = 0;
d: Nat

nz: d ≠ 0

mk' 0 1 = 0 
d: Nat

nz: d ≠ 0

normalize 0 d = 0rfl
Goals accomplished! 🐙

theorem 
mk_eq_normalize: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num den
mk_eq_normalize (
num: ?m.1668
num 
den: Nat
den 
nz: den ≠ 0
nz 
c: Nat.coprime (Int.natAbs num) den
c) : ⟨
num: ?m.1668
num, 
den: ?m.1671
den, 
nz: ?m.1674
nz, 
c: ?m.1677
c⟩ = 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: ?m.1668
num 
den: ?m.1671
den 
nz: ?m.1674
nz := by
Goals accomplished! 🐙
  
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den

mk' 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) den
c.
gcd_eq_one: ∀ {m n : Nat}, Nat.coprime m n → Nat.gcd m n = 1
gcd_eq_one]
Goals accomplished! 🐙

theorem 
normalize_self: ∀ (r : Rat), normalize r.num r.den = r
normalize_self (
r: Rat
r : 
Rat: Type
Rat) : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
r: Rat
r.
num: Rat → Int
num 
r: Rat
r.
den: Rat → Nat
den 
r: Rat
r.
den_nz: ∀ (self : Rat), self.den ≠ 0
den_nz = 
r: Rat
r := (
mk_eq_normalize: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num den
mk_eq_normalize ..).
symm: ∀ {α : Sort ?u.2002} {a b : α}, a = b → b = a
symm

theorem 
normalize_mul_left: ∀ {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0), normalize (↑a * n) (a * d) = normalize n d
normalize_mul_left {
a: Nat
a : 
Nat: Type
Nat} (
d0: d ≠ 0
d0 : 
d: ?m.2026
d ≠ 
0: ?m.2074
0) (
a0: a ≠ 0
a0 : 
a: Nat
a ≠ 
0: ?m.2088
0) :
    
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize (↑
a: Nat
a * 
n: ?m.2066
n) (
a: Nat
a * 
d: ?m.2026
d) (
Nat.mul_ne_zero: ∀ {n m : Nat}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
Nat.mul_ne_zero 
a0: a ≠ 0
a0 
d0: d ≠ 0
d0) = 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n: ?m.2066
n 
d: ?m.2026
d 
d0: d ≠ 0
d0 := by
Goals accomplished! 🐙
  
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (↑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 b
Int.natAbs_mul, 
Nat.gcd_mul_left: ∀ (m n k : Nat), Nat.gcd (m * n) (m * k) = m * Nat.gcd n k
Nat.gcd_mul_left,
    
Nat.mul_div_mul_left: ∀ {m : Nat} (n k : Nat), 0 < m → m * n / (m * k) = n / k
Nat.mul_div_mul_left 
_: Nat
_ 
_: Nat
_ (
Nat.pos_of_ne_zero: ∀ {n : Nat}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zero 
a0: a ≠ 0
a0), 
Int.ofNat_mul: ∀ (n m : Nat), ↑(n * m) = ↑n * ↑m
Int.ofNat_mul,
    
Int.mul_ediv_mul_of_pos: ∀ {a : Int} (b c : Int), 0 < a → a * b / (a * c) = b / c
Int.mul_ediv_mul_of_pos 
_: Int
_ 
_: Int
_ (
Int.ofNat_pos: ∀ {n : Nat}, 0 < ↑n ↔ 0 < n
Int.ofNat_pos.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.pos_of_ne_zero: ∀ {n : Nat}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zero 
a0: a ≠ 0
a0)]
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 d
normalize_mul_right {
a: Nat
a : 
Nat: Type
Nat} (
d0: d ≠ 0
d0 : 
d: ?m.2780
d ≠ 
0: ?m.2825
0) (
a0: a ≠ 0
a0 : 
a: Nat
a ≠ 
0: ?m.2839
0) :
    
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize (
n: ?m.2817
n * 
a: Nat
a) (
d: ?m.2780
d * 
a: Nat
a) (
Nat.mul_ne_zero: ∀ {n m : Nat}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
Nat.mul_ne_zero 
d0: d ≠ 0
d0 
a0: a ≠ 0
a0) = 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n: ?m.2817
n 
d: ?m.2780
d 
d0: d ≠ 0
d0 := by
Goals accomplished! 🐙
  
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize n drw [
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (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 d
normalize_mul_left (d0 := 
d0: d ≠ 0
d0) 
a0: a ≠ 0
a0
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)]
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d);
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d) 
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize n dcongr 1
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

e_num
n * ↑a = ↑a * n
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

e_den
d * a = a * d <;> [
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)apply 
Int.mul_comm: ∀ (a b : Int), a * b = b * a
Int.mul_comm
Goals accomplished! 🐙; 
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0

normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)apply 
Nat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm
Goals 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₁ ≠ 0
z₁ : 
d₁: ?m.3267
d₁ ≠ 
0: unknown metavariable '?_uniq.3326'
0) (
z₂: d₂ ≠ 0
z₂ : 
d₂: ?m.3287
d₂ ≠ 
0: ?m.3382
0) :
    
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n₁: ?m.3320
n₁ 
d₁: ?m.3267
d₁ 
z₁: d₁ ≠ 0
z₁ = 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n₂: ?m.3362
n₂ 
d₂: ?m.3287
d₂ 
z₂: d₂ ≠ 0
z₂ ↔ 
n₁: ?m.3320
n₁ * 
d₂: ?m.3287
d₂ = 
n₂: ?m.3362
n₂ * 
d₁: ?m.3267
d₁ := by
Goals accomplished! 🐙
  
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁constructor
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mp
normalize n₁ d₁ = normalize n₂ d₂ → n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mpr
n₁ * ↑d₂ = n₂ * ↑d₁ → normalize n₁ d₁ = normalize n₂ d₂ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁<;>
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mp
normalize n₁ d₁ = normalize n₂ d₂ → n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mpr
n₁ * ↑d₂ = n₂ * ↑d₁ → normalize n₁ d₁ = normalize n₂ d₂ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁intro 
h: ?a
h
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize n₁ d₁ = normalize n₂ d₂
  
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁·
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize 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: ?a
h
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
    
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁have' 
hn₁: ?m.3810
hn₁ := 
Int.ofNat_dvd_left: ∀ {n : Nat} {z : Int}, ↑n ∣ z ↔ n ∣ Int.natAbs z
Int.ofNat_dvd_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.gcd_dvd_left: ∀ (m n : Nat), Nat.gcd m n ∣ m
Nat.gcd_dvd_left 
n₁: Int
n₁.
natAbs: Int → Nat
natAbs 
d₁: Nat
d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

mp
n₁ * ↑d₂ = n₂ * ↑d₁
    
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁have' 
hn₂: ?m.3826
hn₂ := 
Int.ofNat_dvd_left: ∀ {n : Nat} {z : Int}, ↑n ∣ z ↔ n ∣ Int.natAbs z
Int.ofNat_dvd_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.gcd_dvd_left: ∀ (m n : Nat), Nat.gcd m n ∣ m
Nat.gcd_dvd_left 
n₂: Int
n₂.
natAbs: Int → Nat
natAbs 
d₂: Nat
d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
    
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁have' 
hd₁: ?m.3837
hd₁ := 
Int.ofNat_dvd: ∀ {m n : Nat}, ↑m ∣ ↑n ↔ m ∣ n
Int.ofNat_dvd.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.gcd_dvd_right: ∀ (m n : Nat), Nat.gcd m n ∣ n
Nat.gcd_dvd_right 
n₁: Int
n₁.
natAbs: Int → Nat
natAbs 
d₁: Nat
d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

mp
n₁ * ↑d₂ = n₂ * ↑d₁
    
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁have' 
hd₂: ?m.3848
hd₂ := 
Int.ofNat_dvd: ∀ {m n : Nat}, ↑m ∣ ↑n ↔ m ∣ n
Int.ofNat_dvd.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.gcd_dvd_right: ∀ (m n : Nat), Nat.gcd m n ∣ n
Nat.gcd_dvd_right 
n₂: Int
n₂.
natAbs: Int → Nat
natAbs 
d₂: Nat
d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
    
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁rw [
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁← 
Int.ediv_mul_cancel: ∀ {a b : Int}, b ∣ a → a / b * b = a
Int.ediv_mul_cancel (
Int.dvd_trans: ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
Int.dvd_trans 
hd₂: ?m.3848
hd₂ (
Int.dvd_mul_left: ∀ (a b : Int), b ∣ a * b
Int.dvd_mul_left ..)),
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
      
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑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.3848
hd₂,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * (↑d₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂)) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁← 
Int.ofNat_ediv: ∀ (m n : Nat), ↑(m / n) = ↑m / ↑n
Int.ofNat_ediv,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑(d₂ / Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑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 → b
2,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑(d₁ / Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
Int.ofNat_ediv: ∀ (m n : Nat), ↑(m / n) = ↑m / ↑n
Int.ofNat_ediv,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * (↑d₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁)) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
      
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑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.3837
hd₁,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
Int.mul_ediv_assoc': ∀ (b : Int) {a c : Int}, c ∣ a → a * b / c = a / c * b
Int.mul_ediv_assoc' 
_: Int
_ 
hn₁: ?m.3810
hn₁,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑d₁ * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
      
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
Int.mul_right_comm: ∀ (a b c : Int), a * b * c = a * c * b
Int.mul_right_comm,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑d₁ = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑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 → a
1,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑d₁ = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₁ * ↑d₂ = n₂ * ↑d₁
Int.ediv_mul_cancel: ∀ {a b : Int}, b ∣ a → a / b * b = a
Int.ediv_mul_cancel 
hn₂: ?m.3826
hn₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

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₂

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₂

mp
n₂ * ↑d₁ = n₂ * ↑d₁]
Goals accomplished! 🐙
  
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁·
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize n₁ d₁ = normalize n₂ d₂ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize n₁ d₁ = normalize n₂ d₂rw [
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize 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 d
normalize_mul_right 
_: ?m.3954 ≠ 0
_ 
z₂: d₂ ≠ 0
z₂,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize n₂ d₂ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize 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 d
normalize_mul_left 
z₂: d₂ ≠ 0
z₂ 
z₁: d₁ ≠ 0
z₁,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize (↑d₁ * n₂) (d₁ * d₂) 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize n₁ d₁ = normalize n₂ d₂
Int.mul_comm: ∀ (a b : Int), a * b = b * a
Int.mul_comm 
d₁: Nat
d₁,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize (n₂ * ↑d₁) (d₁ * d₂) 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize n₁ d₁ = normalize n₂ d₂
h: ?b
h
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁

mpr
normalize (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 den
maybeNormalize_eq_normalize {
num: Int
num : 
Int: Type
Int} {
den: Nat
den 
g: Nat
g : 
Nat: Type
Nat} (
den_nz: den / g ≠ 0
den_nz 
reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
reduced)
    (
hn: ?m.4055 ∣ num
hn : ↑
g: Nat
g ∣ 
num: Int
num) (
hd: g ∣ den
hd : 
g: Nat
g ∣ 
den: Nat
den) :
    
maybeNormalize: (num : Int) → (den g : Nat) → den / g ≠ 0 → Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g) → Rat
maybeNormalize 
num: Int
num 
den: Nat
den 
g: Nat
g 
den_nz: ?m.4044
den_nz 
reduced: ?m.4047
reduced = 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: Int
num 
den: Nat
den (
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt 
(: den = 0 → den / g = 0
(
by: den = 0 → den / g = 0
by
Goals accomplished! 🐙
 simp [·]): den = 0 → den / g = 0
 
 simp [·]): den = 0 → den / g = 0
simp
 simp [·]): den = 0 → den / g = 0
 [·]) 
den_nz: ?m.4044
den_nz) := by
Goals accomplished! 🐙
  
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

maybeNormalize 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 den
mk_eq_normalize, 
Int.div_eq_ediv_of_dvd: ∀ {a b : Int}, b ∣ a → Int.div a b = a / b
Int.div_eq_ediv_of_dvd 
hn: ↑g ∣ num
hn]
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

normalize (num / ↑g) (den / g) = normalize num den
  
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

maybeNormalize num den g den_nz reduced = normalize num denhave : 
g: Nat
g ≠ 
0: ?m.4413
0 := 
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt 
(: g = 0 → den / g = 0
(
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

normalize (num / ↑g) (den / g) = normalize num den
by: g = 0 → den / g = 0
by
Goals accomplished! 🐙
 simp [·]): g = 0 → den / g = 0
 
 simp [·]): g = 0 → den / g = 0
simp
 simp [·]): g = 0 → den / g = 0
 [·]) 
den_nz: den / g ≠ 0
den_nz
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize (num / ↑g) (den / g) = normalize num den
  
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

maybeNormalize num den g den_nz reduced = normalize num denrw [
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize (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 d
normalize_mul_right 
_: ?m.4446 ≠ 0
_ 
this: g ≠ 0
this,
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize (num / ↑g * ↑g) (den / g * g) = normalize num den 
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize (num / ↑g) (den / g) = normalize num den
Int.ediv_mul_cancel: ∀ {a b : Int}, b ∣ a → a / b * b = a
Int.ediv_mul_cancel 
hn: ↑g ∣ num
hn
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize num (den / g * g) = normalize num den]
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

normalize num (den / g * g) = normalize num den
  
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

maybeNormalize num den g den_nz reduced = normalize num dencongr 1
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

e_den
den / g * g = den;
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0

e_den
den / g * g = den 
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

maybeNormalize num den g den_nz reduced = normalize num denexact 
Nat.div_mul_cancel: ∀ {n m : Nat}, n ∣ m → m / n * n = m
Nat.div_mul_cancel 
hd: g ∣ den
hd
Goals accomplished! 🐙

@[simp] theorem 
normalize_eq_zero: ∀ {d : Nat} {n : Int} (d0 : d ≠ 0), normalize n d = 0 ↔ n = 0
normalize_eq_zero (
d0: d ≠ 0
d0 : 
d: ?m.4799
d ≠ 
0: unknown metavariable '?_uniq.4805'
0) : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n: ?m.4818
n 
d: ?m.4799
d 
d0: d ≠ 0
d0 = 
0: ?m.4846
0 ↔ 
n: ?m.4818
n = 
0: ?m.4864
0 := by
Goals accomplished! 🐙
  
d: Nat

n: Int

d0: d ≠ 0

normalize 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 ≠ 0
d0 
Nat.one_ne_zero: 1 ≠ 0
Nat.one_ne_zero
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_2
Int
  
d: Nat

n: Int

d0: d ≠ 0

normalize n d = 0 ↔ n = 0rw [
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_2
Int
normalize_zero: ∀ {d : Nat} (nz : d ≠ 0), normalize 0 d = 0
normalize_zero (d := 
1: ?m.4901
1)
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int]
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int at 
this: ?m.4887
this
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int;
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int 
d: Nat

n: Int

d0: d ≠ 0

normalize n d = 0 ↔ n = 0rw [
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d

refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
d: Nat

n: Int

d0: d ≠ 0

refine'_1
Int
this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d
this
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d

refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0]
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d

refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0;
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d

refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0 
d: Nat

n: Int

d0: d ≠ 0

normalize n d = 0 ↔ n = 0simp
Goals 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 * d
normalize_num_den' (
num: Int
num 
den: ?m.5050
den 
nz: ?m.5053
nz) : ∃ 
d: Nat
d : 
Nat: Type
Nat, 
d: Nat
d ≠ 
0: ?m.5063
0 ∧
    
num: ?m.5047
num = (
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: ?m.5047
num 
den: ?m.5050
den 
nz: ?m.5053
nz).
num: Rat → Int
num * 
d: Nat
d ∧ 
den: ?m.5050
den = (
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: ?m.5047
num 
den: ?m.5050
den 
nz: ?m.5053
nz).
den: Rat → Nat
den * 
d: Nat
d := by
Goals accomplished! 🐙
  
num: Int

den: Nat

nz: den ≠ 0

∃ d, d ≠ 0 ∧ num = (normalize num den).num * ↑d ∧ den = (normalize num den).den * drefine ⟨
num: Int
num.
natAbs: Int → Nat
natAbs.
gcd: Nat → Nat → Nat
gcd 
den: Nat
den, 
Nat.gcd_ne_zero_right: ∀ {n m : Nat}, n ≠ 0 → Nat.gcd m n ≠ 0
Nat.gcd_ne_zero_right 
nz: den ≠ 0
nz, 
?_: ?m.5223
?_⟩
num: Int

den: Nat

nz: den ≠ 0

num = (normalize num den).num * ↑(Nat.gcd (Int.natAbs num) den) ∧   den = (normalize num den).den * Nat.gcd (Int.natAbs num) den
  
num: Int

den: Nat

nz: 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 = a
Int.ediv_mul_cancel (
Int.ofNat_dvd_left: ∀ {n : Nat} {z : Int}, ↑n ∣ z ↔ n ∣ Int.natAbs z
Int.ofNat_dvd_left.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| 
Nat.gcd_dvd_left: ∀ (m n : Nat), Nat.gcd m n ∣ m
Nat.gcd_dvd_left ..),
    
Nat.div_mul_cancel: ∀ {n m : Nat}, n ∣ m → m / n * n = m
Nat.div_mul_cancel (
Nat.gcd_dvd_right: ∀ (m n : Nat), Nat.gcd m n ∣ n
Nat.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' * m
normalize_num_den (
h: normalize n d = mk' n' d'
h : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n: ?m.5692
n 
d: ?m.5697
d 
z: ?m.5702
z = ⟨
n': ?m.5715
n', 
d': ?m.5728
d', 
z': ?m.5741
z', 
c: ?m.5754
c⟩) :
    ∃ 
m: Nat
m : 
Nat: Type
Nat, 
m: Nat
m ≠ 
0: ?m.5775
0 ∧ 
n: ?m.5692
n = 
n': ?m.5715
n' * 
m: Nat
m ∧ 
d: ?m.5697
d = 
d': ?m.5728
d' * 
m: Nat
m := by
Goals accomplished! 🐙
  
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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 * d
normalize_num_den' 
n: Int
n 
d: Nat
d 
z: d ≠ 0
z
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * mrwa [
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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
h: normalize n d = mk' n' d'
h
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: 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.5921
this
Goals accomplished! 🐙

theorem 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat {
num: ?m.5975
num 
den: Nat
den} (
den_nz: den ≠ 0
den_nz) : 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
num: ?m.5975
num 
den: ?m.5978
den 
den_nz: ?m.5981
den_nz = 
mkRat: Int → Nat → Rat
mkRat 
num: ?m.5975
num 
den: ?m.5978
den := by
Goals accomplished! 🐙
  
num: Int

den: Nat

den_nz: den ≠ 0

normalize num den = mkRat num densimp [
mkRat: Int → Nat → Rat
mkRat, 
den_nz: den ≠ 0
den_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' * m
mkRat_num_den (
z: d ≠ 0
z : 
d: ?m.6164
d ≠ 
0: ?m.6297
0) (
h: mkRat n d = mk' n' d'
h : 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.6183
n 
d: ?m.6164
d = ⟨
n': ?m.6210
n', 
d': ?m.6237
d', 
z': ?m.6264
z', 
c: ?m.6291
c⟩) :
    ∃ 
m: Nat
m : 
Nat: Type
Nat, 
m: Nat
m ≠ 
0: ?m.6326
0 ∧ 
n: ?m.6183
n = 
n': ?m.6210
n' * 
m: Nat
m ∧ 
d: ?m.6164
d = 
d': ?m.6237
d' * 
m: Nat
m :=
  
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' * m
normalize_num_den ((
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat 
z: d ≠ 0
z).
symm: ∀ {α : Sort ?u.6502} {a b : α}, a = b → b = a
symm ▸ 
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 d
mkRat_def (
n: ?m.6570
n 
d: ?m.6573
d) : 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.6570
n 
d: ?m.6573
d = if 
d0: ?m.6618
d0 : 
d: ?m.6573
d = 
0: ?m.6579
0 then 
0: ?m.6605
0 else 
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize 
n: ?m.6570
n 
d: ?m.6573
d 
d0: ?m.6618
d0 := 
rfl: ∀ {α : Sort ?u.6643} {a : α}, a = a
rfl

theorem 
mkRat_self: ∀ (a : Rat), mkRat a.num a.den = a
mkRat_self (
a: Rat
a : 
Rat: Type
Rat) : 
mkRat: Int → Nat → Rat
mkRat 
a: Rat
a.
num: Rat → Int
num 
a: Rat
a.
den: Rat → Nat
den = 
a: Rat
a := by
Goals accomplished! 🐙
  
a: Rat

mkRat a.num a.den = arw [
a: Rat

mkRat a.num a.den = a← 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat 
a: Rat
a.
den_nz: ∀ (self : Rat), self.den ≠ 0
den_nz,
a: Rat

normalize a.num a.den = a 
a: Rat

mkRat a.num a.den = a
normalize_self: ∀ (r : Rat), normalize r.num r.den = r
normalize_self
a: Rat

a = 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 den
mk_eq_mkRat (
num: ?m.6801
num 
den: Nat
den 
nz: ?m.6807
nz 
c: ?m.6810
c) : ⟨
num: ?m.6801
num, 
den: ?m.6804
den, 
nz: ?m.6807
nz, 
c: ?m.6810
c⟩ = 
mkRat: Int → Nat → Rat
mkRat 
num: ?m.6801
num 
den: ?m.6804
den := by
Goals accomplished! 🐙
  
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den

mk' 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 den
mk_eq_normalize, 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat]
Goals accomplished! 🐙

@[simp] theorem 
zero_mkRat: ∀ (n : Nat), mkRat 0 n = 0
zero_mkRat (
n: Nat
n) : 
mkRat: Int → Nat → Rat
mkRat 
0: ?m.6975
0 
n: ?m.6970
n = 
0: ?m.6984
0 := by
Goals accomplished! 🐙 
n: Nat

mkRat 0 n = 0simp [
mkRat_def: ∀ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n d
mkRat_def]
n: Nat

(if h : n = 0 then 0 else 0) = 0;
n: Nat

(if h : n = 0 then 0 else 0) = 0 
n: Nat

mkRat 0 n = 0apply 
ite_self: ∀ {α : Sort ?u.7318} {c : Prop} {d : Decidable c} (a : α), (if c then a else a) = a
ite_self
Goals accomplished! 🐙

@[simp] theorem 
mkRat_zero: ∀ (n : Int), mkRat n 0 = 0
mkRat_zero (
n: ?m.7382
n) : 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.7382
n 
0: ?m.7387
0 = 
0: ?m.7396
0 := by
Goals accomplished! 🐙 
n: Int

mkRat n 0 = 0simp [
mkRat_def: ∀ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n d
mkRat_def]
Goals accomplished! 🐙

theorem 
mkRat_eq_zero: ∀ {d : Nat} {n : Int}, d ≠ 0 → (mkRat n d = 0 ↔ n = 0)
mkRat_eq_zero (
d0: d ≠ 0
d0 : 
d: ?m.7564
d ≠ 
0: ?m.7589
0) : 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.7583
n 
d: ?m.7564
d = 
0: ?m.7602
0 ↔ 
n: ?m.7583
n = 
0: ?m.7622
0 := by
Goals accomplished! 🐙 
d: Nat

n: Int

d0: d ≠ 0

mkRat n d = 0 ↔ n = 0simp [
mkRat_def: ∀ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n d
mkRat_def, 
d0: d ≠ 0
d0]
Goals accomplished! 🐙

theorem 
mkRat_ne_zero: ∀ {d : Nat} {n : Int}, d ≠ 0 → (mkRat n d ≠ 0 ↔ n ≠ 0)
mkRat_ne_zero (
d0: d ≠ 0
d0 : 
d: ?m.7819
d ≠ 
0: ?m.7845
0) : 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.7839
n 
d: ?m.7819
d ≠ 
0: ?m.7859
0 ↔ 
n: ?m.7839
n ≠ 
0: ?m.7870
0 := 
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 ≠ 0
d0)

theorem 
mkRat_mul_left: ∀ {n : Int} {d a : Nat}, a ≠ 0 → mkRat (↑a * n) (a * d) = mkRat n d
mkRat_mul_left {
a: Nat
a : 
Nat: Type
Nat} (
a0: a ≠ 0
a0 : 
a: Nat
a ≠ 
0: ?m.7985
0) : 
mkRat: Int → Nat → Rat
mkRat (↑
a: Nat
a * 
n: ?m.7923
n) (
a: Nat
a * 
d: ?m.7977
d) = 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.7923
n 
d: ?m.7977
d := by
Goals accomplished! 🐙
  
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (↑a * n) (a * d) = mkRat n dif 
d0: ?m.8122
d0 : 
d: Nat
d = 
0: ?m.8084
0 
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (↑a * n) (a * d) = mkRat n dthen
n: Int

d, a: Nat

a0: a ≠ 0

d0: d = 0

mkRat (↑a * n) (a * d) = mkRat n d 
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (↑a * n) (a * d) = mkRat n dsimp [
d0: ?m.8115
d0]
Goals accomplished! 🐙 
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (↑a * n) (a * d) = mkRat n delse
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑a * n) (a * d) = mkRat n d
  
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (↑a * n) (a * d) = mkRat n drw [
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑a * n) (a * d) = mkRat n d← 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat 
d0: ?m.8122
d0,
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑a * n) (a * d) = normalize n d 
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑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 d
normalize_mul_left 
d0: ?m.8122
d0 
a0: a ≠ 0
a0,
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑a * n) (a * d) = normalize (↑a * n) (a * d) 
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑a * n) (a * d) = mkRat n d
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0

mkRat (↑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 d
mkRat_mul_right {
a: Nat
a : 
Nat: Type
Nat} (
a0: a ≠ 0
a0 : 
a: Nat
a ≠ 
0: ?m.8381
0) : 
mkRat: Int → Nat → Rat
mkRat (
n: ?m.8262
n * 
a: Nat
a) (
d: ?m.8373
d * 
a: Nat
a) = 
mkRat: Int → Nat → Rat
mkRat 
n: ?m.8262
n 
d: ?m.8373
d := by
Goals accomplished! 🐙
  
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat n drw [
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat n d← 
mkRat_mul_left: ∀ {n : Int} {d a : Nat}, a ≠ 0 → mkRat (↑a * n) (a * d) = mkRat n d
mkRat_mul_left (d := 
d: Nat
d) 
a0: a ≠ 0
a0
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)]
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d);
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d) 
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat n dcongr 1
n: Int

d, a: Nat

a0: a ≠ 0

e_num
n * ↑a = ↑a * n
n: Int

d, a: Nat

a0: a ≠ 0

e_den
d * a = a * d <;> [
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)apply 
Int.mul_comm: ∀ (a b : Int), a * b = b * a
Int.mul_comm
Goals accomplished! 🐙; 
n: Int

d, a: Nat

a0: a ≠ 0

mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)apply 
Nat.mul_comm: ∀ (n m : Nat), n * m = m * n
Nat.mul_comm
Goals 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₁ ≠ 0
z₁ : 
d₁: ?m.8746
d₁ ≠ 
0: unknown metavariable '?_uniq.8805'
0) (
z₂: d₂ ≠ 0
z₂ : 
d₂: ?m.8766
d₂ ≠ 
0: ?m.8852
0) :
    
mkRat: Int → Nat → Rat
mkRat 
n₁: ?m.8799
n₁ 
d₁: ?m.8746
d₁ = 
mkRat: Int → Nat → Rat
mkRat 
n₂: ?m.8832
n₂ 
d₂: ?m.8766
d₂ ↔ 
n₁: ?m.8799
n₁ * 
d₂: ?m.8766
d₂ = 
n₂: ?m.8832
n₂ * 
d₁: ?m.8746
d₁ := by
Goals accomplished! 🐙
  
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁rw [
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mkRat 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 den
normalize_eq_mkRat 
z₁: d₁ ≠ 0
z₁,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mkRat 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 den
normalize_eq_mkRat 
z₂: d₂ ≠ 0
z₂,
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁ 
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

mkRat 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_iff
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ * ↑d₂ = n₂ * ↑d₁ ↔ n₁ * ↑d₂ = n₂ * ↑d₁]
Goals accomplished! 🐙

@[simp] theorem 
divInt_ofNat: ∀ (num : Int) (den : Nat), num /. ↑den = mkRat num den
divInt_ofNat (
num: ?m.9108
num 
den: ?m.9111
den) : 
num: ?m.9108
num /. (
den: ?m.9111
den : 
Nat: Type
Nat) = 
mkRat: Int → Nat → Rat
mkRat 
num: ?m.9108
num 
den: ?m.9111
den := by
Goals accomplished! 🐙
  
num: Int

den: Nat

num /. ↑den = mkRat num densimp [
divInt: Int → Int → Rat
divInt, 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_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 /. ↑den
mk_eq_divInt (
num: ?m.9212
num 
den: ?m.9215
den 
nz: ?m.9218
nz 
c: ?m.9221
c) : ⟨
num: ?m.9212
num, 
den: ?m.9215
den, 
nz: ?m.9218
nz, 
c: ?m.9221
c⟩ = 
num: ?m.9212
num /. (
den: ?m.9215
den : 
Nat: Type
Nat) := by
Goals accomplished! 🐙
  
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den

mk' 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 den
mk_eq_mkRat]
Goals accomplished! 🐙

theorem 
divInt_self: ∀ (a : Rat), a.num /. ↑a.den = a
divInt_self (
a: Rat
a : 
Rat: Type
Rat) : 
a: Rat
a.
num: Rat → Int
num /. 
a: Rat
a.
den: Rat → Nat
den = 
a: Rat
a := by
Goals accomplished! 🐙 
a: Rat

a.num /. ↑a.den = arw [
a: Rat

a.num /. ↑a.den = a
divInt_ofNat: ∀ (num : Int) (den : Nat), num /. ↑den = mkRat num den
divInt_ofNat,
a: Rat

mkRat a.num a.den = a 
a: Rat

a.num /. ↑a.den = a
mkRat_self: ∀ (a : Rat), mkRat a.num a.den = a
mkRat_self
a: Rat

a = a]
Goals accomplished! 🐙

@[simp] theorem 
zero_divInt: ∀ (n : Int), 0 /. n = 0
zero_divInt (
n: ?m.9456
n) : 
0: ?m.9461
0 /. 
n: ?m.9456
n = 
0: ?m.9470
0 := by
Goals accomplished! 🐙 
n: Int

0 /. n = 0cases 
n: Int
n
a✝: Nat

ofNat
0 /. Int.ofNat a✝ = 0
a✝: Nat

negSucc
0 /. Int.negSucc a✝ = 0 
n: Int

0 /. n = 0<;>
a✝: Nat

ofNat
0 /. Int.ofNat a✝ = 0
a✝: Nat

negSucc
0 /. Int.negSucc a✝ = 0 
n: Int

0 /. n = 0simp [
divInt: Int → Int → Rat
divInt]
Goals accomplished! 🐙

@[simp] theorem 
divInt_zero: ∀ (n : Int), n /. 0 = 0
divInt_zero (
n: Int
n) : 
n: ?m.9758
n /. 
0: ?m.9763
0 = 
0: ?m.9772
0 := 
mkRat_zero: ∀ (n : Int), mkRat n 0 = 0
mkRat_zero 
n: Int
n

theorem 
neg_divInt_neg: ∀ (num den : Int), -num /. -den = num /. den
neg_divInt_neg (
num: ?m.9818
num 
den: ?m.9821
den) : -
num: ?m.9818
num /. -
den: ?m.9821
den = 
num: ?m.9818
num /. 
den: ?m.9821
den := by
Goals accomplished! 🐙
  
num, den: Int

-num /. -den = num /. denmatch 
den: Int
den with
  
num, den: Int

-num /. -den = num /. den| 
Nat.succ: Nat → Nat
Nat.succ 
n: Nat
n =>
num, den: Int

n: Nat

-num /. -↑(Nat.succ n) = num /. ↑(Nat.succ n) 
num, den: Int

-num /. -den = num /. densimp [
divInt: Int → Int → Rat
divInt, 
Int.neg_ofNat_succ: ∀ (n : Nat), -↑(Nat.succ n) = Int.negSucc n
Int.neg_ofNat_succ, 
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat, 
Int.neg_neg: ∀ (a : Int), - -a = a
Int.neg_neg]
Goals accomplished! 🐙
  
num, den: Int

-num /. -den = num /. den| 
0: Int
0 =>
num, den: Int

-num /. -0 = num /. 0 
num, den: Int

-num /. -den = num /. denrfl
Goals accomplished! 🐙
  
num, den: Int

-num /. -den = num /. den| 
Int.negSucc: Nat → Int
Int.negSucc 
n: Nat
n =>
num, den: Int

n: Nat

-num /. -Int.negSucc n = num /. Int.negSucc n 
num, den: Int

-num /. -den = num /. densimp [
divInt: Int → Int → Rat
divInt, 
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 den
normalize_eq_mkRat, 
Int.neg_neg: ∀ (a : Int), - -a = a
Int.neg_neg]
Goals accomplished! 🐙

theorem 
divInt_neg': ∀ (num den : Int), num /. -den = -num /. den
divInt_neg' (
num: ?m.11657
num 
den: ?m.11660
den) : 
num: ?m.11657
num /. -
den: ?m.11660
den = -
num: ?m.11657
num /. 
den: ?m.11660
den := by
Goals accomplished! 🐙 
num, den: Int

num /. -den = -num /. denrw [
num, den: Int

num /. -den = -num /. den← 
neg_divInt_neg: ∀ (num den : Int), -num /. -den = num /. den
neg_divInt_neg,
num, den: Int

-num /. - -den = -num /. den 
num, den: Int

num /. -den = -num /. den
Int.neg_neg: ∀ (a : Int), - -a = a
Int.neg_neg
num, 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₁ ≠ 0
z₁ : 
d₁: ?m.11710
d₁ ≠ 
0: unknown metavariable '?_uniq.11736'
0) (
z₂: d₂ ≠ 0
z₂ : 
d₂: ?m.11730
d₂ ≠ 
0: unknown metavariable '?_uniq.11750'
0) :
    
n₁: ?m.11763
n₁ /. 
d₁: ?m.11710
d₁ = 
n₂: ?m.11796
n₂ /. 
d₂: ?m.11730
d₂ ↔ 
n₁: ?m.11763
n₁ * 
d₂: ?m.11730
d₂ = 
n₂: ?m.11796
n₂ * 
d₁: ?m.11710
d₁ := by
Goals accomplished! 🐙
  
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁rcases 
Int.eq_nat_or_neg: ∀ (a : Int), ∃ n, a = ↑n ∨ a = -↑n
Int.eq_nat_or_neg 
d₁: Int
d₁ with 
⟨_, rfl | rfl⟩: ∃ n, d₁ = ↑n ∨ d₁ = -↑n
⟨
_: Nat
_
⟨_, rfl | rfl⟩: ∃ n, d₁ = ↑n ∨ d₁ = -↑n
, 
rfl: d₁ = ↑w✝
rfl
rfl | rfl: d₁ = ↑w✝ ∨ d₁ = -↑w✝
 | 
rfl: d₁ = -↑w✝
rfl
⟨_, rfl | rfl⟩: ∃ n, d₁ = ↑n ∨ d₁ = -↑n
⟩
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: ↑w✝ ≠ 0

intro.inl
n₁ /. ↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * ↑w✝
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: -↑w✝ ≠ 0

intro.inr
n₁ /. -↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * -↑w✝ 
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁<;>
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: ↑w✝ ≠ 0

intro.inl
n₁ /. ↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * ↑w✝
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: -↑w✝ ≠ 0

intro.inr
n₁ /. -↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * -↑w✝
  
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁rcases 
Int.eq_nat_or_neg: ∀ (a : Int), ∃ n, a = ↑n ∨ a = -↑n
Int.eq_nat_or_neg 
d₂: Int
d₂ with 
⟨_, rfl | rfl⟩: ∃ n, d₂ = ↑n ∨ d₂ = -↑n
⟨
_: Nat
_
⟨_, rfl | rfl⟩: ∃ n, d₂ = ↑n ∨ d₂ = -↑n
, 
rfl: d₂ = ↑w✝
rfl
rfl | rfl: d₂ = ↑w✝ ∨ d₂ = -↑w✝
 | 
rfl: d₂ = -↑w✝
rfl
⟨_, rfl | rfl⟩: ∃ n, d₂ = ↑n ∨ d₂ = -↑n
⟩
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0

intro.inl.intro.inl
n₁ /. ↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0

intro.inl.intro.inr
n₁ /. ↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * ↑w✝¹ 
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁<;>
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0

intro.inl.intro.inl
n₁ /. ↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0

intro.inl.intro.inr
n₁ /. ↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: -↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0

intro.inr.intro.inl
n₁ /. -↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * -↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: -↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0

intro.inr.intro.inr
n₁ /. -↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * -↑w✝¹
  
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁simp_all [
divInt_neg': ∀ (num den : Int), num /. -den = -num /. den
divInt_neg', 
Int.ofNat_eq_zero: ∀ {n : Nat}, ↑n = 0 ↔ n = 0
Int.ofNat_eq_zero, 
Int.neg_eq_zero: ∀ {a : Int}, -a = 0 ↔ a = 0
Int.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 = -a
Int.eq_neg_comm, 
eq_comm: ∀ {α : Sort ?u.14102} {a b : α}, a = b ↔ b = a
eq_comm]
Goals accomplished! 🐙

theorem 
divInt_mul_left: ∀ {n d a : Int}, a ≠ 0 → a * n /. (a * d) = n /. d
divInt_mul_left {
a: Int
a : 
Int: Type
Int} (
a0: a ≠ 0
a0 : 
a: Int
a ≠ 
0: ?m.15110
0) : (
a: Int
a * 
n: ?m.15051
n) /. (
a: Int
a * 
d: ?m.15102
d) = 
n: ?m.15051
n /. 
d: ?m.15102
d :=