no goals
F : Type ?u.67029
G : Type ?u.67032
α : Type u_1
M : Type ?u.67038
N : Type ?u.67041
inst✝ : DivisionCommMonoid α
a b c d : α
h : IsUnit a
⊢ a / b / a = b⁻¹
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]