[GOAL]
d : ℕ
h : d ≠ 0
w : Nat.coprime (Int.natAbs 0) d
⊢ mk' 0 d = 0
[PROOFSTEP]
congr
[GOAL]
q : ℚ
⊢ q.num = 0 ↔ q = 0
[PROOFSTEP]
induction q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (mk' num✝ den✝).num = 0 ↔ mk' num✝ den✝ = 0
[PROOFSTEP]
constructor
[GOAL]
case mk'.mp
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (mk' num✝ den✝).num = 0 → mk' num✝ den✝ = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mk'.mp
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs 0) den✝
⊢ mk' 0 den✝ = 0
[PROOFSTEP]
exact zero_mk _ _ _
[GOAL]
case mk'.mpr
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ mk' num✝ den✝ = 0 → (mk' num✝ den✝).num = 0
[PROOFSTEP]
exact congr_arg num
[GOAL]
a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0
[PROOFSTEP]
rw [← zero_divInt b, divInt_eq_iff b0 b0, zero_mul, mul_eq_zero, or_iff_left b0]
[GOAL]
C : ℚ → Sort u
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
H : (n : ℤ) → (d : ℕ) → 0 < d → Nat.coprime (Int.natAbs n) d → C (n /. ↑d)
⊢ C (mk' n d)
[PROOFSTEP]
rw [num_den']
[GOAL]
C : ℚ → Sort u
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
H : (n : ℤ) → (d : ℕ) → 0 < d → Nat.coprime (Int.natAbs n) d → C (n /. ↑d)
⊢ C (n /. ↑d)
[PROOFSTEP]
exact H n d (Nat.pos_of_ne_zero h) c
[GOAL]
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
generalize ha : a /. b = x
[GOAL]
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
x : ℚ
ha : a /. b = x
⊢ f x (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
cases' x with n₁ d₁ h₁ c₁
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = mk' n₁ d₁
⊢ f (mk' n₁ d₁) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [num_den'] at ha 
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f (mk' n₁ d₁) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
generalize hc : c /. d = x
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
x : ℚ
hc : c /. d = x
⊢ f (mk' n₁ d₁) x = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
cases' x with n₂ d₂ h₂ c₂
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = mk' n₂ d₂
⊢ f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [num_den'] at hc 
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [fv]
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
have d₁0 := ne_of_gt (Int.ofNat_lt.2 $ Nat.pos_of_ne_zero h₁)
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ ↑0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
have d₂0 := ne_of_gt (Int.ofNat_lt.2 $ Nat.pos_of_ne_zero h₂)
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ ↑0
d₂0 : ↑d₂ ≠ ↑0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
exact (divInt_eq_iff (f0 d₁0 d₂0) (f0 b0 d0)).2 (H ((divInt_eq_iff b0 d₁0).1 ha) ((divInt_eq_iff d0 d₂0).1 hc))
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ n /. ↑d + 0 = n /. ↑d
[PROOFSTEP]
rw [← zero_divInt d, add_def'', zero_mul, add_zero, divInt_mul_right]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case b0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case d0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ 0 + n /. ↑d = n /. ↑d
[PROOFSTEP]
rw [← zero_divInt d, add_def'', zero_mul, zero_add, divInt_mul_right]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case b0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case d0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ n₁ /. ↑d₁ + n₂ /. ↑d₂ = n₂ /. ↑d₂ + n₁ /. ↑d₁
[PROOFSTEP]
simp [h₁, h₂, add_comm, mul_comm]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ + n₂ /. ↑d₂ + n₃ /. ↑d₃ = n₁ /. ↑d₁ + (n₂ /. ↑d₂ + n₃ /. ↑d₃)
[PROOFSTEP]
simp [h₁, h₂, h₃]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ ((n₁ * ↑d₂ + n₂ * ↑d₁) * ↑d₃ + n₃ * (↑d₁ * ↑d₂)) /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ + n₃ * ↑d₂) * ↑d₁) /. (↑d₁ * (↑d₂ * ↑d₃))
[PROOFSTEP]
rw [mul_assoc, add_mul, add_mul, mul_assoc, add_assoc]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂))) /. (↑d₁ * (↑d₂ * ↑d₃)) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁)) /. (↑d₁ * (↑d₂ * ↑d₃))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂) = n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁
[PROOFSTEP]
ac_rfl
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ -(n /. ↑d) + n /. ↑d = 0
[PROOFSTEP]
simp [h, mkRat_add_mkRat]
[GOAL]
a b c : ℚ
⊢ 0 /. 1 = 0
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match 0, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    0
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
⊢ 1 /. 1 = 1
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match 1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    1
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
⊢ -1 /. 1 = -1
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match -1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    -1
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
n : ℤ
⊢ n /. 1 = ↑n
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
n : ℤ
⊢ (match n, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    ↑n
[PROOFSTEP]
simp [mkRat, normalize]
[GOAL]
a b c : ℚ
n : ℤ
⊢ mk' n 1 = ↑n
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
n : ℤ
⊢ mkRat n 1 = ↑n
[PROOFSTEP]
simp [Rat.mkRat_eq, Rat.divInt_one]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ * (n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₂ /. ↑d₂ * (n₃ /. ↑d₃))
[PROOFSTEP]
simp [h₁, h₂, h₃, mul_ne_zero, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ /. ↑d₁ + n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₃ /. ↑d₃) + n₂ /. ↑d₂ * (n₃ /. ↑d₃)
[PROOFSTEP]
simp [h₁, h₂, h₃, mul_ne_zero]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ + n₂ * ↑d₁) * n₃ /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
[PROOFSTEP]
rw [← divInt_mul_right (Int.coe_nat_ne_zero.2 h₃), add_mul, add_mul]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ * n₃ * ↑d₃ + n₂ * ↑d₁ * n₃ * ↑d₃) /. (↑d₁ * ↑d₂ * ↑d₃ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
[PROOFSTEP]
ac_rfl
[GOAL]
a b c : ℚ
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
rw [Rat.mul_comm, Rat.add_mul, Rat.mul_comm, Rat.mul_comm c a]
[GOAL]
a b c : ℚ
⊢ 0 ≠ 1
[PROOFSTEP]
rw [ne_comm, ← divInt_one_one, divInt_ne_zero one_ne_zero]
[GOAL]
a b c : ℚ
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
[PROOFSTEP]
have n0 : n ≠ 0 := mt (by rintro rfl; simp) a0
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n = 0 → n /. ↑d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
a b c : ℚ
d : ℕ
h : d ≠ 0
a0 : 0 /. ↑d ≠ 0
⊢ 0 /. ↑d = 0
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
[PROOFSTEP]
simpa [h, n0, mul_comm] using @divInt_mul_right 1 1 (n * d) (by simp [h, n0])
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n * ↑d ≠ 0
[PROOFSTEP]
simp [h, n0]
[GOAL]
a b c : ℚ
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp only [coe_int_eq_divInt, add_def'' one_ne_zero one_ne_zero, ← divInt_one_one, Nat.cast_add, Nat.cast_one, mul_one]
[GOAL]
a b c : ℚ
⊢ 0⁻¹ = 0
[PROOFSTEP]
change Rat.inv 0 = 0
[GOAL]
a b c : ℚ
⊢ Rat.inv 0 = 0
[PROOFSTEP]
rw [Rat.inv_def]
[GOAL]
a b c : ℚ
⊢ ↑0.den /. 0.num = 0
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
⊢ Nontrivial ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommSemiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Semiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddRightCancelSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Monoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Semigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c p q : ℚ
⊢ p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
conv =>
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
lhs
[GOAL]
a b c p q : ℚ
| p = q
[PROOFSTEP]
rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
⊢ p.num /. ↑p.den = q.num /. ↑q.den ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
apply Rat.divInt_eq_iff
[GOAL]
case z₁
a b c p q : ℚ
⊢ ↑p.den ≠ 0
[PROOFSTEP]
rw [← Nat.cast_zero, Ne, Int.ofNat_inj]
[GOAL]
case z₁
a b c p q : ℚ
⊢ ¬p.den = 0
[PROOFSTEP]
apply den_nz
[GOAL]
case z₂
a b c p q : ℚ
⊢ ↑q.den ≠ 0
[PROOFSTEP]
rw [← Nat.cast_zero, Ne, Int.ofNat_inj]
[GOAL]
case z₂
a b c p q : ℚ
⊢ ¬q.den = 0
[PROOFSTEP]
apply den_nz
[GOAL]
a b c q : ℚ
hq : q.num = 0
⊢ q = 0
[PROOFSTEP]
have : q = q.num /. q.den := num_den.symm
[GOAL]
a b c q : ℚ
hq : q.num = 0
this : q = q.num /. ↑q.den
⊢ q = 0
[PROOFSTEP]
simpa [hq] using this
[GOAL]
a b c q : ℚ
x✝ : q = 0
⊢ q.num = 0
[PROOFSTEP]
simp [*]
[GOAL]
a b c q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0
[PROOFSTEP]
simpa [this] using hqnd
[GOAL]
a b c q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0
[PROOFSTEP]
simpa [this] using hqnd
[GOAL]
a b c q r : ℚ
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
have hq' : (↑q.den : ℤ) ≠ 0 := by have := den_nz q; simpa
[GOAL]
a b c q r : ℚ
⊢ ↑q.den ≠ 0
[PROOFSTEP]
have := den_nz q
[GOAL]
a b c q r : ℚ
this : q.den ≠ 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
have hr' : (↑r.den : ℤ) ≠ 0 := by have := den_nz r; simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ ↑r.den ≠ 0
[PROOFSTEP]
have := den_nz r
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
this : r.den ≠ 0
⊢ ↑r.den ≠ 0
[PROOFSTEP]
simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
suffices q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den) by simpa [num_den] using this
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
this : q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
simpa [num_den] using this
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
simp [mul_def' hq' hr']
[GOAL]
a b c q r : ℚ
hr : r.num = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
[PROOFSTEP]
have hr' : r = 0 := zero_of_num_zero hr
[GOAL]
a b c q r : ℚ
hr : r.num = 0
hr' : r = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
[PROOFSTEP]
simp [*]
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q * r⁻¹ = q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹
[PROOFSTEP]
simp [num_den]
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹ = q.num /. ↑q.den * (↑r.den /. r.num)
[PROOFSTEP]
rw [inv_def']
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
simpa using den_nz q
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c
[PROOFSTEP]
simp [h]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c
[PROOFSTEP]
rw [add_def'' h h, divInt_eq_iff h (mul_ne_zero h h)]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c
[PROOFSTEP]
simp [add_mul, mul_assoc]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
by_cases d0 : d = 0
[GOAL]
case pos
a b c : ℚ
n d : ℤ
d0 : d = 0
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
simp [d0, div_zero]
[GOAL]
case neg
a b c : ℚ
n d : ℤ
d0 : ¬d = 0
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
simp [division_def, coe_int_eq_divInt, mul_def' one_ne_zero d0]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
by_cases hd : d = 0
[GOAL]
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
rw [hd]
[GOAL]
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
[PROOFSTEP]
simp
[GOAL]
case neg
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
rw [mul_def' hx hd, mul_comm x, divInt_mul_right hx]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d
[PROOFSTEP]
rw [div_eq_mul_inv, inv_def', divInt_mul_divInt_cancel hx]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n
[PROOFSTEP]
rw [div_eq_mul_inv, inv_def', mul_comm, divInt_mul_divInt_cancel hx]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ ↑n / ↑d = n /. d
[PROOFSTEP]
repeat' rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ ↑n / ↑d = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / ↑d = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
[PROOFSTEP]
exact divInt_div_divInt_cancel_left one_ne_zero n d
[GOAL]
a b c r : ℚ
⊢ ↑r.num / ↑r.den = r
[PROOFSTEP]
rw [← Int.cast_ofNat]
[GOAL]
a b c r : ℚ
⊢ ↑r.num / ↑↑r.den = r
[PROOFSTEP]
erw [← divInt_eq_div, num_den]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ ↑q.num = q
[PROOFSTEP]
conv_rhs => rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ ↑q.num = q.num /. ↑1
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
n : ℕ
⊢ ↑n = ↑n /. 1
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n : ℕ
⊢ (↑n).num = ↑n
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_num]
[GOAL]
a b c : ℚ
n : ℕ
⊢ (↑n).den = 1
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_den]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ mkRat n d = ↑n / ↑d
[PROOFSTEP]
simp [mkRat]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
by_cases d = 0
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
by_cases d = 0
[GOAL]
case pos
a b c : ℚ
n : ℤ
d : ℕ
h : d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
simp [h]
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
simp [h, HDiv.hDiv, Rat.div, Div.div]
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d = ↑n * Rat.inv ↑d
[PROOFSTEP]
unfold Rat.inv
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
have h₁ : 0 < d := Nat.pos_iff_ne_zero.2 h
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
have h₂ : ¬(d : ℤ) < 0 := by simp
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ ¬↑d < 0
[PROOFSTEP]
simp
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
h₂ : ¬↑d < 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
simp [h, h₁, h₂, ← Rat.normalize_eq_mk', Rat.normalize_eq_mkRat, ← mkRat_one, Rat.mkRat_mul_mkRat]
