-- Mathlib/Data/List/Sym.lean
theorem map_mk_sublist_sym2 (x : α) (xs : List α) (h : x ∈ xs) :
    map (fun y ↦ s(x, y)) xs <+ xs.sym2

Proof state:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ s(x, x') :: map (fun y => s(x, y)) xs <+ s(x', x') :: (map (fun y => s(x', y)) xs ++ xs.sym2)

Tactic:
cases h with
| head =>
  exact (sublist_append_left _ _).cons₂ _
| tail _ h =>
  refine .cons _ ?_
  rw [← singleton_append]
  refine .append ?_ (ih h)
  rw [singleton_sublist, mem_map]
  exact ⟨_, h, Sym2.eq_swap⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
x : α
h : x ∈ []
⊢ map (fun y => s(x, y)) [] <+ [].sym2

Tactic:
simp

Result:
no goals

Proof state:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] <+ map (fun y => s(x', y)) xs

Tactic:
rw [singleton_sublist, mem_map]

Result:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ ∃ a ∈ xs, s(x', a) = s(x, x')

Proof state:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] ++ map (fun y => s(x, y)) xs <+ map (fun y => s(x', y)) xs ++ xs.sym2

Tactic:
refine .append ?_ (ih h)

Result:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] <+ map (fun y => s(x', y)) xs

Proof state:
case cons.head
α : Type u_1
x : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
⊢ s(x, x) :: map (fun y => s(x, y)) xs <+ s(x, x) :: (map (fun y => s(x, y)) xs ++ xs.sym2)

Tactic:
exact (sublist_append_left _ _).cons₂ _

Result:
no goals

Proof state:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ ∃ a ∈ xs, s(x', a) = s(x, x')

Tactic:
exact ⟨_, h, Sym2.eq_swap⟩

Result:
no goals

Proof state:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y => s(x, y)) xs <+ map (fun y => s(x', y)) xs ++ xs.sym2

Tactic:
rw [← singleton_append]

Result:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ [s(x, x')] ++ map (fun y => s(x, y)) xs <+ map (fun y => s(x', y)) xs ++ xs.sym2

Proof state:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y => s(x, y)) xs <+ s(x', x') :: (map (fun y => s(x', y)) xs ++ xs.sym2)

Tactic:
refine .cons _ ?_

Result:
case cons.tail
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : Mem x xs
⊢ s(x, x') :: map (fun y => s(x, y)) xs <+ map (fun y => s(x', y)) xs ++ xs.sym2

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∈ xs
⊢ map (fun y => s(x, y)) xs <+ xs.sym2

Tactic:
induction xs with
| nil => simp
| cons x' xs ih =>
  simp only [map_cons, List.sym2, cons_append]
  cases h with
  | head =>
    exact (sublist_append_left _ _).cons₂ _
  | tail _ h =>
    refine .cons _ ?_
    rw [← singleton_append]
    refine .append ?_ (ih h)
    rw [singleton_sublist, mem_map]
    exact ⟨_, h, Sym2.eq_swap⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ map (fun y => s(x, y)) (x' :: xs) <+ (x' :: xs).sym2

Tactic:
simp only [map_cons, List.sym2, cons_append]

Result:
case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y => s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ s(x, x') :: map (fun y => s(x, y)) xs <+ s(x', x') :: (map (fun y => s(x', y)) xs ++ xs.sym2)