-- Mathlib/Data/List/Sym.lean
theorem sym_map {β : Type*} (f : α → β) (n : ℕ) (xs : List α) :
    (xs.map f).sym n = (xs.sym n).map (Sym.map f) :=
  match n, xs with
  | 0, _ => by simp only [List.sym]; rfl
  | n + 1, [] => by simp [List.sym]
  | n + 1, x :: xs => by
    rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]
    simp only [map_map, List.sym, map_append, append_cancel_right_eq]
    congr
    ext s
    simp only [Function.comp_apply, Sym.map_cons]

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ List.sym (n + 1) (map f (x :: xs)) = map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
rw [map_cons, List.sym, ← map_cons, sym_map f n (x :: xs), sym_map f (n + 1) xs]

Result:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p => f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ map (Sym.map f) (List.sym (n + 1) xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map ((fun p => f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)) =
    map (Sym.map f ∘ fun p => x ::ₛ p) (List.sym n (x :: xs))

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (fun p => f x ::ₛ p) ∘ Sym.map f = Sym.map f ∘ fun p => x ::ₛ p

Proof state:
case e_f
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ (fun p => f x ::ₛ p) ∘ Sym.map f = Sym.map f ∘ fun p => x ::ₛ p

Tactic:
ext s

Result:
case e_f.h.h
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
s : Sym α n
⊢ ↑(((fun p => f x ::ₛ p) ∘ Sym.map f) s) = ↑((Sym.map f ∘ fun p => x ::ₛ p) s)

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map (fun p => f x ::ₛ p) (map (Sym.map f) (List.sym n (x :: xs))) ++ map (Sym.map f) (List.sym (n + 1) xs) =
    map (Sym.map f) (List.sym (n + 1) (x :: xs))

Tactic:
simp only [map_map, List.sym, map_append, append_cancel_right_eq]

Result:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
⊢ map ((fun p => f x ::ₛ p) ∘ Sym.map f) (List.sym n (x :: xs)) =
    map (Sym.map f ∘ fun p => x ::ₛ p) (List.sym n (x :: xs))

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x✝ : List α
⊢ [Sym.nil] = map (Sym.map f) [Sym.nil]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x✝ : List α
⊢ List.sym 0 (map f x✝) = map (Sym.map f) (List.sym 0 x✝)

Tactic:
simp only [List.sym]

Result:
α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x✝ : List α
⊢ [Sym.nil] = map (Sym.map f) [Sym.nil]

Proof state:
case e_f.h.h
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
s : Sym α n
⊢ ↑(((fun p => f x ::ₛ p) ∘ Sym.map f) s) = ↑((Sym.map f ∘ fun p => x ::ₛ p) s)

Tactic:
simp only [Function.comp_apply, Sym.map_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
f : α → β
n✝ : ℕ
xs : List α
n : ℕ
⊢ List.sym (n + 1) (map f []) = map (Sym.map f) (List.sym (n + 1) [])

Tactic:
simp [List.sym]

Result:
no goals