internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case appDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U f✝ ∧ LevelWF U f'✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U a✝² ∧ LevelWF U a'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hf : LevelWF U f✝
hf' : LevelWF U f'✝
left✝ : LevelWF U A✝
hB : LevelWF U B✝
ha : LevelWF U a✝²
ha' : LevelWF U a'✝
right✝ : LevelWF U A✝
⊢ LevelWF U (app f✝ a✝²) ∧ LevelWF U (app f'✝ a'✝) ∧ LevelWF U (inst B✝ a✝²)
Tactic:
exact ⟨⟨hf, ha⟩, ⟨hf', ha'⟩, hB.inst ha⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case lamDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U B✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (lam A✝ body✝) ∧ LevelWF U (lam A'✝ body'✝) ∧ LevelWF U (VExpr.forallE A✝ B✝)
Tactic:
let ⟨hA, hA', _⟩ := ih1 W
Proof state after:
case lamDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U B✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
right✝ : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U (lam A✝ body✝) ∧ LevelWF U (lam A'✝ body'✝) ∧ LevelWF U (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case lamDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U B✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
right✝ : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U (lam A✝ body✝) ∧ LevelWF U (lam A'✝ body'✝) ∧ LevelWF U (VExpr.forallE A✝ B✝)
Tactic:
let ⟨hb, hb', hB⟩ := ih2 ⟨W, hA⟩
Proof state after:
case lamDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U B✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
right✝ : LevelWF U (VExpr.sort u✝)
hb : LevelWF U body✝
hb' : LevelWF U body'✝
hB : LevelWF U B✝
⊢ LevelWF U (lam A✝ body✝) ∧ LevelWF U (lam A'✝ body'✝) ∧ LevelWF U (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case lamDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U B✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
right✝ : LevelWF U (VExpr.sort u✝)
hb : LevelWF U body✝
hb' : LevelWF U body'✝
hB : LevelWF U B✝
⊢ LevelWF U (lam A✝ body✝) ∧ LevelWF U (lam A'✝ body'✝) ∧ LevelWF U (VExpr.forallE A✝ B✝)
Tactic:
exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hA, hB⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case forallEDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U (VExpr.sort v✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (VExpr.forallE A✝ body✝) ∧ LevelWF U (VExpr.forallE A'✝ body'✝) ∧ LevelWF U (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
let ⟨hA, hA', hu⟩ := ih1 W
Proof state after:
case forallEDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U (VExpr.sort v✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
hu : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U (VExpr.forallE A✝ body✝) ∧ LevelWF U (VExpr.forallE A'✝ body'✝) ∧ LevelWF U (VExpr.sort (VLevel.imax u✝ v✝))
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case forallEDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U (VExpr.sort v✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
hu : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U (VExpr.forallE A✝ body✝) ∧ LevelWF U (VExpr.forallE A'✝ body'✝) ∧ LevelWF U (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
let ⟨hb, hb', hv⟩ := ih2 ⟨W, hA⟩
Proof state after:
case forallEDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U (VExpr.sort v✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
hu : LevelWF U (VExpr.sort u✝)
hb : LevelWF U body✝
hb' : LevelWF U body'✝
hv : LevelWF U (VExpr.sort v✝)
⊢ LevelWF U (VExpr.forallE A✝ body✝) ∧ LevelWF U (VExpr.forallE A'✝ body'✝) ∧ LevelWF U (VExpr.sort (VLevel.imax u✝ v✝))
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case forallEDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U A'✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U body✝ ∧ LevelWF U body'✝ ∧ LevelWF U (VExpr.sort v✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
hA : LevelWF U A✝
hA' : LevelWF U A'✝
hu : LevelWF U (VExpr.sort u✝)
hb : LevelWF U body✝
hb' : LevelWF U body'✝
hv : LevelWF U (VExpr.sort v✝)
⊢ LevelWF U (VExpr.forallE A✝ body✝) ∧ LevelWF U (VExpr.forallE A'✝ body'✝) ∧ LevelWF U (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hu, hv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case defeqDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U B✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U B✝
Tactic:
let ⟨_, hB, _⟩ := ih1 W
Proof state after:
case defeqDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U B✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
left✝ : LevelWF U A✝
hB : LevelWF U B✝
right✝ : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U B✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case defeqDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U B✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
left✝ : LevelWF U A✝
hB : LevelWF U B✝
right✝ : LevelWF U (VExpr.sort u✝)
⊢ LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U B✝
Tactic:
let ⟨he1, he2, _⟩ := ih2 W
Proof state after:
case defeqDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U B✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
left✝ : LevelWF U A✝
hB : LevelWF U B✝
right✝¹ : LevelWF U (VExpr.sort u✝)
he1 : LevelWF U e1✝
he2 : LevelWF U e2✝
right✝ : LevelWF U A✝
⊢ LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U B✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case defeqDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U A✝ ∧ LevelWF U B✝ ∧ LevelWF U (VExpr.sort u✝)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
left✝ : LevelWF U A✝
hB : LevelWF U B✝
right✝¹ : LevelWF U (VExpr.sort u✝)
he1 : LevelWF U e1✝
he2 : LevelWF U e2✝
right✝ : LevelWF U A✝
⊢ LevelWF U e1✝ ∧ LevelWF U e2✝ ∧ LevelWF U B✝
Tactic:
exact ⟨he1, he2, hB⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case beta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U B✝
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e'✝ ∧ LevelWF U e'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (app (lam A✝ e✝) e'✝) ∧ LevelWF U (inst e✝ e'✝) ∧ LevelWF U (inst B✝ e'✝)
Tactic:
let ⟨he', _, hA⟩ := ih2 W
Proof state after:
case beta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U B✝
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e'✝ ∧ LevelWF U e'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
he' left✝ : LevelWF U e'✝
hA : LevelWF U A✝
⊢ LevelWF U (app (lam A✝ e✝) e'✝) ∧ LevelWF U (inst e✝ e'✝) ∧ LevelWF U (inst B✝ e'✝)
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case beta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U B✝
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e'✝ ∧ LevelWF U e'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
he' left✝ : LevelWF U e'✝
hA : LevelWF U A✝
⊢ LevelWF U (app (lam A✝ e✝) e'✝) ∧ LevelWF U (inst e✝ e'✝) ∧ LevelWF U (inst B✝ e'✝)
Tactic:
let ⟨he, _, hB⟩ := ih1 ⟨W, hA⟩
Proof state after:
case beta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U B✝
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e'✝ ∧ LevelWF U e'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
he' left✝¹ : LevelWF U e'✝
hA : LevelWF U A✝
he left✝ : LevelWF U e✝
hB : LevelWF U B✝
⊢ LevelWF U (app (lam A✝ e✝) e'✝) ∧ LevelWF U (inst e✝ e'✝) ∧ LevelWF U (inst B✝ e'✝)
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case beta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : (OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U B✝
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e'✝ ∧ LevelWF U e'✝ ∧ LevelWF U A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
he' left✝¹ : LevelWF U e'✝
hA : LevelWF U A✝
he left✝ : LevelWF U e✝
hB : LevelWF U B✝
⊢ LevelWF U (app (lam A✝ e✝) e'✝) ∧ LevelWF U (inst e✝ e'✝) ∧ LevelWF U (inst B✝ e'✝)
Tactic:
exact ⟨⟨⟨hA, he⟩, he'⟩, he.inst he', hB.inst he'⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case eta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (lam A✝ (app (lift e✝) (VExpr.bvar 0))) ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
Tactic:
let ⟨he, _, hA, hB⟩ := ih W
Proof state after:
case eta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
he left✝ : LevelWF U e✝
hA : LevelWF U A✝
hB : LevelWF U B✝
⊢ LevelWF U (lam A✝ (app (lift e✝) (VExpr.bvar 0))) ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case eta
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e✝ ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
W : OnCtx Γ✝ fun x A => LevelWF U A
he left✝ : LevelWF U e✝
hA : LevelWF U A✝
hB : LevelWF U B✝
⊢ LevelWF U (lam A✝ (app (lift e✝) (VExpr.bvar 0))) ∧ LevelWF U e✝ ∧ LevelWF U (VExpr.forallE A✝ B✝)
Tactic:
exact ⟨⟨hA, he.liftN, ⟨⟩⟩, he, hA, hB⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case proofIrrel
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U p✝ ∧ LevelWF U p✝ ∧ LevelWF U (VExpr.sort VLevel.zero)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h✝ ∧ LevelWF U h✝ ∧ LevelWF U p✝
ih3 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h'✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U h✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
Tactic:
let ⟨hh, _, hp⟩ := ih2 W
Proof state after:
case proofIrrel
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U p✝ ∧ LevelWF U p✝ ∧ LevelWF U (VExpr.sort VLevel.zero)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h✝ ∧ LevelWF U h✝ ∧ LevelWF U p✝
ih3 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h'✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hh left✝ : LevelWF U h✝
hp : LevelWF U p✝
⊢ LevelWF U h✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case proofIrrel
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U p✝ ∧ LevelWF U p✝ ∧ LevelWF U (VExpr.sort VLevel.zero)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h✝ ∧ LevelWF U h✝ ∧ LevelWF U p✝
ih3 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h'✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hh left✝ : LevelWF U h✝
hp : LevelWF U p✝
⊢ LevelWF U h✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
Tactic:
let ⟨hh', _, _⟩ := ih3 W
Proof state after:
case proofIrrel
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U p✝ ∧ LevelWF U p✝ ∧ LevelWF U (VExpr.sort VLevel.zero)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h✝ ∧ LevelWF U h✝ ∧ LevelWF U p✝
ih3 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h'✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hh left✝¹ : LevelWF U h✝
hp : LevelWF U p✝
hh' left✝ : LevelWF U h'✝
right✝ : LevelWF U p✝
⊢ LevelWF U h✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case proofIrrel
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U p✝ ∧ LevelWF U p✝ ∧ LevelWF U (VExpr.sort VLevel.zero)
ih2 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h✝ ∧ LevelWF U h✝ ∧ LevelWF U p✝
ih3 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U h'✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
W : OnCtx Γ✝ fun x A => LevelWF U A
hh left✝¹ : LevelWF U h✝
hp : LevelWF U p✝
hh' left✝ : LevelWF U h'✝
right✝ : LevelWF U p✝
⊢ LevelWF U h✝ ∧ LevelWF U h'✝ ∧ LevelWF U p✝
Tactic:
exact ⟨hh, hh', hp⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case extra
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
a✝¹ : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (instL ls✝ df✝.lhs) ∧ LevelWF U (instL ls✝ df✝.rhs) ∧ LevelWF U (instL ls✝ df✝.type)
Tactic:
exact ⟨.instL h2, .instL h2, .instL h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
env : VEnv
henv : Ordered env
n k : Nat
Γ Γ' : List VExpr
U : Nat
e1 e2 A : VExpr
W : Ctx.LiftN n k Γ Γ'
H : IsDefEq env U Γ e1 e2 A
⊢ IsDefEq env U Γ' (liftN n e1 k) (liftN n e2 k) (liftN n A k)
Tactic:
induction H generalizing k Γ' with
| bvar h => refine .bvar (h.weakN W)
| symm _ ih => exact .symm (ih W)
| trans _ _ ih1 ih2 => exact .trans (ih1 W) (ih2 W)
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| constDF h1 h2 h3 h4 h5 =>
  rw [(henv.closedC h1).instL.liftN_eq (Nat.zero_le _)]
  exact .constDF h1 h2 h3 h4 h5
| appDF _ _ ih1 ih2 => exact liftN_inst_hi .. ▸ .appDF (ih1 W) (ih2 W)
| lamDF _ _ ih1 ih2 => exact .lamDF (ih1 W) (ih2 W.succ)
| forallEDF _ _ ih1 ih2 => exact .forallEDF (ih1 W) (ih2 W.succ)
| defeqDF _ _ ih1 ih2 => exact .defeqDF (ih1 W) (ih2 W)
| beta _ _ ih1 ih2 =>
  exact VExpr.liftN_inst_hi .. ▸ VExpr.liftN_instN_hi .. ▸ .beta (ih1 W.succ) (ih2 W)
| eta _ ih =>
  have := IsDefEq.eta (ih W)
  simp [liftN]; rwa [← lift_liftN']
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel (ih1 W) (ih2 W) (ih3 W)
| extra h1 h2 h3 =>
  have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
  rw [
    hA1.instL.liftN_eq (Nat.zero_le _),
    hA2.instL.liftN_eq (Nat.zero_le _),
    hA3.instL.liftN_eq (Nat.zero_le _)]
  exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case bvar
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.bvar i✝) k) (liftN n (VExpr.bvar i✝) k) (liftN n A✝ k)
Tactic:
refine .bvar (h.weakN W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case symm
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e✝ k) (liftN n e'✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n e'✝ k) (liftN n e✝ k) (liftN n A✝ k)
Tactic:
exact .symm (ih W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case trans
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e₁✝ k) (liftN n e₂✝ k) (liftN n A✝ k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → IsDefEq env U Γ' (liftN n e₂✝ k) (liftN n e₃✝ k) (liftN n A✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n e₁✝ k) (liftN n e₃✝ k) (liftN n A✝ k)
Tactic:
exact .trans (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case sortDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.sort l✝) k) (liftN n (VExpr.sort l'✝) k) (liftN n (VExpr.sort (VLevel.succ l✝)) k)
Tactic:
exact .sortDF h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.weakN
Proof state before:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List 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'✝
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.const c✝ ls✝) k) (liftN n (VExpr.const c✝ ls'✝) k) (liftN n (instL ls✝ ci✝.type) k)
Tactic:
rw [(henv.closedC h1).instL.liftN_eq (Nat.zero_le _)]
Proof state after:
case constDF
env : VEnv
henv : Ordered env
n : Nat
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List 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'✝
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ IsDefEq env U Γ' (liftN n (VExpr.const c✝ ls✝) k) (liftN n (VExpr.const c✝ ls'✝) k) (instL ls✝ ci✝.type)