internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := h3.forallE_inv' henv envIH hΓ (.inl rfl)
Proof state after:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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 Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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 Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hu := hA.defeq.sort_r henv hΓ.defeq
Proof state after:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
Proof state after:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hv := hB.defeq.sort_r henv hΓ'.defeq
Proof state after:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
hv : VLevel.WF U v
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case appDF
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
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 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : 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)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
hv : VLevel.WF U v
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
exact .appDF hu hv hA hB (ih1 hΓ) (ih2 hΓ) <|
  .instDF (v := v.succ) henv hΓ hu hv hA (.sortDF hv hv rfl) hB (ih2 hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
have hu := hA.sort_r henv hΓ.defeq
Proof state after:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
Proof state after:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
let ⟨_, hB⟩ := (ih2 hΓ').isType' henv envIH hΓ'
Proof state after:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case lamDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .lamDF hu (hB.defeq.sort_r henv hΓ'.defeq) (ih1 hΓ)
  hB ((ih1 hΓ).defeqDF_l henv hΓ hB) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case forallEDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
have hu := hA.sort_r henv hΓ.defeq
Proof state after:
case forallEDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case forallEDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
Proof state after:
case forallEDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case forallEDF
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
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallEDF hu (hb.sort_r henv hΓ'.defeq)
  (ih1 hΓ) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.strong'
Proof state before:
case defeqDF
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
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
hAB : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ e1✝ e2✝ B✝
Tactic:
exact .defeqDF (hAB.sort_r henv hΓ.defeq) (ih1 hΓ) (ih2 hΓ)
Proof state after:
no goals
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 Γ✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have he' := ih2 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✝
⊢ 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✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have ⟨_, hA⟩ := 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✝)
⊢ 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✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
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✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)