Theorem: List.map_eq_self_iff (FOL/List.lean)

State before:
α : Type
f : α → α
xs : List α
⊢ map f xs = xs ↔ ∀ x ∈ xs, f x = x
Tactic:
induction xs
State after:
case nil
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x

case cons
α : Type
f : α → α
head✝ : α
tail✝ : List α
tail_ih✝ : map f tail✝ = tail✝ ↔ ∀ x ∈ tail✝, f x = x
⊢ map f (head✝ :: tail✝) = head✝ :: tail✝ ↔ ∀ x ∈ head✝ :: tail✝, f x = x

State before:
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x
Tactic:
case nil =>
  simp
State after:
no goals

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ map f (hd :: tl) = hd :: tl ↔ ∀ x ∈ hd :: tl, f x = x
Tactic:
case cons hd tl ih =>
  simp
  intro _
  exact ih
State after:
no goals

State before:
α : Type
f : α → α
⊢ map f [] = [] ↔ ∀ x ∈ [], f x = x
Tactic:
simp
State after:
no goals

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ map f (hd :: tl) = hd :: tl ↔ ∀ x ∈ hd :: tl, f x = x
Tactic:
simp
State after:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ f hd = hd → (map f tl = tl ↔ ∀ a ∈ tl, f a = a)

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
⊢ f hd = hd → (map f tl = tl ↔ ∀ a ∈ tl, f a = a)
Tactic:
intro _
State after:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
a✝ : f hd = hd
⊢ map f tl = tl ↔ ∀ a ∈ tl, f a = a

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : map f tl = tl ↔ ∀ x ∈ tl, f x = x
a✝ : f hd = hd
⊢ map f tl = tl ↔ ∀ a ∈ tl, f a = a
Tactic:
exact ih
State after:
no goals