Theorem: Lean4Lean.VExpr.LevelWF.instL_id (Lean4Lean/Theory/VExpr.lean)

State before:
U : Nat
e : VExpr
h : LevelWF U e
⊢ instL (List.map VLevel.param (List.range U)) e = e
Tactic:
induction e <;> simp_all [instL, LevelWF, VLevel.inst_id]
State after:
case const
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝

State before:
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝
Tactic:
case const => exact List.map_id'' _ fun _ h1 => VLevel.inst_id (h _ h1)
State after:
no goals

State before:
U : Nat
declName✝ : Name
us✝ : List VLevel
h : ∀ (l : VLevel), l ∈ us✝ → VLevel.WF U l
⊢ List.map (VLevel.inst (List.map VLevel.param (List.range U))) us✝ = us✝
Tactic:
exact List.map_id'' _ fun _ h1 => VLevel.inst_id (h _ h1)
State after:
no goals