no goals
α : Type u_1
β : Type ?u.285626
γ : Type ?u.285629
δ : Type ?u.285632
inst✝ : CommMonoid α
x y : Associates α
a b : α
h : Quotient.mk (Associated.setoid α) a * Quotient.mk (Associated.setoid α) b = 1
this : a * b ~ᵤ 1
⊢ b * ?m.287732 a b h this ~ᵤ 1
rwa [mul_comm] at this
no goals
α : Type u_1
β : Type ?u.285626
γ : Type ?u.285629
δ : Type ?u.285632
inst✝ : CommMonoid α
x y : Associates α
⊢ x = 1 ∧ y = 1 → x * y = 1
simp (config := { contextual := true })