English
Assuming IsPretransitive, for any a and any embedding x: Fin n.succ → α there exist g ∈ G and y: Fin n ↪ ofStabilizer G a such that g • x = ofStabilizer.snoc y.
Русский
При предположении IsPretransitive для любого a и отображения x: Fin n.succ → α существуют g ∈ G и y: Fin n ↪ ofStabilizer G a такие, что g • x = ofStabilizer.snoc y.
LaTeX
$$$\\exists g:\\,G\\;\\exists y:\\,Fin\\,n\\hookrightarrow\\mathrm{ofStabilizer}(G,a),\\ g \\cdot x = \\mathrm{ofStabilizer.snoc}(y).$$$
Lean4
@[to_additive]
theorem exists_smul_of_last_eq [IsPretransitive G α] {n : ℕ} (a : α) (x : Fin n.succ ↪ α) :
∃ (g : G) (y : Fin n ↪ ofStabilizer G a), g • x = ofStabilizer.snoc y :=
by
obtain ⟨g, hgx⟩ := exists_smul_eq G (x (Fin.last n)) a
have H : ∀ i, Fin.Embedding.init (g • x) i ∈ ofStabilizer G a := fun i ↦
by
simp only [mem_ofStabilizer_iff, Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]
suffices Fin.Embedding.init (g • x) i = (g • x) i.castSucc by simp [this]
simp [Fin.Embedding.init, Fin.init_def]
use g, (Fin.Embedding.init (g • x)).codRestrict (ofStabilizer G a) H
ext i
rcases Fin.eq_castSucc_or_eq_last i with ⟨i, rfl⟩ | ⟨rfl⟩
· simpa [ofStabilizer.snoc] using Subtype.eq_iff.mp <| Function.Embedding.codRestrict_apply _ _ H i
· simpa only [smul_apply, ofStabilizer.snoc, Fin.Embedding.snoc_last]
