[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
⊢ ↑n / ↑1 = ↑n
[PROOFSTEP]
rw [Nat.cast_one, div_one]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n
[PROOFSTEP]
rw [← Int.cast_ofNat, cast_coe_int, Int.cast_ofNat]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r) a
[PROOFSTEP]
simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
[PROOFSTEP]
have b0' : b ≠ 0 := by
  refine' mt _ b0
  simp (config := { contextual := true })
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b ≠ 0
[PROOFSTEP]
refine' mt _ b0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
⊢ b = 0 → ↑b = 0
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
⊢ ↑(a /. b) = ↑a / ↑b
[PROOFSTEP]
cases' e : a /. b with n d h c
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑(mk' n d) = ↑a / ↑b
[PROOFSTEP]
have d0 : (d : α) ≠ 0 := by
  intro d0
  have dd := den_dvd a b
  cases' show (d : ℤ) ∣ b by rwa [e] at dd  with k ke
  have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_ofNat]
  rw [d0, zero_mul] at this
  contradiction
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
⊢ ↑d ≠ 0
[PROOFSTEP]
intro d0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
⊢ False
[PROOFSTEP]
have dd := den_dvd a b
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ False
[PROOFSTEP]
cases' show (d : ℤ) ∣ b by rwa [e] at dd  with k ke
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ ↑d ∣ b
[PROOFSTEP]
rwa [e] at dd
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ False
[PROOFSTEP]
have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_ofNat]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ ↑b = ↑d * ↑k
[PROOFSTEP]
rw [ke, Int.cast_mul, Int.cast_ofNat]
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = ↑d * ↑k
⊢ False
[PROOFSTEP]
rw [d0, zero_mul] at this
[GOAL]
case intro
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
this : ↑b = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = mk' n d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
[PROOFSTEP]
rw [num_den'] at e
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
⊢ ↑(mk' n d) = ↑a / ↑b
[PROOFSTEP]
have := congr_arg ((↑) : ℤ → α) ((divInt_eq_iff b0' <| ne_of_gt <| Int.coe_nat_pos.2 h.bot_lt).1 e)
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑(a * ↑d) = ↑(n * b)
⊢ ↑(mk' n d) = ↑a / ↑b
[PROOFSTEP]
rw [Int.cast_mul, Int.cast_mul, Int.cast_ofNat] at this
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑(mk' n d) = ↑a / ↑b
[PROOFSTEP]
apply Eq.symm
[GOAL]
case mk'.h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
e : a /. b = n /. ↑d
d0 : ↑d ≠ 0
this : ↑a * ↑d = ↑n * ↑b
⊢ ↑a / ↑b = ↑(mk' n d)
[PROOFSTEP]
rw [cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq, ← mul_assoc, this, mul_assoc,
  mul_inv_cancel b0, mul_one]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ + mk' n₂ d₂) = ↑(mk' n₁ d₁) + ↑(mk' n₂ d₂)
[PROOFSTEP]
have d₁0' : (d₁ : ℤ) ≠ 0 := Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₁0 ; exact d₁0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
[PROOFSTEP]
rw [e] at d₁0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑0 ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
[PROOFSTEP]
exact d₁0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
⊢ ↑(mk' n₁ d₁ + mk' n₂ d₂) = ↑(mk' n₁ d₁) + ↑(mk' n₂ d₂)
[PROOFSTEP]
have d₂0' : (d₂ : ℤ) ≠ 0 := Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₂0 ; exact d₂0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
[PROOFSTEP]
rw [e] at d₂0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑0 ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
[PROOFSTEP]
exact d₂0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ + mk' n₂ d₂) = ↑(mk' n₁ d₁) + ↑(mk' n₂ d₂)
[PROOFSTEP]
rw [num_den', num_den', add_def'' d₁0' d₂0']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑((n₁ * ↑d₂ + n₂ * ↑d₁) /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) + ↑(n₂ /. ↑d₂)
[PROOFSTEP]
suffices
  (n₁ * (d₂ * ((d₂ : α)⁻¹ * (d₁ : α)⁻¹)) + n₂ * (d₁ * (d₂ : α)⁻¹) * (d₁ : α)⁻¹ : α) = n₁ * (d₁ : α)⁻¹ + n₂ * (d₂ : α)⁻¹
  by
  rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero]
  · simpa [division_def, left_distrib, right_distrib, mul_inv_rev, d₁0, d₂0, mul_assoc]
  all_goals simp [d₁0, d₂0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑((n₁ * ↑d₂ + n₂ * ↑d₁) /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) + ↑(n₂ /. ↑d₂)
[PROOFSTEP]
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑(n₁ * ↑d₂ + n₂ * ↑d₁) / ↑(↑d₁ * ↑d₂) = ↑n₁ / ↑↑d₁ + ↑n₂ / ↑↑d₂
[PROOFSTEP]
simpa [division_def, left_distrib, right_distrib, mul_inv_rev, d₁0, d₂0, mul_assoc]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑↑d₂ ≠ 0
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑↑d₁ ≠ 0
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
[PROOFSTEP]
all_goals simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑↑d₂ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑↑d₁ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑n₁ * (↑d₂ * ((↑d₂)⁻¹ * (↑d₁)⁻¹)) + ↑n₂ * (↑d₁ * (↑d₂)⁻¹) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
[PROOFSTEP]
rw [← mul_assoc (d₂ : α), mul_inv_cancel d₂0, one_mul, (Nat.cast_commute _ _).eq]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * ((↑d₂)⁻¹ * ↑d₁) * (↑d₁)⁻¹ = ↑n₁ * (↑d₁)⁻¹ + ↑n₂ * (↑d₂)⁻¹
[PROOFSTEP]
simp [d₁0, mul_assoc]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
⊢ ↑(-mk' n d) = -↑(mk' n d)
[PROOFSTEP]
simpa only [cast_def] using
  show (↑(-n) / d : α) = -(n / d) by rw [div_eq_mul_inv, div_eq_mul_inv, Int.cast_neg, neg_mul_eq_neg_mul]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
⊢ ↑(-n) / ↑d = -(↑n / ↑d)
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, Int.cast_neg, neg_mul_eq_neg_mul]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
have : ((-n).den : α) ≠ 0 := by cases n; exact n0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
⊢ ↑(-n).den ≠ 0
[PROOFSTEP]
cases n
[GOAL]
case mk'
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m : ℚ
m0 : ↑m.den ≠ 0
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
n0 : ↑(mk' num✝ den✝).den ≠ 0
⊢ ↑(-mk' num✝ den✝).den ≠ 0
[PROOFSTEP]
exact n0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
this : ↑(-n).den ≠ 0
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
simp [sub_eq_add_neg, cast_add_of_ne_zero m0 this]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
[PROOFSTEP]
have d₁0' : (d₁ : ℤ) ≠ 0 := Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₁0 ; exact d₁0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
[PROOFSTEP]
rw [e] at d₁0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑0 ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
[PROOFSTEP]
exact d₁0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
[PROOFSTEP]
have d₂0' : (d₂ : ℤ) ≠ 0 := Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₂0 ; exact d₂0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
[PROOFSTEP]
rw [e] at d₂0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑0 ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
[PROOFSTEP]
exact d₂0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
[PROOFSTEP]
rw [num_den', num_den', mul_def' d₁0' d₂0']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(n₁ * n₂ /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) * ↑(n₂ /. ↑d₂)
[PROOFSTEP]
suffices (n₁ * (n₂ * (d₂ : α)⁻¹ * (d₁ : α)⁻¹) : α) = n₁ * ((d₁ : α)⁻¹ * (n₂ * (d₂ : α)⁻¹))
  by
  rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero]
  · simpa [division_def, mul_inv_rev, d₁0, d₂0, mul_assoc]
  all_goals simp [d₁0, d₂0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(n₁ * n₂ /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) * ↑(n₂ /. ↑d₂)
[PROOFSTEP]
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(n₁ * n₂) / ↑(↑d₁ * ↑d₂) = ↑n₁ / ↑↑d₁ * (↑n₂ / ↑↑d₂)
[PROOFSTEP]
simpa [division_def, mul_inv_rev, d₁0, d₂0, mul_assoc]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₂ ≠ 0
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₁ ≠ 0
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
[PROOFSTEP]
all_goals simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₂ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₁ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
[PROOFSTEP]
rw [(d₁.commute_cast (_ : α)).inv_right₀.eq]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
⊢ ↑(↑Nat.zero)⁻¹ = (↑Nat.zero)⁻¹
[PROOFSTEP]
simp
[GOAL]
case succ
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Nat.succ n))⁻¹ = (↑(Nat.succ n))⁻¹
[PROOFSTEP]
rw [cast_def, inv_coe_nat_num, inv_coe_nat_den, if_neg n.succ_ne_zero,
  Int.sign_eq_one_of_pos (Nat.cast_pos.mpr n.succ_pos), Int.cast_one, one_div]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹
[PROOFSTEP]
cases' n with n n
[GOAL]
case ofNat
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹
[PROOFSTEP]
simp [ofInt_eq_cast, cast_inv_nat]
[GOAL]
case negSucc
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹
[PROOFSTEP]
simp only [ofInt_eq_cast, Int.cast_negSucc, ← Nat.cast_succ, cast_neg, inv_neg, cast_inv_nat]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
[PROOFSTEP]
have _ : (n : ℤ) ≠ 0 := fun e => by rw [e] at n0 ; exact n0 Int.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
e : n = 0
⊢ False
[PROOFSTEP]
rw [e] at n0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑0 ≠ 0
d0 : ↑d ≠ 0
e : n = 0
⊢ False
[PROOFSTEP]
exact n0 Int.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝ : n ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
[PROOFSTEP]
have _ : (d : ℤ) ≠ 0 := Int.coe_nat_ne_zero.2 fun e => by rw [e] at d0 ; exact d0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝ : n ≠ 0
e : d = 0
⊢ False
[PROOFSTEP]
rw [e] at d0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑0 ≠ 0
x✝ : n ≠ 0
e : d = 0
⊢ False
[PROOFSTEP]
exact d0 Nat.cast_zero
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
[PROOFSTEP]
rw [num_den', inv_def']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(↑d /. n) = (↑(n /. ↑d))⁻¹
[PROOFSTEP]
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, inv_div]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑↑d ≠ 0
[PROOFSTEP]
simp [n0, d0]
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
simp [n0, d0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
have : (n⁻¹.den : ℤ) ∣ n.num := by
  conv in n⁻¹.den => rw [← @num_den n, inv_def']
  apply den_dvd
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑n⁻¹.den ∣ n.num
[PROOFSTEP]
conv in n⁻¹.den => rw [← @num_den n, inv_def']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
| n⁻¹.den
[PROOFSTEP]
rw [← @num_den n, inv_def']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
| n⁻¹.den
[PROOFSTEP]
rw [← @num_den n, inv_def']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
| n⁻¹.den
[PROOFSTEP]
rw [← @num_den n, inv_def']
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑(↑n.den /. n.num).den ∣ n.num
[PROOFSTEP]
apply den_dvd
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
have : (n⁻¹.den : α) = 0 → (n.num : α) = 0 := fun h =>
  by
  let ⟨k, e⟩ := this
  have := congr_arg ((↑) : ℤ → α) e; rwa [Int.cast_mul, Int.cast_ofNat, h, zero_mul] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
⊢ ↑n.num = 0
[PROOFSTEP]
let ⟨k, e⟩ := this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
⊢ ↑n.num = 0
[PROOFSTEP]
have := congr_arg ((↑) : ℤ → α) e
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
this : ↑n.num = ↑(↑n⁻¹.den * k)
⊢ ↑n.num = 0
[PROOFSTEP]
rwa [Int.cast_mul, Int.cast_ofNat, h, zero_mul] at this
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
this : ↑n⁻¹.den = 0 → ↑n.num = 0
⊢ ↑(m / n) = ↑m / ↑n
[PROOFSTEP]
rw [division_def, cast_mul_of_ne_zero md (mt this nn), cast_inv_of_ne_zero nn nd, division_def]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
⊢ ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂) ↔ mk' n₁ d₁ = mk' n₂ d₂
[PROOFSTEP]
refine' ⟨fun h => _, congr_arg _⟩
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
⊢ mk' n₁ d₁ = mk' n₂ d₂
[PROOFSTEP]
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
[PROOFSTEP]
have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(mk' n₁ d₁) = ↑(mk' n₂ d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ mk' n₁ d₁ = mk' n₂ d₂
[PROOFSTEP]
rw [num_den', num_den'] at h ⊢
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
[PROOFSTEP]
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑n₁ / ↑↑d₁ = ↑n₂ / ↑↑d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
[PROOFSTEP]
simp [d₁0, d₂0] at h ⊢
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₂ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0] at h ⊢
[GOAL]
case b0
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
h : ↑(n₁ /. ↑d₁) = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ ↑↑d₁ ≠ 0
[PROOFSTEP]
simp [d₁0, d₂0] at h ⊢
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
h : ↑n₁ / ↑d₁ = ↑n₂ / ↑d₂
⊢ mkRat n₁ d₁ = mkRat n₂ d₂
[PROOFSTEP]
rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq, ← mul_assoc, ←
  division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_ofNat d₁, ← Int.cast_mul, ← Int.cast_ofNat d₂, ←
  Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0] at h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ ↑n = 0 ↔ n = 0
[PROOFSTEP]
rw [← cast_zero, cast_inj]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ ↑(bit1 n) = bit1 ↑n
[PROOFSTEP]
rw [bit1, cast_add, cast_one, cast_bit0]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n : ℚ
⊢ bit0 ↑n + 1 = bit1 ↑n
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a b : ℤ
⊢ ↑(a /. b) = ↑a / ↑b
[PROOFSTEP]
simp only [divInt_eq_div, cast_div, cast_coe_int]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
r : ℚ
hr : 0 < r
⊢ 0 < ↑r
[PROOFSTEP]
rw [Rat.cast_def]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
r : ℚ
hr : 0 < r
⊢ 0 < ↑r.num / ↑r.den
[PROOFSTEP]
exact div_pos (Int.cast_pos.2 <| num_pos_iff_pos.2 hr) (Nat.cast_pos.2 r.pos)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
m n : ℚ
⊢ m < n → ↑m < ↑n
[PROOFSTEP]
simpa only [sub_pos, cast_sub] using @cast_pos_of_pos K _ (n - m)
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
n : ℚ
⊢ 0 ≤ ↑n ↔ 0 ≤ n
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
n : ℚ
⊢ ↑n ≤ 0 ↔ n ≤ 0
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
n : ℚ
⊢ 0 < ↑n ↔ 0 < n
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
n : ℚ
⊢ ↑n < 0 ↔ n < 0
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
q : ℚ
⊢ ↑|q| = |↑q|
[PROOFSTEP]
simp [abs_eq_max_neg]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Icc ↑a ↑b = Icc a b
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Icc ↑a ↑b ↔ x ∈ Icc a b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Ico ↑a ↑b = Ico a b
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ico ↑a ↑b ↔ x ∈ Ico a b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Ioc ↑a ↑b = Ioc a b
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioc ↑a ↑b ↔ x ∈ Ioc a b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b : ℚ
⊢ Rat.cast ⁻¹' Ioo ↑a ↑b = Ioo a b
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a b x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioo ↑a ↑b ↔ x ∈ Ioo a b
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a : ℚ
⊢ Rat.cast ⁻¹' Ici ↑a = Ici a
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ici ↑a ↔ x ∈ Ici a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a : ℚ
⊢ Rat.cast ⁻¹' Iic ↑a = Iic a
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Iic ↑a ↔ x ∈ Iic a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a : ℚ
⊢ Rat.cast ⁻¹' Ioi ↑a = Ioi a
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Ioi ↑a ↔ x ∈ Ioi a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a : ℚ
⊢ Rat.cast ⁻¹' Iio ↑a = Iio a
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : LinearOrderedField K
a x : ℚ
⊢ x ∈ Rat.cast ⁻¹' Iio ↑a ↔ x ∈ Iio a
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ ↑f ↑q = ↑q
[PROOFSTEP]
rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
k : Type u_5
inst✝¹ : DivisionRing k
inst✝ : RingHomClass F ℚ k
f : F
r : ℚ
⊢ ↑f r = ↑r
[PROOFSTEP]
rw [← map_ratCast f, Rat.cast_id]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M₀ : Type u_5
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m
r : ℚ
⊢ ↑f r = ↑g r
[PROOFSTEP]
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_ofNat, eq_on_inv₀ f g]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M₀ : Type u_5
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m
r : ℚ
⊢ ↑f ↑↑r.den = ↑g ↑↑r.den
[PROOFSTEP]
apply h
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M₀ : Type u_5
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : ↑f (-1) = ↑g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → ↑f ↑n = ↑g ↑n
⊢ ↑(comp ↑f ↑(Int.castRingHom ℚ)) (-1) = ↑(comp ↑g ↑(Int.castRingHom ℚ)) (-1)
[PROOFSTEP]
simpa
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
M₀ : Type u_5
inst✝¹ : MonoidWithZero M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
same_on_neg_one : ↑f (-1) = ↑g (-1)
same_on_pnat : ∀ (n : ℕ), 0 < n → ↑f ↑n = ↑g ↑n
⊢ ∀ (n : ℕ), 0 < n → ↑(comp ↑f ↑(Int.castRingHom ℚ)) ↑n = ↑(comp ↑g ↑(Int.castRingHom ℚ)) ↑n
[PROOFSTEP]
simpa
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : DivisionRing K
a : ℚ
⊢ a • 0 = 0
[PROOFSTEP]
rw [smul_def, mul_zero]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : DivisionRing K
a : ℚ
x y : K
⊢ a • (x + y) = a • x + a • y
[PROOFSTEP]
rw [smul_def, smul_def, smul_def, mul_add]
[GOAL]
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
K : Type u_5
inst✝ : DivisionRing K
a : ℚ
x y : K
⊢ (a • x) • y = a • x • y
[PROOFSTEP]
simp only [smul_def, smul_eq_mul, mul_assoc]


[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