[GOAL]
a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a
[PROOFSTEP]
cases' e : a /. b with n d h c
[GOAL]
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ (mk' n d).num ∣ a
[PROOFSTEP]
rw [Rat.num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e 
[GOAL]
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ (mk' n d).num ∣ a
[PROOFSTEP]
refine' Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.coe_nat_dvd.2 <| c.dvd_of_dvd_mul_right _
[GOAL]
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ Int.natAbs n ∣ Int.natAbs a * d
[PROOFSTEP]
have := congr_arg Int.natAbs e
[GOAL]
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs (a * ↑d) = Int.natAbs (n * b)
⊢ Int.natAbs n ∣ Int.natAbs a * d
[PROOFSTEP]
simp only [Int.natAbs_mul, Int.natAbs_ofNat] at this 
[GOAL]
case mk'
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
this : Int.natAbs a * d = Int.natAbs n * Int.natAbs b
⊢ Int.natAbs n ∣ Int.natAbs a * d
[PROOFSTEP]
simp [this]
[GOAL]
a b : ℤ
⊢ ↑(a /. b).den ∣ b
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
a b : ℤ
b0 : b = 0
⊢ ↑(a /. b).den ∣ b
[PROOFSTEP]
simp [b0]
[GOAL]
case neg
a b : ℤ
b0 : ¬b = 0
⊢ ↑(a /. b).den ∣ b
[PROOFSTEP]
cases' e : a /. b with n d h c
[GOAL]
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d).den ∣ b
[PROOFSTEP]
rw [num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e 
[GOAL]
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑(mk' n d).den ∣ b
[PROOFSTEP]
refine' Int.dvd_natAbs.1 <| Int.coe_nat_dvd.2 <| c.symm.dvd_of_dvd_mul_left _
[GOAL]
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ d ∣ Int.natAbs n * Int.natAbs b
[PROOFSTEP]
rw [← Int.natAbs_mul, ← Int.coe_nat_dvd, Int.dvd_natAbs, ← e]
[GOAL]
case neg.mk'
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d
[PROOFSTEP]
simp
[GOAL]
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
[PROOFSTEP]
obtain rfl | hn := eq_or_ne n 0
[GOAL]
case inl
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ c, 0 = c * q.num ∧ d = c * ↑q.den
[PROOFSTEP]
simp [qdf]
[GOAL]
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
[PROOFSTEP]
have : q.num * d = n * ↑q.den := by
  refine' (divInt_eq_iff _ hd).mp _
  · exact Int.coe_nat_ne_zero.mpr (Rat.den_nz _)
  · rwa [num_den]
[GOAL]
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * ↑q.den
[PROOFSTEP]
refine' (divInt_eq_iff _ hd).mp _
[GOAL]
case refine'_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
exact Int.coe_nat_ne_zero.mpr (Rat.den_nz _)
[GOAL]
case refine'_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num /. ↑q.den = n /. d
[PROOFSTEP]
rwa [num_den]
[GOAL]
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
[PROOFSTEP]
have hqdn : q.num ∣ n := by
  rw [qdf]
  exact Rat.num_dvd _ hd
[GOAL]
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ q.num ∣ n
[PROOFSTEP]
rw [qdf]
[GOAL]
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
⊢ (n /. d).num ∣ n
[PROOFSTEP]
exact Rat.num_dvd _ hd
[GOAL]
case inr
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ ∃ c, n = c * q.num ∧ d = c * ↑q.den
[PROOFSTEP]
refine' ⟨n / q.num, _, _⟩
[GOAL]
case inr.refine'_1
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ n = n / q.num * q.num
[PROOFSTEP]
rw [Int.ediv_mul_cancel hqdn]
[GOAL]
case inr.refine'_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ d = n / q.num * ↑q.den
[PROOFSTEP]
refine' Int.eq_mul_div_of_mul_eq_mul_of_dvd_left _ hqdn this
[GOAL]
case inr.refine'_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ q.num ≠ 0
[PROOFSTEP]
rw [qdf]
[GOAL]
case inr.refine'_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0
[PROOFSTEP]
exact Rat.num_ne_zero_of_ne_zero ((divInt_ne_zero hd).mpr hn)
[GOAL]
n d : ℤ
⊢ (n /. d).num = Int.sign d * n / ↑(Int.gcd n d)
[PROOFSTEP]
rcases d with ((_ | _) | _)
[GOAL]
case ofNat.zero
n : ℤ
⊢ (n /. Int.ofNat Nat.zero).num = Int.sign (Int.ofNat Nat.zero) * n / ↑(Int.gcd n (Int.ofNat Nat.zero))
[PROOFSTEP]
rw [← Int.div_eq_ediv_of_dvd]
[GOAL]
case ofNat.succ
n : ℤ
n✝ : ℕ
⊢ (n /. Int.ofNat (Nat.succ n✝)).num = Int.sign (Int.ofNat (Nat.succ n✝)) * n / ↑(Int.gcd n (Int.ofNat (Nat.succ n✝)))
[PROOFSTEP]
rw [← Int.div_eq_ediv_of_dvd]
[GOAL]
case negSucc
n : ℤ
a✝ : ℕ
⊢ (n /. Int.negSucc a✝).num = Int.sign (Int.negSucc a✝) * n / ↑(Int.gcd n (Int.negSucc a✝))
[PROOFSTEP]
rw [← Int.div_eq_ediv_of_dvd]
[GOAL]
case ofNat.zero
n : ℤ
⊢ (n /. Int.ofNat Nat.zero).num = Int.div (Int.sign (Int.ofNat Nat.zero) * n) ↑(Int.gcd n (Int.ofNat Nat.zero))
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
case ofNat.zero
n : ℤ
⊢ ↑(Int.gcd n (Int.ofNat Nat.zero)) ∣ Int.sign (Int.ofNat Nat.zero) * n
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
case ofNat.succ
n : ℤ
n✝ : ℕ
⊢ (n /. Int.ofNat (Nat.succ n✝)).num =
    Int.div (Int.sign (Int.ofNat (Nat.succ n✝)) * n) ↑(Int.gcd n (Int.ofNat (Nat.succ n✝)))
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
case ofNat.succ
n : ℤ
n✝ : ℕ
⊢ ↑(Int.gcd n (Int.ofNat (Nat.succ n✝))) ∣ Int.sign (Int.ofNat (Nat.succ n✝)) * n
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
case negSucc
n : ℤ
a✝ : ℕ
⊢ (n /. Int.negSucc a✝).num = Int.div (Int.sign (Int.negSucc a✝) * n) ↑(Int.gcd n (Int.negSucc a✝))
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
case negSucc
n : ℤ
a✝ : ℕ
⊢ ↑(Int.gcd n (Int.negSucc a✝)) ∣ Int.sign (Int.negSucc a✝) * n
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ, Int.zero_ediv, Int.ofNat_dvd_left,
  Nat.gcd_dvd_left]
[GOAL]
n d : ℤ
⊢ (n /. d).den = if d = 0 then 1 else Int.natAbs d / Int.gcd n d
[PROOFSTEP]
rcases d with ((_ | _) | _)
[GOAL]
case ofNat.zero
n : ℤ
⊢ (n /. Int.ofNat Nat.zero).den =
    if Int.ofNat Nat.zero = 0 then 1 else Int.natAbs (Int.ofNat Nat.zero) / Int.gcd n (Int.ofNat Nat.zero)
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ]
[GOAL]
case ofNat.succ
n : ℤ
n✝ : ℕ
⊢ (n /. Int.ofNat (Nat.succ n✝)).den =
    if Int.ofNat (Nat.succ n✝) = 0 then 1
    else Int.natAbs (Int.ofNat (Nat.succ n✝)) / Int.gcd n (Int.ofNat (Nat.succ n✝))
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ]
[GOAL]
case negSucc
n : ℤ
a✝ : ℕ
⊢ (n /. Int.negSucc a✝).den = if Int.negSucc a✝ = 0 then 1 else Int.natAbs (Int.negSucc a✝) / Int.gcd n (Int.negSucc a✝)
[PROOFSTEP]
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd, -Nat.cast_succ]
[GOAL]
q₁ q₂ : ℚ
⊢ (q₁ + q₂).den ∣ q₁.den * q₂.den
[PROOFSTEP]
rw [add_def, normalize_eq]
[GOAL]
q₁ q₂ : ℚ
⊢ (mk'
        ((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) /
          ↑(Nat.gcd (Int.natAbs (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den)) (q₁.den * q₂.den)))
        (q₁.den * q₂.den / Nat.gcd (Int.natAbs (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den)) (q₁.den * q₂.den))).den ∣
    q₁.den * q₂.den
[PROOFSTEP]
apply Nat.div_dvd_of_dvd
[GOAL]
case h
q₁ q₂ : ℚ
⊢ Nat.gcd (Int.natAbs (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den)) (q₁.den * q₂.den) ∣ q₁.den * q₂.den
[PROOFSTEP]
apply Nat.gcd_dvd_right
[GOAL]
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den
[PROOFSTEP]
rw [mul_def, normalize_eq]
[GOAL]
q₁ q₂ : ℚ
⊢ (mk' (q₁.num * q₂.num / ↑(Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den)))
        (q₁.den * q₂.den / Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den))).den ∣
    q₁.den * q₂.den
[PROOFSTEP]
apply Nat.div_dvd_of_dvd
[GOAL]
case h
q₁ q₂ : ℚ
⊢ Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den) ∣ q₁.den * q₂.den
[PROOFSTEP]
apply Nat.gcd_dvd_right
[GOAL]
q₁ q₂ : ℚ
⊢ (q₁ * q₂).num = q₁.num * q₂.num / ↑(Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den))
[PROOFSTEP]
rw [mul_def, normalize_eq]
[GOAL]
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den)
[PROOFSTEP]
rw [mul_def, normalize_eq]
[GOAL]
q : ℚ
⊢ (q * q).num = q.num * q.num
[PROOFSTEP]
rw [mul_num, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
[GOAL]
q : ℚ
⊢ Nat.coprime (Int.natAbs q.num * Int.natAbs q.num) (q.den * q.den)
[PROOFSTEP]
exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)
[GOAL]
q : ℚ
⊢ (q * q).den = q.den * q.den
[PROOFSTEP]
rw [Rat.mul_den, Int.natAbs_mul, Nat.coprime.gcd_eq_one, Nat.div_one]
[GOAL]
q : ℚ
⊢ Nat.coprime (Int.natAbs q.num * Int.natAbs q.num) (q.den * q.den)
[PROOFSTEP]
exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)
[GOAL]
q r : ℚ
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
[PROOFSTEP]
have hqd : (q.den : ℤ) ≠ 0 := Int.coe_nat_ne_zero_iff_pos.2 q.den_pos
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
[PROOFSTEP]
have hrd : (r.den : ℤ) ≠ 0 := Int.coe_nat_ne_zero_iff_pos.2 r.den_pos
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
[PROOFSTEP]
conv_lhs => rw [← @num_den q, ← @num_den r, Rat.add_def'' hqd hrd]
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q + r
[PROOFSTEP]
rw [← @num_den q, ← @num_den r, Rat.add_def'' hqd hrd]
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q + r
[PROOFSTEP]
rw [← @num_den q, ← @num_den r, Rat.add_def'' hqd hrd]
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q + r
[PROOFSTEP]
rw [← @num_den q, ← @num_den r, Rat.add_def'' hqd hrd]
[GOAL]
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
⊢ (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den) = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
[PROOFSTEP]
rw [mul_comm r.num q.den]
[GOAL]
n d : ℤ
d_ne_zero : d ≠ 0
⊢ ↑n / ↑d = n /. d
[PROOFSTEP]
rw [← Rat.divInt_eq_div]
[GOAL]
q r : ℚ
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
[PROOFSTEP]
let s := q.num * r.num /. (q.den * r.den : ℤ)
[GOAL]
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
[PROOFSTEP]
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.coe_nat_ne_zero_iff_pos.mpr (mul_pos q.pos r.pos)
[GOAL]
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
[PROOFSTEP]
obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ := exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.num) hs
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
[PROOFSTEP]
rw [c_mul_num, mul_assoc, mul_comm]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q * r).num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
nth_rw 1 [c_mul_den]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
repeat' rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * ((↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den)
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num) =
    c * ((↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den)
[PROOFSTEP]
apply mul_eq_mul_left_iff.2
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den ∨
    c = 0
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
      (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
intro
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
have h : _ = s :=
  @mul_def' q.num q.den r.num r.den (Int.coe_nat_ne_zero_iff_pos.mpr q.pos) (Int.coe_nat_ne_zero_iff_pos.mpr r.pos)
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den * (r.num /. ↑r.den) = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
rw [num_den, num_den] at h 
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
[PROOFSTEP]
rw [h]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * s.num = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑s.den
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ s.num * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den = (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑s.den
[PROOFSTEP]
apply Rat.eq_iff_mul_eq_mul.mp
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q * r = s
⊢ s = ↑(q.num * r.num) / ↑(↑q.den * ↑r.den)
[PROOFSTEP]
rw [← divInt_eq_div]
[GOAL]
q r : ℚ
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
[PROOFSTEP]
let s := divInt (q.num * r.den + r.num * q.den) (q.den * r.den : ℤ)
[GOAL]
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
[PROOFSTEP]
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.coe_nat_ne_zero_iff_pos.mpr (mul_pos q.pos r.pos)
[GOAL]
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
[PROOFSTEP]
obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ := exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.den + r.num * q.den) hs
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ (q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
[PROOFSTEP]
rw [c_mul_num, mul_assoc, mul_comm]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q + r).num = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
nth_rw 1 [c_mul_den]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
repeat' rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
[PROOFSTEP]
rw [Int.mul_assoc]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * (↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num) =
    c * ((↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den)
[PROOFSTEP]
apply mul_eq_mul_left_iff.2
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den ∨
    c = 0
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ¬c = 0 →
    ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
      (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
intro
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
have h : _ = s :=
  @add_def'' q.num q.den r.num r.den (Int.coe_nat_ne_zero_iff_pos.mpr q.pos) (Int.coe_nat_ne_zero_iff_pos.mpr r.pos)
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q.num /. ↑q.den + r.num /. ↑r.den = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
rw [num_den, num_den] at h 
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
[PROOFSTEP]
rw [h]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * s.num =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s.num * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den =
    (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑s.den
[PROOFSTEP]
apply Rat.eq_iff_mul_eq_mul.mp
[GOAL]
case intro.intro
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s = ↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)
[PROOFSTEP]
rw [← divInt_eq_div]
[GOAL]
q r : ℚ
⊢ (q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r, add_num_den' q (-r)]
[GOAL]
q : ℚ
⊢ q⁻¹ = ↑q.den / ↑q.num
[PROOFSTEP]
conv_lhs => rw [← @num_den q]
[GOAL]
q : ℚ
| q⁻¹
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
| q⁻¹
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
| q⁻¹
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
⊢ (q.num /. ↑q.den)⁻¹ = ↑q.den / ↑q.num
[PROOFSTEP]
rw [inv_def', divInt_eq_div]
[GOAL]
q : ℚ
⊢ ↑↑q.den / ↑q.num = ↑q.den / ↑q.num
[PROOFSTEP]
rfl
[GOAL]
q : ℚ
⊢ (-q)⁻¹ = -q⁻¹
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
[PROOFSTEP]
simp only [Rat.neg_def, Rat.inv_def', eq_self_iff_true, Rat.divInt_neg_den]
[GOAL]
q : ℚ
⊢ q * ↑q.den = ↑q.num
[PROOFSTEP]
suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1
  by
  conv => pattern (occs := 1) q; (rw [← @num_den q])
  simp only [coe_int_eq_divInt, coe_nat_eq_divInt, num_den] at this ⊢; assumption
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q * ↑q.den = ↑q.num
[PROOFSTEP]
conv => pattern (occs := 1) q; (rw [← @num_den q])
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q * ↑q.den = ↑q.num
[PROOFSTEP]
pattern (occs := 1) q; (rw [← @num_den q])
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q * ↑q.den = ↑q.num
[PROOFSTEP]
pattern (occs := 1) q; (rw [← @num_den q])
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q * ↑q.den = ↑q.num
[PROOFSTEP]
pattern (occs := 1) q
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q
[PROOFSTEP]
(rw [← @num_den q])
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
| q
[PROOFSTEP]
rw [← @num_den q]
[GOAL]
q : ℚ
this : q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
⊢ q.num /. ↑q.den * ↑q.den = ↑q.num
[PROOFSTEP]
simp only [coe_int_eq_divInt, coe_nat_eq_divInt, num_den] at this ⊢
[GOAL]
q : ℚ
this : q * (↑q.den /. 1) = q.num /. 1
⊢ q * (↑q.den /. 1) = q.num /. 1
[PROOFSTEP]
assumption
[GOAL]
q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
[PROOFSTEP]
have : (q.den : ℤ) ≠ 0 := ne_of_gt (by exact_mod_cast q.pos)
[GOAL]
q : ℚ
⊢ 0 < ↑q.den
[PROOFSTEP]
exact_mod_cast q.pos
[GOAL]
q : ℚ
this : ↑q.den ≠ 0
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
[PROOFSTEP]
rw [Rat.mul_def' this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
[GOAL]
m n : ℤ
hn : n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m
[PROOFSTEP]
replace hn : (n : ℚ) ≠ 0
[GOAL]
case hn
m n : ℤ
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
rwa [Ne.def, ← Int.cast_zero, coe_int_inj]
[GOAL]
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 ↔ n ∣ m
[PROOFSTEP]
constructor
[GOAL]
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ n ∣ m
[PROOFSTEP]
use((m : ℚ) / n).num
[GOAL]
case h
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
⊢ m = n * (↑m / ↑n).num
[PROOFSTEP]
have hk := Rat.coe_int_num_of_den_eq_one h
[GOAL]
case h
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑(↑m / ↑n).num = ↑m / ↑n
⊢ m = n * (↑m / ↑n).num
[PROOFSTEP]
simp_rw [eq_div_iff_mul_eq hn, ← Int.cast_mul] at hk 
[GOAL]
case h
m n : ℤ
hn : ↑n ≠ 0
h : (↑m / ↑n).den = 1
hk : ↑((↑m / ↑n).num * n) = ↑m
⊢ m = n * (↑m / ↑n).num
[PROOFSTEP]
rwa [mul_comm, eq_comm, coe_int_inj] at hk 
[GOAL]
case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
[PROOFSTEP]
rintro ⟨d, rfl⟩
[GOAL]
case mpr.intro
n : ℤ
hn : ↑n ≠ 0
d : ℤ
⊢ (↑(n * d) / ↑n).den = 1
[PROOFSTEP]
rw [Int.cast_mul, mul_comm, mul_div_cancel _ hn, Rat.coe_int_den]
[GOAL]
a b : ℤ
hb0 : 0 < b
h : Nat.coprime (Int.natAbs a) (Int.natAbs b)
⊢ (↑a / ↑b).num = a
[PROOFSTEP]
rw [← Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div, ← mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]
[GOAL]
a b : ℤ
hb0 : 0 < b
h : Nat.coprime (Int.natAbs a) (Int.natAbs b)
⊢ ↑(↑a / ↑b).den = b
[PROOFSTEP]
rw [← Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div, ← mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]
[GOAL]
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : Nat.coprime (Int.natAbs a) (Int.natAbs b)
h2 : Nat.coprime (Int.natAbs c) (Int.natAbs d)
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c ∧ b = d
[PROOFSTEP]
apply And.intro
[GOAL]
case left
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : Nat.coprime (Int.natAbs a) (Int.natAbs b)
h2 : Nat.coprime (Int.natAbs c) (Int.natAbs d)
h : ↑a / ↑b = ↑c / ↑d
⊢ a = c
[PROOFSTEP]
rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
[GOAL]
case right
a b c d : ℤ
hb0 : 0 < b
hd0 : 0 < d
h1 : Nat.coprime (Int.natAbs a) (Int.natAbs b)
h2 : Nat.coprime (Int.natAbs c) (Int.natAbs d)
h : ↑a / ↑b = ↑c / ↑d
⊢ b = d
[PROOFSTEP]
rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]
[GOAL]
n : ℤ
⊢ ↑(n / n) = ↑n / ↑n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n : ℤ
hn : n = 0
⊢ ↑(n / n) = ↑n / ↑n
[PROOFSTEP]
subst hn
[GOAL]
case pos
⊢ ↑(0 / 0) = ↑0 / ↑0
[PROOFSTEP]
simp only [Int.cast_zero, Int.zero_div, zero_div]
[GOAL]
case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n
[PROOFSTEP]
have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn 
[GOAL]
n : ℤ
hn : ¬n = 0
⊢ ↑n ≠ 0
[PROOFSTEP]
rwa [← coe_int_inj] at hn 
[GOAL]
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n
[PROOFSTEP]
simp only [Int.ediv_self hn, Int.cast_one, Ne.def, not_false_iff, div_self this]
[GOAL]
a b : ℤ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b
[PROOFSTEP]
rcases h with ⟨c, rfl⟩
[GOAL]
case intro
b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
[PROOFSTEP]
rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul, coe_int_div_self, Int.cast_mul, mul_div_assoc]
[GOAL]
a b : ℕ
h : b ∣ a
⊢ ↑(a / b) = ↑a / ↑b
[PROOFSTEP]
rcases h with ⟨c, rfl⟩
[GOAL]
case intro
b c : ℕ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b
[PROOFSTEP]
simp only [mul_comm b, Nat.mul_div_assoc c (dvd_refl b), Nat.cast_mul, mul_div_assoc, coe_nat_div_self]
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1
[PROOFSTEP]
rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_def', divInt_eq_div, Nat.cast_one]
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ (↑1 / ↑a).num = 1
[PROOFSTEP]
apply num_div_eq_of_coprime ha0
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime (Int.natAbs 1) (Int.natAbs a)
[PROOFSTEP]
rw [Int.natAbs_one]
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime 1 (Int.natAbs a)
[PROOFSTEP]
exact Nat.coprime_one_left _
[GOAL]
a : ℕ
ha0 : 0 < a
⊢ 0 < ↑a
[PROOFSTEP]
exact_mod_cast ha0
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ ↑(↑a)⁻¹.den = a
[PROOFSTEP]
rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_def', divInt_eq_div, Nat.cast_one]
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ ↑(↑1 / ↑a).den = a
[PROOFSTEP]
apply den_div_eq_of_coprime ha0
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime (Int.natAbs 1) (Int.natAbs a)
[PROOFSTEP]
rw [Int.natAbs_one]
[GOAL]
a : ℤ
ha0 : 0 < a
⊢ Nat.coprime 1 (Int.natAbs a)
[PROOFSTEP]
exact Nat.coprime_one_left _
[GOAL]
a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a
[PROOFSTEP]
rw [← Int.ofNat_inj, ← Int.cast_ofNat a, inv_coe_int_den_of_pos]
[GOAL]
a : ℕ
ha0 : 0 < a
⊢ 0 < ↑a
[PROOFSTEP]
rwa [Nat.cast_pos]
[GOAL]
a : ℤ
⊢ (↑a)⁻¹.num = Int.sign a
[PROOFSTEP]
induction a using Int.induction_on
[GOAL]
case hz
⊢ (↑0)⁻¹.num = Int.sign 0
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_num_of_pos, -Int.cast_negSucc, @eq_comm ℤ 1, Int.sign_eq_one_of_pos, ofInt_eq_cast]
[GOAL]
case hp
i✝ : ℕ
a✝ : (↑↑i✝)⁻¹.num = Int.sign ↑i✝
⊢ (↑(↑i✝ + 1))⁻¹.num = Int.sign (↑i✝ + 1)
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_num_of_pos, -Int.cast_negSucc, @eq_comm ℤ 1, Int.sign_eq_one_of_pos, ofInt_eq_cast]
[GOAL]
case hn
i✝ : ℕ
a✝ : (↑(-↑i✝))⁻¹.num = Int.sign (-↑i✝)
⊢ (↑(-↑i✝ - 1))⁻¹.num = Int.sign (-↑i✝ - 1)
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_num_of_pos, -Int.cast_negSucc, @eq_comm ℤ 1, Int.sign_eq_one_of_pos, ofInt_eq_cast]
[GOAL]
a : ℤ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else Int.natAbs a
[PROOFSTEP]
induction a using Int.induction_on
[GOAL]
case hz
⊢ (↑0)⁻¹.den = if 0 = 0 then 1 else Int.natAbs 0
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_den_of_pos, -Int.cast_negSucc, ofInt_eq_cast]
[GOAL]
case hp
i✝ : ℕ
a✝ : (↑↑i✝)⁻¹.den = if ↑i✝ = 0 then 1 else Int.natAbs ↑i✝
⊢ (↑(↑i✝ + 1))⁻¹.den = if ↑i✝ + 1 = 0 then 1 else Int.natAbs (↑i✝ + 1)
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_den_of_pos, -Int.cast_negSucc, ofInt_eq_cast]
[GOAL]
case hn
i✝ : ℕ
a✝ : (↑(-↑i✝))⁻¹.den = if -↑i✝ = 0 then 1 else Int.natAbs (-↑i✝)
⊢ (↑(-↑i✝ - 1))⁻¹.den = if -↑i✝ - 1 = 0 then 1 else Int.natAbs (-↑i✝ - 1)
[PROOFSTEP]
simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out, -Nat.cast_succ,
  inv_coe_nat_den_of_pos, -Int.cast_negSucc, ofInt_eq_cast]
[GOAL]
a : ℕ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else a
[PROOFSTEP]
simpa [-inv_coe_int_den, ofInt_eq_cast] using inv_coe_int_den a
[GOAL]
p : ℚ → Prop
h : ∀ (a b : ℤ), p (↑a / ↑b)
q : ℚ
⊢ p q
[PROOFSTEP]
have := h q.num q.den
[GOAL]
p : ℚ → Prop
h : ∀ (a b : ℤ), p (↑a / ↑b)
q : ℚ
this : p (↑q.num / ↑↑q.den)
⊢ p q
[PROOFSTEP]
rwa [Int.cast_ofNat, num_div_den q] at this 
[GOAL]
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ p (↑r.num / ↑↑r.den)
[PROOFSTEP]
convert hr
[GOAL]
case h.e'_1
p : ℚ → Prop
x✝ : ∃ r, p r
r : ℚ
hr : p r
⊢ ↑r.num / ↑↑r.den = r
[PROOFSTEP]
convert num_div_den r
