α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : ↑f x✝ = ↑g x✝
a✝ : ↑f y✝ = ↑g y✝
⊢ ↑f (x✝ * y✝) = ↑g (x✝ * y✝)
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x : FreeMagma α
⊢ ∀ (x y : FreeMagma α), ↑f x = ↑g x → ↑f y = ↑g y → ↑f (x * y) = ↑g (x * y)
intros
no goals
α : Type u
β : Type v
inst✝ : Mul β
f g : FreeMagma α →ₙ* β
h : ↑f ∘ of = ↑g ∘ of
x x✝ y✝ : FreeMagma α
a✝¹ : ↑f x✝ = ↑g x✝
a✝ : ↑f y✝ = ↑g y✝
⊢ ↑f (x✝ * y✝) = ↑g (x✝ * y✝)
simp only [map_mul, *]