α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h✝ : c * a = b
h : a * c = b
⊢ a * ?m.8324 c h✝ = b
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h : c * a = b
⊢ a * ?m.8324 c h = b
rw [mul_comm] at h
no goals
α : Type u_1
inst✝ : CommSemigroup α
a b c✝ c : α
h✝ : c * a = b
h : a * c = b
⊢ a * ?m.8324 c h✝ = b
apply h