internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case appDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst f✝ e₀ k) (inst f'✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst a✝² e₀ k) (inst a'✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (app f✝ a✝²) e₀ k) (inst (app f'✝ a'✝) e₀ k) (inst (inst B✝ a✝²) e₀ k)
Tactic:
exact VExpr.inst_inst_hi .. ▸ .appDF (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case lamDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst A✝ e₀ k) (inst A'✝ e₀ k) (inst (VExpr.sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ → IsDefEq env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst B✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (lam A✝ body✝) e₀ k) (inst (lam A'✝ body'✝) e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Tactic:
exact .lamDF (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case forallEDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst A✝ e₀ k) (inst A'✝ e₀ k) (inst (VExpr.sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ → IsDefEq env U Γ (inst body✝ e₀ k) (inst body'✝ e₀ k) (inst (VExpr.sort v✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.forallE A✝ body✝) e₀ k) (inst (VExpr.forallE A'✝ body'✝) e₀ k)
    (inst (VExpr.sort (VLevel.imax u✝ v✝)) e₀ k)
Tactic:
exact .forallEDF (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case defeqDF
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst A✝ e₀ k) (inst B✝ e₀ k) (inst (VExpr.sort u✝) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e1✝ e₀ k) (inst e2✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst e1✝ e₀ k) (inst e2✝ e₀ k) (inst B✝ e₀ k)
Tactic:
exact .defeqDF (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case beta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k (A✝ :: Γ✝) Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst B✝ e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e'✝ e₀ k) (inst e'✝ e₀ k) (inst A✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (app (lam A✝ e✝) e'✝) e₀ k) (inst (inst e✝ e'✝) e₀ k) (inst (inst B✝ e'✝) e₀ k)
Tactic:
exact VExpr.inst_inst_hi .. ▸ VExpr.inst_inst_hi .. ▸ .beta (ih1 W.succ) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Tactic:
have := IsDefEq.eta (ih W)
Proof state after:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
this :
  IsDefEq env U Γ (lam (inst A✝ e₀ k) (app (lift (inst e✝ e₀ k)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (VExpr.forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEq env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
this :
  IsDefEq env U Γ (lam (inst A✝ e₀ k) (app (lift (inst e✝ e₀ k)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (VExpr.forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEq env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Tactic:
rw [lift, VExpr.liftN_instN_lo (hj := Nat.zero_le _), Nat.add_comm] at this
Proof state after:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
this :
  IsDefEq env U Γ (lam (inst A✝ e₀ k) (app (inst (liftN 1 e✝) e₀ (k + 1)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (VExpr.forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEq env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case eta
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst e✝ e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
this :
  IsDefEq env U Γ (lam (inst A✝ e₀ k) (app (inst (liftN 1 e✝) e₀ (k + 1)) (VExpr.bvar 0))) (inst e✝ e₀ k)
    (VExpr.forallE (inst A✝ e₀ k) (inst B✝ e₀ (k + 1)))
⊢ IsDefEq env U Γ (inst (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e₀ k) (inst e✝ e₀ k) (inst (VExpr.forallE A✝ B✝) e₀ k)
Tactic:
simpa [inst]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case proofIrrel
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst p✝ e₀ k) (inst p✝ e₀ k) (inst (VExpr.sort VLevel.zero) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst h✝ e₀ k) (inst h✝ e₀ k) (inst p✝ e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → IsDefEq env U Γ (inst h'✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst h✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
Tactic:
exact .proofIrrel (ih1 W) (ih2 W) (ih3 W)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
⊢ IsDefEq env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Tactic:
have ⟨⟨hA1, _⟩, hA2, hA3⟩ := henv.closed.2 h1
Proof state after:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
    (inst (VExpr.instL ls✝ df✝.type) e₀ k)
Tactic:
rw [
  hA1.instL.instN_eq (Nat.zero_le _),
  hA2.instL.instN_eq (Nat.zero_le _),
  hA3.instL.instN_eq (Nat.zero_le _)]
Proof state after:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.instN
Proof state before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : HasType env U Γ₀ e₀ A₀
Γ₁ : 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
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
⊢ IsDefEq env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B
Tactic:
have ⟨_, H1, H2⟩ : ∃ Γ', Ctx.LiftN 1 (Δ.length + 1) (Δ ++ A :: Γ) Γ' ∧
    Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) Δ.length Γ' (Δ ++ A' :: Γ) := by
  clear h1 h2
  induction Δ with
  | nil => exact ⟨_, .succ (.one (A := A')), .zero⟩
  | cons B Δ ih =>
    have ⟨Γ', h1, h2⟩ := ih
    exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
Proof state after:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
w✝ : List VExpr
H1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) w✝
H2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) w✝ (Δ ++ A' :: Γ)
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
w✝ : List VExpr
H1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) w✝
H2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) w✝ (Δ ++ A' :: Γ)
⊢ IsDefEq env U (Δ ++ A' :: Γ) e1 e2 B
Tactic:
simpa [instN_bvar0] using
  instN henv (h1.weakN henv (.one (A := A')) |>.symm.defeq (.bvar .zero)) H2 (.weakN henv H1 h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
h1 : IsDefEq env U Γ A A' (VExpr.sort u)
h2 : IsDefEq env U (Δ ++ A :: Γ) e1 e2 B
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Tactic:
clear h1 h2
Proof state after:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
Δ : List VExpr
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Tactic:
induction Δ with
| nil => exact ⟨_, .succ (.one (A := A')), .zero⟩
| cons B Δ ih =>
  have ⟨Γ', h1, h2⟩ := ih
  exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
case nil
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B : VExpr
henv : Ordered env
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length [] + 1) ([] ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length []) Γ' ([] ++ A' :: Γ)
Tactic:
exact ⟨_, .succ (.one (A := A')), .zero⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)
Tactic:
have ⟨Γ', h1, h2⟩ := ih
Proof state after:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
case cons
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ ∃ Γ',
    Ctx.LiftN 1 (List.length (B :: Δ) + 1) (B :: Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) Γ' (B :: Δ ++ A' :: Γ)
Tactic:
exact ⟨_, .succ h1, by simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDF_l'
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B✝ : VExpr
henv : Ordered env
B : VExpr
Δ : List VExpr
ih :
  ∃ Γ',
    Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ' ∧
      Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
Γ' : List VExpr
h1 : Ctx.LiftN 1 (List.length Δ + 1) (Δ ++ A :: Γ) Γ'
h2 : Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length Δ) Γ' (Δ ++ A' :: Γ)
⊢ Ctx.InstN (A' :: Γ) (VExpr.bvar 0) (liftN 1 A) (List.length (B :: Δ)) (liftN 1 B (List.length (B :: Δ)) :: Γ')
    (B :: Δ ++ A' :: Γ)
Tactic:
simpa [instN_bvar0] using h2.succ (A := liftN 1 B (Δ.length + 1))
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDFC'
Proof state before:
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ Δ : List VExpr
e₁ e₂ A : VExpr
henv : Ordered env
h1 : IsDefEqCtx env U Γ₀ Γ₁ Γ₂
h2 : IsDefEq env U (Δ ++ Γ₁) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ Γ₂) e₁ e₂ A
Tactic:
induction h1 generalizing e₁ e₂ A Δ with
| zero => exact h2
| @succ _ _ _ A₂ _ _ AA ih =>
  simpa using ih (Δ := Δ ++ [A₂]) (by simpa using AA.defeqDF_l' henv h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDFC'
Proof state before:
case zero
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ Γ₀) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ Γ₀) e₁ e₂ A
Tactic:
exact h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDFC'
Proof state before:
case succ
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Γ₁✝ Γ₂✝ : List VExpr
A₁✝ A₂ : VExpr
u✝ : VLevel
a✝ : IsDefEqCtx env U Γ₀ Γ₁✝ Γ₂✝
AA : IsDefEq env U Γ₁✝ A₁✝ A₂ (VExpr.sort u✝)
ih : ∀ {Δ : List VExpr} {e₁ e₂ A : VExpr}, IsDefEq env U (Δ ++ Γ₁✝) e₁ e₂ A → IsDefEq env U (Δ ++ Γ₂✝) e₁ e₂ A
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ A₁✝ :: Γ₁✝) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ A₂ :: Γ₂✝) e₁ e₂ A
Tactic:
simpa using ih (Δ := Δ ++ [A₂]) (by simpa using AA.defeqDF_l' henv h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.defeqDFC'
Proof state before:
env : VEnv
U : Nat
Γ₀ Γ₁ Γ₂ : List VExpr
henv : Ordered env
Γ₁✝ Γ₂✝ : List VExpr
A₁✝ A₂ : VExpr
u✝ : VLevel
a✝ : IsDefEqCtx env U Γ₀ Γ₁✝ Γ₂✝
AA : IsDefEq env U Γ₁✝ A₁✝ A₂ (VExpr.sort u✝)
ih : ∀ {Δ : List VExpr} {e₁ e₂ A : VExpr}, IsDefEq env U (Δ ++ Γ₁✝) e₁ e₂ A → IsDefEq env U (Δ ++ Γ₂✝) e₁ e₂ A
Δ : List VExpr
e₁ e₂ A : VExpr
h2 : IsDefEq env U (Δ ++ A₁✝ :: Γ₁✝) e₁ e₂ A
⊢ IsDefEq env U (Δ ++ [A₂] ++ Γ₁✝) e₁ e₂ A
Tactic:
simpa using AA.defeqDF_l' henv h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e'✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain eq | eq := eq
Proof state after:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B

case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih1 (.inl eq)
Proof state after:
no goals