no goals
F : Type ?u.51726
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.51738
G : Type ?u.51741
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 : α
g₁ g₂ : B →*[n] γ
f : A →*[n] β
hf : Set.SurjOn (↑f) A B
hf' : Set.MapsTo (↑f) A B
⊢ Set.EqOn (↑(FreimanHom.comp g₁ f hf')) (↑(FreimanHom.comp g₂ f hf')) A ↔ Set.EqOn (↑g₁) (↑g₂) B
simp [hf.cancel_right hf']