internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.mono
Proof state before:
case proofIrrel
env env' : VEnv
henv : env ≤ env'
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✝
ih1 : IsDefEq env' U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
ih2 : IsDefEq env' U Γ✝ h✝ h✝ p✝
ih3 : IsDefEq env' U Γ✝ h'✝ h'✝ p✝
⊢ IsDefEq env' U Γ✝ h✝ h'✝ p✝
Tactic:
exact .proofIrrel ih1 ih2 ih3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.mono
Proof state before:
case extra
env env' : VEnv
henv : env ≤ env'
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
⊢ IsDefEq env' U Γ✝ (instL ls✝ df✝.lhs) (instL ls✝ df✝.rhs) (instL ls✝ df✝.type)
Tactic:
exact .extra (henv.2 _ h1) h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case empty
env : VEnv
n : Name
ci : VConstant
h : ∅.constants n = some (some ci)
⊢ VConstant.WF ∅ ci
Tactic:
cases h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env'✝ ci
Tactic:
refine .mono (addConst_le h3) ?_
Proof state after:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
unfold addConst at h3
Proof state after:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
split at h3 <;> cases h3
Proof state after:
case const.h_2.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h :
  { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n =
    some (some ci)
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const.h_2.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h :
  { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n =
    some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
simp at h
Proof state after:
case const.h_2.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h : (if n✝ = n then some oci✝ else env✝.constants n) = some (some ci)
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const.h_2.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h : (if n✝ = n then some oci✝ else env✝.constants n) = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
split at h
Proof state after:
case const.h_2.refl.inl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h : some oci✝ = some (some ci)
⊢ VConstant.WF env✝ ci

case const.h_2.refl.inr
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : ¬n✝ = n
h : env✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const.h_2.refl.inl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h : some oci✝ = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
cases h
Proof state after:
case const.h_2.refl.inl.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
n✝ : Name
a✝ : Ordered env✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h2 : ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env✝ ci_1
⊢ VConstant.WF env✝ ci
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const.h_2.refl.inl.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
n✝ : Name
a✝ : Ordered env✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h2 : ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env✝ ci_1
⊢ VConstant.WF env✝ ci
Tactic:
exact h2 _ rfl
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case const.h_2.refl.inr
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : ¬n✝ = n
h : env✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
exact ih h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.constWF
Proof state before:
case defeq
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : (addDefEq env✝ df✝).constants n = some (some ci)
⊢ VConstant.WF (addDefEq env✝ df✝) ci
Tactic:
exact .mono addDefEq_le (ih h)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case empty
env : VEnv
df : VDefEq
h : ∅.defeqs df
⊢ VDefEq.WF ∅ df
Tactic:
cases h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ VDefEq.WF env'✝ df
Tactic:
refine .mono (addConst_le h3) (ih ?_)
Proof state after:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Tactic:
unfold addConst at h3
Proof state after:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Tactic:
split at h3 <;> cases h3
Proof state after:
case const.h_2.refl
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.defeqs df → VDefEq.WF env✝ df
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h : { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.defeqs df
⊢ env✝.defeqs df
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case const.h_2.refl
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.defeqs df → VDefEq.WF env✝ df
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h : { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.defeqs df
⊢ env✝.defeqs df
Tactic:
exact h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF (addDefEq env✝ df✝) df
Tactic:
refine .mono addDefEq_le ?_
Proof state after:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF env✝ df
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF env✝ df
Tactic:
obtain rfl | h := h
Proof state after:
case defeq.inl
env : VEnv
df : VDefEq
env✝ : VEnv
a✝¹ : Ordered env✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
a✝ : VDefEq.WF env✝ df
⊢ VDefEq.WF env✝ df

case defeq.inr
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env✝.defeqs df
⊢ VDefEq.WF env✝ df
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case defeq.inl
env : VEnv
df : VDefEq
env✝ : VEnv
a✝¹ : Ordered env✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
a✝ : VDefEq.WF env✝ df
⊢ VDefEq.WF env✝ df
Tactic:
assumption
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.defEqWF
Proof state before:
case defeq.inr
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env✝.defeqs df
⊢ VDefEq.WF env✝ df
Tactic:
exact ih h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
H : IsDefEq env U Γ e1 e2 A
W : OnCtx Γ fun x A => LevelWF U A
⊢ LevelWF U e1 ∧ LevelWF U e2 ∧ LevelWF U A
Tactic:
induction H with
| bvar h =>
  refine ⟨⟨⟩, ⟨⟩, ?_⟩
  induction h with
  | zero => exact W.2.liftN
  | succ _ ih => exact (ih W.1).liftN
| symm _ ih => let ⟨he, he', hA⟩ := ih W; exact ⟨he', he, hA⟩
| trans _ _ ih1 ih2 => let ⟨he1, _, hA⟩ := ih1 W; let ⟨_, he3, _⟩ := ih2 W; exact ⟨he1, he3, hA⟩
| sortDF h1 h2 => exact ⟨h1, h2, h1⟩
| constDF _ h2 h3 => exact ⟨h2, h3, .instL h2⟩
| appDF _ _ ih1 ih2 =>
  let ⟨hf, hf', _, hB⟩ := ih1 W; let ⟨ha, ha', _⟩ := ih2 W
  exact ⟨⟨hf, ha⟩, ⟨hf', ha'⟩, hB.inst ha⟩
| lamDF _ _ ih1 ih2 =>
  let ⟨hA, hA', _⟩ := ih1 W; let ⟨hb, hb', hB⟩ := ih2 ⟨W, hA⟩
  exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hA, hB⟩
| forallEDF _ _ ih1 ih2 =>
  let ⟨hA, hA', hu⟩ := ih1 W; let ⟨hb, hb', hv⟩ := ih2 ⟨W, hA⟩
  exact ⟨⟨hA, hb⟩, ⟨hA', hb'⟩, hu, hv⟩
| defeqDF _ _ ih1 ih2 => let ⟨_, hB, _⟩ := ih1 W; let ⟨he1, he2, _⟩ := ih2 W; exact ⟨he1, he2, hB⟩
| beta _ _ ih1 ih2 =>
  let ⟨he', _, hA⟩ := ih2 W; let ⟨he, _, hB⟩ := ih1 ⟨W, hA⟩
  exact ⟨⟨⟨hA, he⟩, he'⟩, he.inst he', hB.inst he'⟩
| eta _ ih => let ⟨he, _, hA, hB⟩ := ih W; exact ⟨⟨hA, he.liftN, ⟨⟩⟩, he, hA, hB⟩
| proofIrrel _ _ _ _ ih2 ih3 =>
  let ⟨hh, _, hp⟩ := ih2 W; let ⟨hh', _, _⟩ := ih3 W
  exact ⟨hh, hh', hp⟩
| extra _ h2 => exact ⟨.instL h2, .instL h2, .instL h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case bvar
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (VExpr.bvar i✝) ∧ LevelWF U (VExpr.bvar i✝) ∧ LevelWF U A✝
Tactic:
refine ⟨⟨⟩, ⟨⟩, ?_⟩
Proof state after:
case bvar
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U A✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case bvar
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U A✝
Tactic:
induction h with
| zero => exact W.2.liftN
| succ _ ih => exact (ih W.1).liftN
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case bvar.zero
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
i✝ : Nat
A✝ ty✝ : VExpr
Γ✝ : List VExpr
W : OnCtx (ty✝ :: Γ✝) fun x A => LevelWF U A
⊢ LevelWF U (lift ty✝)
Tactic:
exact W.2.liftN
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case bvar.succ
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝¹ : List VExpr
i✝ : Nat
A✝¹ : VExpr
Γ✝ : List VExpr
n✝ : Nat
ty✝ A✝ : VExpr
a✝ : Lookup Γ✝ n✝ ty✝
ih : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U ty✝
W : OnCtx (A✝ :: Γ✝) fun x A => LevelWF U A
⊢ LevelWF U (lift ty✝)
Tactic:
exact (ih W.1).liftN
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case symm
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : (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 e'✝ ∧ LevelWF U e✝ ∧ LevelWF U A✝
Tactic:
let ⟨he, he', hA⟩ := ih W
Proof state after:
case symm
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : (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 : LevelWF U e✝
he' : LevelWF U e'✝
hA : LevelWF U A✝
⊢ LevelWF U e'✝ ∧ LevelWF U e✝ ∧ LevelWF U A✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case symm
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : (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 : LevelWF U e✝
he' : LevelWF U e'✝
hA : LevelWF U A✝
⊢ LevelWF U e'✝ ∧ LevelWF U e✝ ∧ LevelWF U A✝
Tactic:
exact ⟨he', he, hA⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case trans
env : VEnv
U : Nat
Γ : List VExpr
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 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e₁✝ ∧ LevelWF U e₂✝ ∧ LevelWF U A✝
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 e₁✝ ∧ LevelWF U e₃✝ ∧ LevelWF U A✝
Tactic:
let ⟨he1, _, hA⟩ := ih1 W
Proof state after:
case trans
env : VEnv
U : Nat
Γ : List VExpr
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 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e₁✝ ∧ LevelWF U e₂✝ ∧ LevelWF U A✝
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
he1 : LevelWF U e₁✝
left✝ : LevelWF U e₂✝
hA : LevelWF U A✝
⊢ LevelWF U e₁✝ ∧ LevelWF U e₃✝ ∧ LevelWF U A✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case trans
env : VEnv
U : Nat
Γ : List VExpr
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 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e₁✝ ∧ LevelWF U e₂✝ ∧ LevelWF U A✝
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
he1 : LevelWF U e₁✝
left✝ : LevelWF U e₂✝
hA : LevelWF U A✝
⊢ LevelWF U e₁✝ ∧ LevelWF U e₃✝ ∧ LevelWF U A✝
Tactic:
let ⟨_, he3, _⟩ := ih2 W
Proof state after:
case trans
env : VEnv
U : Nat
Γ : List VExpr
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 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e₁✝ ∧ LevelWF U e₂✝ ∧ LevelWF U A✝
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
he1 : LevelWF U e₁✝
left✝¹ : LevelWF U e₂✝
hA : LevelWF U A✝
left✝ : LevelWF U e₂✝
he3 : LevelWF U e₃✝
right✝ : LevelWF U A✝
⊢ LevelWF U e₁✝ ∧ LevelWF U e₃✝ ∧ LevelWF U A✝
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case trans
env : VEnv
U : Nat
Γ : List VExpr
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 : (OnCtx Γ✝ fun x A => LevelWF U A) → LevelWF U e₁✝ ∧ LevelWF U e₂✝ ∧ LevelWF U A✝
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
he1 : LevelWF U e₁✝
left✝¹ : LevelWF U e₂✝
hA : LevelWF U A✝
left✝ : LevelWF U e₂✝
he3 : LevelWF U e₃✝
right✝ : LevelWF U A✝
⊢ LevelWF U e₁✝ ∧ LevelWF U e₃✝ ∧ LevelWF U A✝
Tactic:
exact ⟨he1, he3, hA⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case sortDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
a✝ : l✝ ≈ l'✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (VExpr.sort l✝) ∧ LevelWF U (VExpr.sort l'✝) ∧ LevelWF U (VExpr.sort (VLevel.succ l✝))
Tactic:
exact ⟨h1, h2, h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.levelWF
Proof state before:
case constDF
env : VEnv
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
a✝² : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
W : OnCtx Γ✝ fun x A => LevelWF U A
⊢ LevelWF U (VExpr.const c✝ ls✝) ∧ LevelWF U (VExpr.const c✝ ls'✝) ∧ LevelWF U (instL ls✝ ci✝.type)
Tactic:
exact ⟨h2, h3, .instL h2⟩
Proof state after:
no goals
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
⊢ LevelWF U (app f✝ a✝²) ∧ LevelWF U (app f'✝ a'✝) ∧ LevelWF U (inst B✝ a✝²)
Tactic:
let ⟨hf, hf', _, hB⟩ := ih1 W
Proof state after:
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✝
⊢ LevelWF U (app f✝ a✝²) ∧ LevelWF U (app f'✝ a'✝) ∧ LevelWF U (inst B✝ a✝²)
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✝
⊢ LevelWF U (app f✝ a✝²) ∧ LevelWF U (app f'✝ a'✝) ∧ LevelWF U (inst B✝ a✝²)
Tactic:
let ⟨ha, ha', _⟩ := ih2 W
Proof state after:
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✝²)