F : Type ?u.56766
G : Type ?u.56769
α : Type u_1
M : Type ?u.56775
N : Type ?u.56778
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
F : Type ?u.56766
G : Type ?u.56769
α : Type u_1
M : Type ?u.56775
N : Type ?u.56778
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b
simp only [div_eq_mul_inv]
no goals
F : Type ?u.56766
G : Type ?u.56769
α : Type u_1
M : Type ?u.56775
N : Type ?u.56778
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
exact Units.mul_left_inj h.inv.unit'