no goals
α : Type ?u.42728
β : Type ?u.42731
K : Type u_1
inst✝ : DivisionRing K
a b c d : K
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
rw [mul_sub_left_distrib (1 / a), one_div_mul_cancel ha, mul_sub_right_distrib, one_mul,
  mul_assoc, mul_one_div_cancel hb, mul_one]