Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.type)) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) []) (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (VExpr.instL ls✝ df✝.lhs))
    (VExpr.instL ls (VExpr.instL ls✝ df✝.rhs)) (VExpr.instL ls (VExpr.instL ls✝ df✝.type))
Tactic:
simp [VExpr.instL, VExpr.instL_instL] at ih1 ih2 ih3 ih4 ih5 ⊢
Proof state after:
case extra
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
ih1 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type) (sort (VLevel.inst ls u✝))
ih2 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih3 :
  IsDefEqStrong env U' [] (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.lhs)
    (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.rhs) (VExpr.instL (List.map (VLevel.inst ls) ls✝) df✝.type)