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

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

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

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

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

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

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1 : f hd = hd ∧ ∀ a ∈ tl, f a = a
⊢ map f (hd :: tl) = hd :: tl
Tactic:
cases h1
State after:
case intro
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
left✝ : f hd = hd
right✝ : ∀ a ∈ tl, f a = a
⊢ map f (hd :: tl) = hd :: tl

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

State before:
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ f hd = hd ∧ map f tl = tl
Tactic:
constructor
State after:
case left
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ f hd = hd

case right
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ map f tl = tl

State before:
case left
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ f hd = hd
Tactic:
exact h1_left
State after:
no goals

State before:
case right
α : Type
f : α → α
hd : α
tl : List α
ih : (∀ x ∈ tl, f x = x) → map f tl = tl
h1_left : f hd = hd
h1_right : ∀ a ∈ tl, f a = a
⊢ map f tl = tl
Tactic:
exact ih h1_right
State after:
no goals