English
If hg : t is injOn g, hf1 : s maps to t, hf2 : s maps to t, then equality on g ∘ f1 and g ∘ f2 on s is equivalent to equality on f1 and f2 on s.
Русский
Если hg: t инъOn g, hf1: s отображает в t, hf2: s отображает в t, тогда равенство функций g∘f1 и g∘f2 на s эквивалентно равенству f1 и f2 на s.
LaTeX
$$$ ( \\operatorname{InjOn} g t) \, (\\operatorname{MapsTo} f_1 s t) \, (\\operatorname{MapsTo} f_2 s t ) \\Rightarrow (s.EqOn (g \\circ f_1) (g \\circ f_2) \\iff s.EqOn f_1 f_2)$$$
Lean4
theorem cancel_left (h : s.EqOn (g ∘ f₁) (g ∘ f₂)) (hg : t.InjOn g) (hf₁ : s.MapsTo f₁ t) (hf₂ : s.MapsTo f₂ t) :
s.EqOn f₁ f₂ := fun _ ha => hg (hf₁ ha) (hf₂ ha) (h ha)
