internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have he := ih1 hΓ'
Proof state after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have ⟨_, hB⟩ := he.isType' henv envIH hΓ'
Proof state after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝¹ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝¹)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝¹ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝¹)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
exact .beta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
  hA hB he he' (he'.instN henv hΓ .zero hB hΓ) (he'.instN henv hΓ .zero he hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
have he := ih hΓ
Proof state after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
let ⟨_, hAB⟩ := he.isType' henv envIH hΓ
Proof state after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := hAB.forallE_inv' henv envIH hΓ (.inl rfl)
Proof state after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
Proof state after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
exact .eta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
  hA hB (hB.weakN henv (.succ .one)) he (he.weakN henv .one)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : 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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ h✝ h✝ p✝
ih3 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ h✝ h'✝ p✝
Tactic:
exact .proofIrrel (ih1 hΓ) (ih2 hΓ) (ih3 hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
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
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
let ⟨⟨hl, ⟨_, ht⟩, _⟩, hr, _, _⟩ := envIH.2 h1
Proof state after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
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
hΓ : CtxStrong env U Γ✝
hl : IsDefEqStrong env df✝.uvars [] df✝.lhs df✝.lhs df✝.type
w✝ : VLevel
ht : IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort w✝)
right✝¹ :
  ∀ (A B : VExpr),
    df✝.lhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
hr : IsDefEqStrong env df✝.uvars [] df✝.rhs df✝.rhs df✝.type
left✝ : ∃ u, IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort u)
right✝ :
  ∀ (A B : VExpr),
    df✝.rhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
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
hΓ : CtxStrong env U Γ✝
hl : IsDefEqStrong env df✝.uvars [] df✝.lhs df✝.lhs df✝.type
w✝ : VLevel
ht : IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort w✝)
right✝¹ :
  ∀ (A B : VExpr),
    df✝.lhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
hr : IsDefEqStrong env df✝.uvars [] df✝.rhs df✝.rhs df✝.type
left✝ : ∃ u, IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort u)
right✝ :
  ∀ (A B : VExpr),
    df✝.rhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3 (.inst h2) (ht.instL h2)
  (hl.instL h2) (hr.instL h2) ((hl.instL h2).weak0 henv) ((hr.instL h2).weak0 henv)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.CtxStrong.strong'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
hΓ : OnCtx Γ (IsType env U)
⊢ CtxStrong env U Γ
Tactic:
induction Γ with
| nil => trivial
| cons _ _ ih => let ⟨hΓ, _, hA⟩ := hΓ; exact ⟨ih hΓ, _, hA.strong' henv envIH (ih hΓ)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.CtxStrong.strong'
Proof state before:
case nil
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
hΓ : OnCtx [] (IsType env U)
⊢ CtxStrong env U []
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.CtxStrong.strong'
Proof state before:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ : OnCtx (head✝ :: tail✝) (IsType env U)
⊢ CtxStrong env U (head✝ :: tail✝)
Tactic:
let ⟨hΓ, _, hA⟩ := hΓ
Proof state after:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ✝ : OnCtx (head✝ :: tail✝) (IsType env U)
hΓ : OnCtx tail✝ (IsType env U)
w✝ : VLevel
hA : HasType env U tail✝ head✝ (sort w✝)
⊢ CtxStrong env U (head✝ :: tail✝)
Theorem: Lean4Lean.VEnv.CtxStrong.strong'
Proof state before:
case cons
env : VEnv
U : Nat
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
head✝ : VExpr
tail✝ : List VExpr
ih : OnCtx tail✝ (IsType env U) → CtxStrong env U tail✝
hΓ✝ : OnCtx (head✝ :: tail✝) (IsType env U)
hΓ : OnCtx tail✝ (IsType env U)
w✝ : VLevel
hA : HasType env U tail✝ head✝ (sort w✝)
⊢ CtxStrong env U (head✝ :: tail✝)
Tactic:
exact ⟨ih hΓ, _, hA.strong' henv envIH (ih hΓ)⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V f a : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = app f a ∨ e2 = app f a
⊢ ∃ A B, HasType env U Γ f (VExpr.forallE A B) ∧ HasType env U Γ a A
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 f a : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = app f a ∨ e2 = app f a
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ A B, HasType env U Γ f (VExpr.forallE A B) ∧ HasType env U Γ a A
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 V f a : VExpr
H : IsDefEq env U Γ e1 e2 V
eq : e1 = app f a ∨ e2 = app f a
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ A B, HasType env U Γ f (VExpr.forallE A B) ∧ HasType env U Γ a A
Tactic:
clear H hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
eq : e1 = app f a ∨ e2 = app f a
H' : IsDefEqStrong env U Γ e1 e2 V
⊢ ∃ 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 symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ 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
eq : e'✝ = app f a ∨ e✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ih eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case extra
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : 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 = app f a ∨ VExpr.instL ls✝ df✝.type = app f a →
    ∃ A B, HasType env U [] f (VExpr.forallE A B) ∧ HasType env U [] a A
a_ih✝¹ :
  VExpr.instL ls✝ df✝.lhs = app f a ∨ VExpr.instL ls✝ df✝.lhs = app f a →
    ∃ A B, HasType env U [] f (VExpr.forallE A B) ∧ HasType env U [] a A
a_ih✝ :
  VExpr.instL ls✝ df✝.rhs = app f a ∨ VExpr.instL ls✝ df✝.rhs = app f a →
    ∃ A B, HasType env U [] f (VExpr.forallE A B) ∧ HasType env U [] a A
ih1 :
  VExpr.instL ls✝ df✝.lhs = app f a ∨ VExpr.instL ls✝ df✝.lhs = app f a →
    ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ih2 :
  VExpr.instL ls✝ df✝.rhs = app f a ∨ VExpr.instL ls✝ df✝.rhs = app f a →
    ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : VExpr.instL ls✝ df✝.lhs = app f a ∨ VExpr.instL ls✝ df✝.rhs = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
obtain eq | eq := eq <;> [exact ih1 (.inl eq); exact ih2 (.inr eq)]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case appDF.inl.refl
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
f'✝ a'✝ : 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_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
h1 : IsDefEqStrong env U Γ✝ f f'✝ (VExpr.forallE A✝ B✝)
a_ih✝² : f = app f a ∨ f'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
h2 : IsDefEqStrong env U Γ✝ a a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a) (inst B✝ a'✝) (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✝ :
  inst B✝ a = app f a ∨ inst B✝ a'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ⟨_, _, h1.defeq.hasType.1, h2.defeq.hasType.1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case appDF.inr.refl
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
f✝ a✝⁵ : 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_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
h1 : IsDefEqStrong env U Γ✝ f✝ f (VExpr.forallE A✝ B✝)
a_ih✝² : f✝ = app f a ∨ f = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
h2 : IsDefEqStrong env U Γ✝ a✝⁵ a A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁵) (inst B✝ a) (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✝ :
  inst B✝ a✝⁵ = app f a ∨ inst B✝ a = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ⟨_, _, h1.defeq.hasType.2, h2.defeq.hasType.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : 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✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ih2 : e1✝ = app f a ∨ e2✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : e1✝ = app f a ∨ e2✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
exact ih2 eq
Proof state after:
no goals