Theorem: Lean4Lean.VLevel.inst_congr (Lean4Lean/Theory/VLevel.lean)

State before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ inst ls l ≈ inst ls' l'
Tactic:
simp [equiv_def, eval_inst, ← equiv_def.1 h1]
State after:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ ∀ (ls_1 : List Nat), eval (List.map (eval ls_1) ls) l = eval (List.map (eval ls_1) ls') l

State before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
⊢ ∀ (ls_1 : List Nat), eval (List.map (eval ls_1) ls) l = eval (List.map (eval ls_1) ls') l
Tactic:
intro ns
State after:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ eval (List.map (eval ns) ls) l = eval (List.map (eval ns) ls') l

State before:
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ eval (List.map (eval ns) ls) l = eval (List.map (eval ns) ls') l
Tactic:
congr 1
State after:
case e_ls
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ List.map (eval ns) ls = List.map (eval ns) ls'

State before:
case e_ls
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
h2 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'
ns : List Nat
⊢ List.map (eval ns) ls = List.map (eval ns) ls'
Tactic:
induction h2 with
| nil => rfl
| cons h2 => simp [*, equiv_def.1 h2]
State after:
no goals

State before:
case e_ls.nil
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
ns : List Nat
⊢ List.map (eval ns) [] = List.map (eval ns) []
Tactic:
rfl
State after:
no goals

State before:
case e_ls.cons
l' : VLevel
ls ls' : List VLevel
l : VLevel
h1 : l ≈ l'
ns : List Nat
a✝¹ b✝ : VLevel
l₁✝ l₂✝ : List VLevel
h2 : a✝¹ ≈ b✝
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) l₁✝ l₂✝
a_ih✝ : List.map (eval ns) l₁✝ = List.map (eval ns) l₂✝
⊢ List.map (eval ns) (a✝¹ :: l₁✝) = List.map (eval ns) (b✝ :: l₂✝)
Tactic:
simp [*, equiv_def.1 h2]
State after:
no goals