internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)
Tactic:
let ⟨⟨_, A1⟩, v, A2⟩ := IH _ _ rfl
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)
Tactic:
refine ⟨⟨_, (A1.instL h2).weak0 henv⟩, v.inst ls, ?_⟩
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have := (A2.instL h2).weakN henv (.succ (.zero Γ))
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have C1 := (A1.instL h2).closedN henv ⟨⟩
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.sort v)) (0 + 1))
C1 : ClosedN (VExpr.instL ls A) (List.length (List.map (VExpr.instL ls) []))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
have C2 := (A2.instL h2).closedN henv ⟨⟨⟩, C1⟩
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.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]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (liftN (List.length Γ) (VExpr.instL ls A) :: (Γ ++ List.map (VExpr.instL ls) []))
    (liftN (List.length Γ) (VExpr.instL ls B) (0 + 1)) (liftN (List.length Γ) (VExpr.instL ls (VExpr.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]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
rw [C1.liftN_eq (Nat.zero_le _), C2.liftN_eq (by exact Nat.le_refl _)] at this
Proof state after:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (VExpr.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]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType env U (VExpr.instL ls A :: (Γ ++ List.map (VExpr.instL ls) [])) (VExpr.instL ls B)
    (liftN (List.length Γ) (VExpr.instL ls (VExpr.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]))
⊢ HasType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B) (VExpr.sort (VLevel.inst ls v))
Tactic:
simpa [liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
have ⟨A1, A2⟩ := envIH.2 h1
Proof state after:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
A1 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.lhs df.type
A2 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.rhs df.type
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
eq : VExpr.instL ls df.lhs = VExpr.forallE A B ∨ VExpr.instL ls df.rhs = VExpr.forallE A B
this :
  ∀ (e : VExpr),
    VExpr.instL ls e = VExpr.forallE A B →
      (∀ (A B : VExpr), e = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B) →
        IsType env U Γ A ∧ IsType env U (A :: Γ) B
A1 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.lhs df.type
A2 :
  (fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B) df.uvars df.rhs df.type
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ✝ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
A B : VExpr
IH :
  ∀ (A_1 B_1 : VExpr),
    VExpr.forallE A B = VExpr.forallE A_1 B_1 → IsType env df.uvars [] A_1 ∧ IsType env df.uvars [A_1] B_1
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls A) (VExpr.instL ls B)
w✝ : VLevel
A1 : HasType env df.uvars [] A (VExpr.sort w✝)
v : VLevel
A2 : HasType env df.uvars [A] B (VExpr.sort v)
this :
  HasType 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 (VExpr.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.IsDefEq.forallE_inv'
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e x => ∀ (A B : VExpr), e = VExpr.forallE A B → IsType env U [] A ∧ IsType env U [A] B
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝¹ :
  ∀ {A B : VExpr}, A✝ = VExpr.forallE A B ∨ A'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
a_ih✝ :
  ∀ {A B : VExpr},
    body✝ = VExpr.forallE A B ∨ body'✝ = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
A B : VExpr
eq : lam A✝ body✝ = VExpr.forallE A B ∨ lam A'✝ body'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.HasType.forallE_inv
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
refine H.forallE_inv' henv ?_ (.inl rfl)
Proof state after:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ OnTypes env fun U e x => ∀ (A B : VExpr), e = forallE A B → IsType env U [] A ∧ IsType env U [A] B
Theorem: Lean4Lean.VEnv.HasType.forallE_inv
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
V A B : VExpr
henv : Ordered env
H : HasType env U Γ (forallE A B) V
⊢ OnTypes env fun U e x => ∀ (A B : VExpr), e = forallE A B → IsType env U [] A ∧ IsType env U [A] B
Tactic:
exact henv.induction
  (fun env U e _ => ∀ A B, e = forallE A B → IsType env U [] A ∧ IsType env U [A] B)
  (fun le H A B eq => (H A B eq).imp (.mono le) (.mono le))
  (fun henv IH H A B eq => H.forallE_inv' henv IH (.inl eq))
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
H : IsDefEq env U Γ e1 e2 V
eq : e1 = VExpr.sort u ∨ e2 = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
induction H with
| symm _ ih => exact ih eq.symm
| trans _ _ ih1 ih2
| proofIrrel _ _ _ _ ih1 ih2 =>
  obtain eq | eq := eq <;> [exact ih1 (.inl eq); exact ih2 (.inr eq)]
| sortDF => obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq <;> assumption
| defeqDF _ _ _ ih2 => exact ih2 eq
| @beta _ _ e _ _ h1 _ ih1 ih2 =>
  obtain ⟨⟨⟩⟩ | eq := eq
  cases e with
  | bvar i =>
    cases i with simp [inst] at eq
    | zero => exact ih2 (.inl eq)
  | _ => cases eq <;> exact ih1 (.inl rfl)
| eta _ ih =>
  obtain ⟨⟨⟩⟩ | eq := eq
  exact ih (.inl eq)
| @extra df ls _ h1 h2 =>
  suffices ∀ e, VExpr.instL ls e = .sort u → HasType env df.uvars [] e df.type → u.WF U by
    have ⟨A1, A2⟩ := henv.defEqWF h1
    cases eq <;> exact this _ ‹_› ‹_›
  intro e eq IH
  cases e <;> cases eq; rename_i u
  exact VLevel.WF.inst h2
| _ => nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case symm
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : e✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
eq : e'✝ = VExpr.sort u ∨ e✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
exact ih eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : 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✝
a_ih✝ : p✝ = VExpr.sort u ∨ p✝ = VExpr.sort u → VLevel.WF U u
ih1 : h✝ = VExpr.sort u ∨ h✝ = VExpr.sort u → VLevel.WF U u
ih2 : h'✝ = VExpr.sort u ∨ h'✝ = VExpr.sort u → VLevel.WF U u
eq : h✝ = VExpr.sort u ∨ h'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
obtain eq | eq := eq <;> [exact ih1 (.inl eq); exact ih2 (.inr eq)]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case sortDF
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u l✝ l'✝ : VLevel
Γ✝ : List VExpr
a✝² : VLevel.WF U l✝
a✝¹ : VLevel.WF U l'✝
a✝ : l✝ ≈ l'✝
eq : VExpr.sort l✝ = VExpr.sort u ∨ VExpr.sort l'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq <;> assumption
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case defeqDF
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
a_ih✝ : A✝ = VExpr.sort u ∨ B✝ = VExpr.sort u → VLevel.WF U u
ih2 : e1✝ = VExpr.sort u ∨ e2✝ = VExpr.sort u → VLevel.WF U u
eq : e1✝ = VExpr.sort u ∨ e2✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
exact ih2 eq
Proof state after:
no goals