α : Type u_1
β : Type ?u.307911
γ : Type ?u.307914
δ : Type ?u.307917
inst✝ : CommMonoid α
a b : α
x✝ : a ∣ b
c : α
hc : b = a * c
⊢ Associates.mk (a * c) = Associates.mk a * Associates.mk c
α : Type u_1
β : Type ?u.307911
γ : Type ?u.307914
δ : Type ?u.307917
inst✝ : CommMonoid α
a b : α
x✝ : a ∣ b
c : α
hc : b = a * c
⊢ Associates.mk b = Associates.mk a * Associates.mk c
simp [hc]
no goals
α : Type u_1
β : Type ?u.307911
γ : Type ?u.307914
δ : Type ?u.307917
inst✝ : CommMonoid α
a b : α
x✝ : a ∣ b
c : α
hc : b = a * c
⊢ Associates.mk (a * c) = Associates.mk a * Associates.mk c
rfl