internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls B✝)
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
    (VExpr.instL ls (sort v✝))
ih6 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝))
    (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝)) (sort (VLevel.inst ls v✝))
Tactic:
simpa using ih5
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls B✝)
ih4 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e'✝) (VExpr.instL ls e'✝) (VExpr.instL ls A✝)
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst B✝ e'✝)) (VExpr.instL ls (inst B✝ e'✝))
    (VExpr.instL ls (sort v✝))
ih6 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (inst e✝ e'✝)) (VExpr.instL ls (inst e✝ e'✝))
    (VExpr.instL ls (inst B✝ e'✝))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (inst (VExpr.instL ls e✝) (VExpr.instL ls e'✝))
    (inst (VExpr.instL ls e✝) (VExpr.instL ls e'✝)) (inst (VExpr.instL ls B✝) (VExpr.instL ls e'✝))
Tactic:
simpa using ih6
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
case eta
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls (lam A✝ (app (lift e✝) (VExpr.bvar 0))))
    (VExpr.instL ls e✝) (VExpr.instL ls (forallE A✝ B✝))
Tactic:
simpa [VExpr.instL] using .eta (.inst hls) (.inst hls) ih1 ih2
  (by simpa using ih3) ih4 (by simpa [VExpr.instL] using ih5)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (lift (VExpr.instL ls A✝) :: VExpr.instL ls A✝ :: List.map (VExpr.instL ls) Γ✝)
    (liftN 1 (VExpr.instL ls B✝) 1) (liftN 1 (VExpr.instL ls B✝) 1) (sort (VLevel.inst ls v✝))
Tactic:
simpa using ih3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls A✝) (VExpr.instL ls A✝) (VExpr.instL ls (sort u✝))
ih2 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls B✝) (VExpr.instL ls B✝)
    (VExpr.instL ls (sort v✝))
ih3 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (lift A✝ :: A✝ :: Γ✝)) (VExpr.instL ls (liftN 1 B✝ 1))
    (VExpr.instL ls (liftN 1 B✝ 1)) (VExpr.instL ls (sort v✝))
ih4 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls e✝) (VExpr.instL ls e✝)
    (VExpr.instL ls (forallE A✝ B✝))
ih5 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) (A✝ :: Γ✝)) (VExpr.instL ls (lift e✝)) (VExpr.instL ls (lift e✝))
    (VExpr.instL ls (forallE (lift A✝) (liftN 1 B✝ 1)))
⊢ IsDefEqStrong env U' (VExpr.instL ls A✝ :: List.map (VExpr.instL ls) Γ✝) (lift (VExpr.instL ls e✝))
    (lift (VExpr.instL ls e✝)) (forallE (lift (VExpr.instL ls A✝)) (liftN 1 (VExpr.instL ls B✝) 1))
Tactic:
simpa [VExpr.instL] using ih5
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
case proofIrrel
U' : Nat
env : VEnv
ls : List VLevel
hls : ∀ (l : VLevel), l ∈ ls → VLevel.WF U' l
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 :
  IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls p✝) (VExpr.instL ls p✝)
    (VExpr.instL ls (sort VLevel.zero))
ih2 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h✝) (VExpr.instL ls p✝)
ih3 : IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h'✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
⊢ IsDefEqStrong env U' (List.map (VExpr.instL ls) Γ✝) (VExpr.instL ls h✝) (VExpr.instL ls h'✝) (VExpr.instL ls p✝)
Tactic:
exact .proofIrrel ih1 ih2 ih3
Proof state after:
no goals
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' [] (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)
Tactic:
exact .extra h1 (by simp [h2, VLevel.WF.inst hls]) (by simp [h3])
  (.inst hls) ih1 ih2 ih3 ih4 ih5
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
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)
⊢ ∀ (l : VLevel), l ∈ List.map (VLevel.inst ls) ls✝ → VLevel.WF U' l
Tactic:
simp [h2, VLevel.WF.inst hls]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instL
Proof state before:
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)
⊢ List.length (List.map (VLevel.inst ls) ls✝) = df✝.uvars
Tactic:
simp [h3]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst (VExpr.bvar i) e₀ k) (inst (VExpr.bvar i) e₀ k) (inst ty e₀ k)
Tactic:
dsimp [inst]
Proof state after:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
h2 : IsDefEqStrong env U Γ✝ ty ty (sort u✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst ty e₀ k) (inst ty e₀ k) (inst (sort u✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Tactic:
clear h2 ih
Proof state after:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i : Nat
ty : VExpr
u✝ : VLevel
h : Lookup Γ✝ i ty
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (instVar i e₀ k) (instVar i e₀ k) (inst ty e₀ k)
Tactic:
induction W generalizing i ty with
| zero =>
  cases h with simp [inst_lift]
  | zero => exact h₀
  | succ h =>
    let ⟨u, hty⟩ := hΓ₀.lookup henv h
    exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
| succ _ ih =>
  cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
  | zero =>
    let ⟨u, hty⟩ := hΓ.lookup henv .zero
    exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
  | succ h => exact (ih h hΓ.1).weakN henv .one
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
i : Nat
ty : VExpr
h : Lookup (A₀ :: Γ₀) i ty
hΓ : CtxStrong env U Γ₀
⊢ IsDefEqStrong env U Γ₀ (instVar i e₀) (instVar i e₀) (inst ty e₀)
Tactic:
cases h with simp [inst_lift]
| zero => exact h₀
| succ h =>
  let ⟨u, hty⟩ := hΓ₀.lookup henv h
  exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.zero.zero
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
⊢ IsDefEqStrong env U Γ₀ e₀ e₀ A₀
Tactic:
exact h₀
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Tactic:
let ⟨u, hty⟩ := hΓ₀.lookup henv h
Proof state after:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
u : VLevel
hty : IsDefEqStrong env U Γ₀ ty✝ ty✝ (sort u)
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.zero.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
a✝ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
hΓ : CtxStrong env U Γ₀
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ₀ n✝ ty✝
u : VLevel
hty : IsDefEqStrong env U Γ₀ ty✝ ty✝ (sort u)
⊢ IsDefEqStrong env U Γ₀ (VExpr.bvar n✝) (VExpr.bvar n✝) ty✝
Tactic:
exact .bvar h (hty.defeq.sort_r henv hΓ₀.defeq) hty
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
i : Nat
ty : VExpr
h : Lookup (A✝ :: Γ✝) i ty
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar i e₀ (k✝ + 1)) (instVar i e₀ (k✝ + 1)) (inst ty e₀ (k✝ + 1))
Tactic:
cases h with (simp; rw [Nat.add_comm, ← liftN_instN_lo (hj := Nat.zero_le _)])
| zero =>
  let ⟨u, hty⟩ := hΓ.lookup henv .zero
  exact .bvar .zero (hty.defeq.sort_r henv hΓ.defeq) hty
| succ h => exact (ih h hΓ.1).weakN henv .one
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (instVar (n✝ + 1) e₀ (k✝ + 1)) (instVar (n✝ + 1) e₀ (k✝ + 1))
    (inst (lift ty✝) e₀ (k✝ + 1))
Tactic:
simp
Proof state after:
case bvar.succ.succ
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
u✝ : VLevel
a✝¹ : VLevel.WF U u✝
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ e₀ A₀ k✝ Γ✝ Γ'✝
ih :
  ∀ {i : Nat} {ty : VExpr},
    Lookup Γ✝ i ty → CtxStrong env U Γ'✝ → IsDefEqStrong env U Γ'✝ (instVar i e₀ k✝) (instVar i e₀ k✝) (inst ty e₀ k✝)
hΓ : CtxStrong env U (inst A✝ e₀ k✝ :: Γ'✝)
n✝ : Nat
ty✝ : VExpr
h : Lookup Γ✝ n✝ ty✝
⊢ IsDefEqStrong env U (inst A✝ e₀ k✝ :: Γ'✝) (lift (instVar n✝ e₀ k✝)) (lift (instVar n✝ e₀ k✝))
    (inst (lift ty✝) e₀ (k✝ + 1))