Lean4
theorem isRat_add {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} :
f = HAdd.hAdd →
IsRat a na da →
IsRat b nb db →
Int.add (Int.mul na db) (Int.mul nb da) = Int.mul k nc → Nat.mul da db = Nat.mul k dc → IsRat (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 [Int.cast_add, Int.cast_mul, Int.cast_natCast, ← 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]
