internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (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) (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✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ IsDefEqStrong env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.instL ls B) (sort (VLevel.inst ls v))
Tactic:
simpa [liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (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) (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✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ
eq : VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = forallE A B →
      EnvStrong env df.uvars e df.type →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ u, IsDefEqStrong env U (A :: Γ) B B (sort u)
A1 : EnvStrong env df.uvars df.lhs df.type
A2 : EnvStrong env df.uvars df.rhs df.type
⊢ (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
Tactic:
cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
u✝ : VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (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) (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✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.type = forallE A B ∨ VExpr.instL ls df.type = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U [] →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U [] A A (sort u)) ∧ ∃ v, IsDefEqStrong env U [A] B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.lhs = forallE A B ∨ VExpr.instL ls df.lhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ →
      VExpr.instL ls df.rhs = forallE A B ∨ VExpr.instL ls df.rhs = forallE A B →
        (∃ u, IsDefEqStrong env U Γ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ) B B (sort v)
hΓ : CtxStrong env U Γ
A B : VExpr
IH : EnvStrong env df.uvars (forallE A B) df.type
eq :
  VExpr.instL ls df.lhs = forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : IsDefEqStrong env df.uvars [] A A (sort w✝)
v : VLevel
A2 : IsDefEqStrong env df.uvars [A] B B (sort v)
this :
  IsDefEqStrong env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1))
    (liftN (List.length Γ) (VExpr.instL ls (sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
C2 : ClosedN (VExpr.instL ls B) (List.length (List.map (VExpr.instL ls) [A]))
⊢ List.length (List.map (VExpr.instL ls) [A]) ≤ 0 + 1
Tactic:
exact Nat.le_refl _
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝⁴ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ A'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
a_ih✝³ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝² :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      B✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
a_ih✝¹ :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U (A'✝ :: Γ✝) →
      body✝ = forallE A B ∨ body'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A'✝ :: Γ✝) B B (sort v)
A B : VExpr
hΓ : CtxStrong env U Γ✝
eq : lam A✝ body✝ = forallE A B ∨ lam A'✝ body'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hΓ : CtxStrong env U Γ
H : IsDefEqStrong env U Γ e1 e2 A
⊢ ∃ u, IsDefEqStrong env U Γ A A (sort u)
Tactic:
induction H with
| bvar h => exact hΓ.lookup henv h
| symm _ ih => exact ih hΓ
| trans _ _ ih1 => exact ih1 hΓ
| sortDF h1 => exact ⟨_, .sortDF h1 h1 rfl⟩
| constDF h1 h2 =>
  let ⟨_, h⟩ := envIH.1 h1
  exact ⟨_, (h.1.instL h2).weak0 henv⟩
| appDF _ _ _ _ _ h4 _ _ _ ih3 =>
  let ⟨_, ih3⟩ := ih3 hΓ
  have ⟨_, _, ih3⟩ := ih3.forallE_inv' henv envIH hΓ (.inl rfl)
  exact ⟨_, h4.hasType.1.instN henv hΓ .zero ih3 hΓ⟩
| lamDF h1 h2 h3 h4 => exact ⟨_, .forallEDF h1 h2 h3.hasType.1 h4 h4⟩
| forallEDF h1 h2 => exact ⟨_, .sortDF ⟨h1, h2⟩ ⟨h1, h2⟩ rfl⟩
| defeqDF _ h2 => exact ⟨_, h2.hasType.2⟩
| beta _ _ _ h4 _ h6 => exact ⟨_, h6.hasType.1.instN henv hΓ .zero h4 hΓ⟩
| eta _ _ _ _ _ _ _ _ _ _ ih => exact ih hΓ
| proofIrrel h1 => exact ⟨_, h1⟩
| extra h1 h2 =>
  have ⟨_, h⟩ := (envIH.2 h1).2.2.1
  exact ⟨_, (h.instL h2).weak0 henv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h : Lookup Γ✝ i✝ A✝
a✝¹ : VLevel.WF U u✝
a✝ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
Tactic:
exact hΓ.lookup henv h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
Tactic:
exact ih hΓ
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case trans
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
ih1 a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
Tactic:
exact ih1 hΓ
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case sortDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
a✝¹ : VLevel.WF U l'✝
a✝ : l✝ ≈ l'✝
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ (sort (VLevel.succ l✝)) (sort (VLevel.succ l✝)) (sort u)
Tactic:
exact ⟨_, .sortDF h1 h1 rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝⁷ : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝⁶ : List.length ls✝ = ci✝.uvars
a✝⁵ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝³ a_ih✝² : CtxStrong env U [] → ∃ u, IsDefEqStrong env U [] (sort u✝) (sort u✝) (sort u)
a_ih✝¹ a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u)
Tactic:
let ⟨_, h⟩ := envIH.1 h1
Proof state after:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝⁷ : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝⁶ : List.length ls✝ = ci✝.uvars
a✝⁵ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝³ a_ih✝² : CtxStrong env U [] → ∃ u, IsDefEqStrong env U [] (sort u✝) (sort u✝) (sort u)
a_ih✝¹ a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h : EnvStrong env ci✝.uvars ci✝.type (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u)
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝⁷ : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝⁶ : List.length ls✝ = ci✝.uvars
a✝⁵ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (sort u✝)
a_ih✝³ a_ih✝² : CtxStrong env U [] → ∃ u, IsDefEqStrong env U [] (sort u✝) (sort u✝) (sort u)
a_ih✝¹ a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h : EnvStrong env ci✝.uvars ci✝.type (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (sort u)
Tactic:
exact ⟨_, (h.1.instL h2).weak0 henv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁶ a'✝ : VExpr
a✝⁵ : VLevel.WF U u✝
a✝⁴ : VLevel.WF U v✝
a✝³ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
h4 : IsDefEqStrong env U Γ✝ a✝⁶ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a'✝) (sort v✝)
a_ih✝³ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝² : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
ih3 : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
a_ih✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort v✝) (sort v✝) (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a✝⁶) (sort u)
Tactic:
let ⟨_, ih3⟩ := ih3 hΓ
Proof state after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁶ a'✝ : VExpr
a✝⁵ : VLevel.WF U u✝
a✝⁴ : VLevel.WF U v✝
a✝³ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
h4 : IsDefEqStrong env U Γ✝ a✝⁶ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a'✝) (sort v✝)
a_ih✝³ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝² : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
ih3✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
a_ih✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort v✝) (sort v✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
ih3 : IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a✝⁶) (sort u)
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁶ a'✝ : VExpr
a✝⁵ : VLevel.WF U u✝
a✝⁴ : VLevel.WF U v✝
a✝³ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
h4 : IsDefEqStrong env U Γ✝ a✝⁶ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a'✝) (sort v✝)
a_ih✝³ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝² : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
ih3✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
a_ih✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort v✝) (sort v✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
ih3 : IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a✝⁶) (sort u)
Tactic:
have ⟨_, _, ih3⟩ := ih3.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
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁶ a'✝ : VExpr
a✝⁵ : VLevel.WF U u✝
a✝⁴ : VLevel.WF U v✝
a✝³ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
h4 : IsDefEqStrong env U Γ✝ a✝⁶ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a'✝) (sort v✝)
a_ih✝³ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝² : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
ih3✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
a_ih✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort v✝) (sort v✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝¹ : VLevel
ih3✝ : IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort w✝¹)
left✝ : ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
w✝ : VLevel
ih3 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a✝⁶) (sort u)
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁶ a'✝ : VExpr
a✝⁵ : VLevel.WF U u✝
a✝⁴ : VLevel.WF U v✝
a✝³ : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ f✝ f'✝ (forallE A✝ B✝)
h4 : IsDefEqStrong env U Γ✝ a✝⁶ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a'✝) (sort v✝)
a_ih✝³ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝² : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
ih3✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
a_ih✝¹ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
a_ih✝ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort v✝) (sort v✝) (sort u)
hΓ : CtxStrong env U Γ✝
w✝¹ : VLevel
ih3✝ : IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort w✝¹)
left✝ : ∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)
w✝ : VLevel
ih3 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort w✝)
⊢ ∃ u, IsDefEqStrong env U Γ✝ (inst B✝ a✝⁶) (inst B✝ a✝⁶) (sort u)
Tactic:
exact ⟨_, h4.hasType.1.instN henv hΓ .zero ih3 hΓ⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.isType'
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
h1 : VLevel.WF U u✝
h2 : VLevel.WF U v✝
h3 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h4 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝⁴ : CtxStrong env U Γ✝ → ∃ u, IsDefEqStrong env U Γ✝ (sort u✝) (sort u✝) (sort u)
a_ih✝³ : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
a_ih✝² : CtxStrong env U (A'✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) (sort v✝) (sort v✝) (sort u)
a_ih✝¹ : CtxStrong env U (A✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort u)
a_ih✝ : CtxStrong env U (A'✝ :: Γ✝) → ∃ u, IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (sort u)
hΓ : CtxStrong env U Γ✝
⊢ ∃ u, IsDefEqStrong env U Γ✝ (forallE A✝ B✝) (forallE A✝ B✝) (sort u)
Tactic:
exact ⟨_, .forallEDF h1 h2 h3.hasType.1 h4 h4⟩
Proof state after:
no goals