formPerm_apply_mem_of_mem — Mathlib

English

If x ∈ l, then formPerm(l) x ∈ l.

Русский

Если x ∈ l, то formPerm(l) x ∈ l.

LaTeX

$$$x \\in l \\Rightarrow formPerm(l) x \\in l$$$

Lean4

theorem formPerm_apply_mem_of_mem (h : x ∈ l) : formPerm l x ∈ l :=
  by
  rcases l with - | ⟨y, l⟩
  · simp at h
  induction l generalizing x y with
  | nil => simpa using h
  | cons z l IH =>
    by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]

Похожие утверждения