no goals
F : Type ?u.92699
α : Type u_1
β : Type u_2
γ : Type ?u.92708
δ : Type ?u.92711
G : Type ?u.92714
inst✝² : FunLike F α fun x => β
inst✝¹ : CommMonoid α
inst✝ : CancelCommMonoid β
A : Set α
m n : ℕ
h : m ≤ n
f g : A →*[n] β
hfg : toFreimanHom h f = toFreimanHom h g
⊢ ∀ (x : α), ↑f x = ↑g x
convert FunLike.ext_iff.1 hfg using 0