α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (a + -b) nc dc
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (f a b) nc dc
rw [hf, sub_eq_add_neg]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (Int.mul (-nb) ↑da) = Int.mul (↑k) nc
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (a + -b) nc dc
refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (-(nb * ↑da)) = Int.mul (↑k) nc
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (Int.mul (-nb) ↑da) = Int.mul (↑k) nc
rw [show Int.mul (-nb) _ = _ from neg_mul ..]
no goals
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (-(nb * ↑da)) = Int.mul (↑k) nc
exact h₁