English
If f and g are cycles and they agree on the intersection of their supports, and this intersection is nonempty because some x ∈ f.support satisfies f x = g x, then f = g.
Русский
Если f и g — циклы и они согласны на пересечении поддержек, причём пересечение непусто (есть x ∈ f.поддержка, такое что f x = g x), то f = g.
LaTeX
$$$\\forall f,g:\\mathrm{Perm}(\\alpha),\\; \\mathrm{IsCycle}(f) \\land \\mathrm{IsCycle}(g) \\land \\big( \\forall x \\in f.\\mathrm{support} \\cap g.\\mathrm{support}, f x = g x \\big) \\land (\\exists x \\in f.\\mathrm{support}, f x = g x) \\Rightarrow f = g.$$$
Lean4
/-- If two cyclic permutations agree on all terms in their intersection,
and that intersection is not empty, then the two cyclic permutations must be equal. -/
theorem eq_on_support_inter_nonempty_congr (hf : IsCycle f) (hg : IsCycle g)
(h : ∀ x ∈ f.support ∩ g.support, f x = g x) (hx : f x = g x) (hx' : x ∈ f.support) : f = g :=
by
have hx'' : x ∈ g.support := by rwa [mem_support, ← hx, ← mem_support]
have : f.support ⊆ g.support := by
intro y hy
obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]
rw [inter_eq_left.mpr this] at h
exact hf.support_congr hg this h
