internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case beta.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V a : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a_ih✝⁴ :
  A✝ = app (lam A✝ e✝) a ∨ A✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app (lam A✝ e✝) a ∨ B✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U (A✝ :: Γ✝) (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝² :
  e✝ = app (lam A✝ e✝) a ∨ e✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U (A✝ :: Γ✝) (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
he' : IsDefEqStrong env U Γ✝ a a A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ a) (inst B✝ a) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ a) (inst e✝ a) (inst B✝ a)
a_ih✝¹ :
  a = app (lam A✝ e✝) a ∨ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ a = app (lam A✝ e✝) a ∨ inst B✝ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ihee :
  inst e✝ a = app (lam A✝ e✝) a ∨ inst e✝ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ⟨_, _, .lam hA.defeq he.defeq, he'.defeq⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case beta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f 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✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝² :
  e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ : e'✝ = app f a ∨ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ e'✝ = app f a ∨ inst B✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ihee :
  inst e✝ e'✝ = app f a ∨ inst e✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : inst e✝ e'✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ihee (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case eta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝² :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ :
  liftN 1 B✝ 1 = app f a ∨ liftN 1 B✝ 1 = app f a →
    ∃ A B, HasType env U (lift A✝ :: A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (lift A✝ :: A✝ :: Γ✝) a A
ih : e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  lift e✝ = app f a ∨ lift e✝ = app f a →
    ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = app f a ∨ e✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case eta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝² :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ :
  liftN 1 B✝ 1 = app f a ∨ liftN 1 B✝ 1 = app f a →
    ∃ A B, HasType env U (lift A✝ :: A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (lift A✝ :: A✝ :: Γ✝) a A
ih : e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  lift e✝ = app f a ∨ lift e✝ = app f a →
    ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
eq : e✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case eta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f 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✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝² :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ :
  liftN 1 B✝ 1 = app f a ∨ liftN 1 B✝ 1 = app f a →
    ∃ A B, HasType env U (lift A✝ :: A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (lift A✝ :: A✝ :: Γ✝) a A
ih : e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  lift e✝ = app f a ∨ lift e✝ = app f a →
    ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
eq : e✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ih (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case forallEDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝² : A✝ = app f a ∨ A'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝¹ :
  body✝ = app f a ∨ body'✝ = app f a →
    ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝ :
  body✝ = app f a ∨ body'✝ = app f a →
    ∃ A B, HasType env U (A'✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A'✝ :: Γ✝) a A
eq : VExpr.forallE A✝ body✝ = app f a ∨ VExpr.forallE A'✝ body'✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V A body : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = lam A body ∨ e2 = lam A body
⊢ IsType env U Γ A ∧ WF env U (A :: Γ) body
Tactic:
have H' := H.strong henv hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V A body : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = lam A body ∨ e2 = lam A body
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ IsType env U Γ A ∧ WF env U (A :: Γ) body
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V A body : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = lam A body ∨ e2 = lam A body
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ IsType env U Γ A ∧ WF env U (A :: Γ) body
Tactic:
clear H hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
eq : e1 = lam A body ∨ e2 = lam A body
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ IsType env U Γ A ∧ WF env U (A :: Γ) body
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : e✝ = lam A body ∨ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : e'✝ = lam A body ∨ e✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ih eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case extra
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
a✝⁸ : env.defeqs df✝
a✝⁷ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝⁶ : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (VExpr.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)
a_ih✝² :
  VExpr.instL ls✝ df✝.type = lam A body ∨ VExpr.instL ls✝ df✝.type = lam A body → IsType env U [] A ∧ WF env U [A] body
a_ih✝¹ :
  VExpr.instL ls✝ df✝.lhs = lam A body ∨ VExpr.instL ls✝ df✝.lhs = lam A body → IsType env U [] A ∧ WF env U [A] body
a_ih✝ :
  VExpr.instL ls✝ df✝.rhs = lam A body ∨ VExpr.instL ls✝ df✝.rhs = lam A body → IsType env U [] A ∧ WF env U [A] body
ih1 :
  VExpr.instL ls✝ df✝.lhs = lam A body ∨ VExpr.instL ls✝ df✝.lhs = lam A body →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
ih2 :
  VExpr.instL ls✝ df✝.rhs = lam A body ∨ VExpr.instL ls✝ df✝.rhs = lam A body →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : VExpr.instL ls✝ df✝.lhs = lam A body ∨ VExpr.instL ls✝ df✝.rhs = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
obtain eq | eq := eq <;> [exact ih1 (.inl eq); exact ih2 (.inr eq)]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case lamDF.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body'✝ : VExpr
a✝³ : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
a✝¹ : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
h1 : IsDefEqStrong env U Γ✝ A A'✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U (A :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝³ : A = lam A body ∨ A'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
h5 : IsDefEqStrong env U (A'✝ :: Γ✝) body body'✝ B✝
a_ih✝¹ : body = lam A body ∨ body'✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
h4 : IsDefEqStrong env U (A :: Γ✝) body body'✝ B✝
a_ih✝ : body = lam A body ∨ body'✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ⟨⟨_, h1.defeq.hasType.1⟩, _, h4.defeq.hasType.1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case lamDF.inr.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ : VExpr
a✝³ : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
h1 : IsDefEqStrong env U Γ✝ A✝ A (VExpr.sort u✝)
a✝ : IsDefEqStrong env U (A :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝³ : A✝ = lam A body ∨ A = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
h4 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body B✝
a_ih✝¹ : body✝ = lam A body ∨ body = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
h5 : IsDefEqStrong env U (A :: Γ✝) body✝ body B✝
a_ih✝ : body✝ = lam A body ∨ body = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ⟨⟨_, h1.defeq.hasType.2⟩, _, h5.defeq.hasType.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
a_ih✝ : A✝ = lam A body ∨ B✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
ih2 : e1✝ = lam A body ∨ e2✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : e1✝ = lam A body ∨ e2✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ih2 eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case beta
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : 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✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.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'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ : A✝ = lam A body ∨ A✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝³ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝² : e✝ = lam A body ∨ e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝¹ : e'✝ = lam A body ∨ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : inst B✝ e'✝ = lam A body ∨ inst B✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
ihee : inst e✝ e'✝ = lam A body ∨ inst e✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : app (lam A✝ e✝) e'✝ = lam A body ∨ inst e✝ e'✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case beta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : 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✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.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'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ : A✝ = lam A body ∨ A✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝³ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝² : e✝ = lam A body ∨ e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝¹ : e'✝ = lam A body ∨ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : inst B✝ e'✝ = lam A body ∨ inst B✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
ihee : inst e✝ e'✝ = lam A body ∨ inst e✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : inst e✝ e'✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case beta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : 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✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.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'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ : A✝ = lam A body ∨ A✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝³ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝² : e✝ = lam A body ∨ e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝¹ : e'✝ = lam A body ∨ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : inst B✝ e'✝ = lam A body ∨ inst B✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
ihee : inst e✝ e'✝ = lam A body ∨ inst e✝ e'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
eq : inst e✝ e'✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ihee (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case eta.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A : VExpr
Γ✝ : List VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A A (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (lift A :: A :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A B✝)
he' : IsDefEqStrong env U (A :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A) (liftN 1 B✝ 1))
ih :
  e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝³ :
  A = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ A = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝² :
  B✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ B✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝¹ :
  liftN 1 B✝ 1 = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ liftN 1 B✝ 1 = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (lift A :: A :: Γ✝) A ∧ WF env U (A :: lift A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝ :
  lift e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ lift e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
Tactic:
exact ⟨⟨_, hA.defeq.hasType.1⟩, _, he'.defeq.hasType.1.app (.bvar .zero)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case eta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
he' : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ : A✝ = lam A body ∨ A✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝¹ :
  liftN 1 B✝ 1 = lam A body ∨ liftN 1 B✝ 1 = lam A body →
    IsType env U (lift A✝ :: A✝ :: Γ✝) A ∧ WF env U (A :: lift A✝ :: A✝ :: Γ✝) body
ih : e✝ = lam A body ∨ e✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : lift e✝ = lam A body ∨ lift e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
eq : e✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
exact ih (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case forallEDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝² : A✝ = lam A body ∨ A'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝¹ : body✝ = lam A body ∨ body'✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝ : body✝ = lam A body ∨ body'✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
eq : VExpr.forallE A✝ body✝ = lam A body ∨ VExpr.forallE A'✝ body'✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V : VExpr
c : Name
ls : List VLevel
H : IsDefEq env U Γ e1 e2 V
eq : e1 = VExpr.const c ls ∨ e2 = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
have H' := H.strong henv hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V : VExpr
c : Name
ls : List VLevel
H : IsDefEq env U Γ e1 e2 V
eq : e1 = VExpr.const c ls ∨ e2 = VExpr.const c ls
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V : VExpr
c : Name
ls : List VLevel
H : IsDefEq env U Γ e1 e2 V
eq : e1 = VExpr.const c ls ∨ e2 = VExpr.const c ls
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
clear H hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
eq : e1 = VExpr.const c ls ∨ e2 = VExpr.const c ls
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars