no goals
α : Type u_1
β : Type ?u.17471
K : Type ?u.17474
inst✝ : DivisionSemiring α
a b c d : α
hab : _root_.Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]