α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b
rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
no goals
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a = b
⊢ a = b
exact hc
no goals
α✝ : Type u
β : Type v
inst✝² : Monoid α✝
inst✝¹ : Monoid β
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b
rw [h]