no goals
F : Type ?u.53167
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.53179
G : Type ?u.53182
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 : B →*[n] γ
f₁ f₂ : A →*[n] β
hg : Set.InjOn (↑g) B
hf₁ : Set.MapsTo (↑f₁) A B
hf₂ : Set.MapsTo (↑f₂) A B
⊢ Set.EqOn (↑(FreimanHom.comp g f₁ hf₁)) (↑(FreimanHom.comp g f₂ hf₂)) A ↔ Set.EqOn (↑f₁) (↑f₂) A
simp [hg.cancel_left hf₁ hf₂]