Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type)) (VExpr.instL ls (sort u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type))
    (VExpr.instL ls (VExpr.instL ls'✝ ci✝.type)) (VExpr.instL ls (sort u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (const c✝ ls✝)) (VExpr.instL ls (const c✝ ls'✝))
    (VExpr.instL ls (VExpr.instL ls✝ ci✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ⊢
Proof state after:
case constDF
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type) (sort (VLevel.inst ls u✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls'✝) ci✝.type) (sort (VLevel.inst ls u✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (const c✝ (List.map (VLevel.inst ls) ls✝))
    (const c✝ (List.map (VLevel.inst ls) ls'✝)) (VExpr.instL (List.map (VLevel.inst ls) ls✝) ci✝.type)