Lean4
theorem isNNRat_add {α} [Semiring α] {f : α → α → α} {a b : α} {na nb nc : ℕ} {da db dc k : ℕ} :
f = HAdd.hAdd →
IsNNRat a na da →
IsNNRat b nb db →
Nat.add (Nat.mul na db) (Nat.mul nb da) = Nat.mul k nc →
Nat.mul da db = Nat.mul k dc → IsNNRat (f a b) nc dc :=
by
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
have := invertibleOfMul' (α := α) h₂
use this
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
simp only [Nat.cast_add, Nat.cast_mul, ← mul_assoc, add_mul, mul_invOf_cancel_right] at h₁
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
simp only [H, mul_invOf_cancel_right', Nat.cast_mul, ← mul_assoc] at h₁ h₂
rw [h₁, h₂, Nat.cast_commute]
simp only [mul_invOf_cancel_right, (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
(Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
-- TODO: clean up and move it somewhere in mathlib? It's a bit much for this file
-- see note [norm_num lemma function equality]
