no goals
F : Type ?u.21144
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
rw [← comp_apply, h, comp_apply]