Theorem: List.id_map (Algdata/Data/List/Instances.lean)

State before:
α β : Type u
γ : Type w
as : List α
⊢ map id as = as
Tactic:
induction as with
| nil => rfl
| cons a as hi =>
  rw [map, hi]
  rfl
State after:
no goals

State before:
case nil
α β : Type u
γ : Type w
⊢ map id [] = []
Tactic:
rfl
State after:
no goals

State before:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ map id (a :: as) = a :: as
Tactic:
rw [map, hi]
State after:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ id a :: as = a :: as

State before:
case cons
α β : Type u
γ : Type w
a : α
as : List α
hi : map id as = as
⊢ id a :: as = a :: as
Tactic:
rfl
State after:
no goals