no goals
α : Type u_1
β : Type ?u.4001
K : Type ?u.4004
inst✝ : DivisionSemiring α
a b c d : α
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
rw [mul_add, one_div_mul_cancel ha, add_mul, one_mul, mul_assoc, mul_one_div_cancel hb, mul_one,
  add_comm]