Lean4
theorem isRat_mul {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} :
f = HMul.hMul →
IsRat a na da →
IsRat b nb db → Int.mul na nb = 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 * nb = k * nc) (h₂ : da * db = k * dc)
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
have := invertibleOfMul' (α := α) h₂
refine ⟨this, ?_⟩
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
have h₁ := congr_arg (Int.cast (R := α)) h₁
simp only [Int.cast_mul, Int.cast_natCast] at h₁
simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
simp only [Nat.cast_mul, ← mul_assoc] at h₂; rw [H] at h₂
simp only [mul_invOf_cancel_right'] at h₂; rw [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]
