Theorem: List.map_id'' (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
f : α → α
l : List α
h : ∀ (x : α), x ∈ l → f x = x
⊢ map f l = l
Tactic:
induction l <;> simp_all
State after:
no goals