no goals
F : Type ?u.80415
α : Type u_1
β : Type u_2
γ : Type ?u.80424
δ : Type ?u.80427
G : Type ?u.80430
inst✝⁵ : FunLike F α fun x => β
inst✝⁴ : CommMonoid α
inst✝³ : CommMonoid β
inst✝² : CommMonoid γ
inst✝¹ : CommMonoid δ
inst✝ : CommGroup G
A : Set α
B : Set β
C : Set γ
n : ℕ
a b c d : α
f g : α →* β
h : toFreimanHom A n f = toFreimanHom A n g
⊢ f = g
rwa [toFreimanHom, toFreimanHom, FreimanHom.mk.injEq, FunLike.coe_fn_eq] at h