internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case proofIrrel.inr
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
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
h1 : IsDefEq env U Γ✝ h✝ h✝ p✝
h2 : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝ : ∀ {A B : VExpr}, p✝ = VExpr.forallE A B ∨ p✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih1 : ∀ {A B : VExpr}, h✝ = VExpr.forallE A B ∨ h✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, h'✝ = VExpr.forallE A B ∨ h'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : h'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 (.inr eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case forallEDF
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'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
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 : VExpr.forallE A✝ body✝ = VExpr.forallE A B ∨ VExpr.forallE A'✝ body'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq
Proof state after:
case forallEDF.inl.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
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
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
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) body✝

case forallEDF.inr.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
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
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
⊢ IsType env U Γ✝ A'✝ ∧ IsType env U (A'✝ :: Γ✝) body'✝
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case forallEDF.inl.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
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
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
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) body✝
Tactic:
exact ⟨⟨_, h1.hasType.1⟩, _, h2.hasType.1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case forallEDF.inr.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
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
h2 : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
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
⊢ IsType env U Γ✝ A'✝ ∧ IsType env U (A'✝ :: Γ✝) body'✝
Tactic:
exact ⟨⟨_, h1.hasType.2⟩, _, h2.hasType.2.defeq_l henv h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case defeqDF
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✝ 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 B : VExpr}, A✝ = VExpr.forallE A B ∨ B✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e1✝ = VExpr.forallE A B ∨ e2✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e1✝ = VExpr.forallE A B ∨ e2✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta
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 A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : app (lam A✝ e) e'✝ = VExpr.forallE A B ∨ inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case beta.inr
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 A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr
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 A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 :
  ∀ {A B : VExpr},
    e = VExpr.forallE A B ∨ e = VExpr.forallE A B → IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : inst e e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases e with
| bvar i =>
  cases i with simp [inst] at eq
  | zero => exact ih2 (.inl eq)
| forallE A B =>
  cases eq
  let ⟨A1, A2⟩ := ih1 (.inl rfl)
  exact ⟨A1.instN henv .zero h2, A2.instN henv (.succ .zero) h2⟩
| _ => cases eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.bvar
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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
i : Nat
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar i) (VExpr.bvar i) B✝
ih1 :
  ∀ {A B : VExpr},
    VExpr.bvar i = VExpr.forallE A B ∨ VExpr.bvar i = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : inst (VExpr.bvar i) e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases i with simp [inst] at eq
| zero => exact ih2 (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.bvar.zero
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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar Nat.zero) (VExpr.bvar Nat.zero) B✝
ih1 :
  ∀ {A B : VExpr},
    VExpr.bvar Nat.zero = VExpr.forallE A B ∨ VExpr.bvar Nat.zero = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih2 (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.forallE
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 A✝¹ : VExpr
Γ✝ : List VExpr
B✝¹ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝¹
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A✝ B✝ A B : VExpr
h1 : IsDefEq env U (A✝¹ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝¹
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝¹ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝¹ :: Γ✝) B_1
eq : inst (VExpr.forallE A B) e'✝ = VExpr.forallE A✝ B✝
⊢ IsType env U Γ✝ A✝ ∧ IsType env U (A✝ :: Γ✝) B✝
Tactic:
cases eq
Proof state after:
case beta.inr.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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Tactic:
let ⟨A1, A2⟩ := ih1 (.inl rfl)
Proof state after:
case beta.inr.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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
A1 : IsType env U (A✝ :: Γ✝) A
A2 : IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE A B) (VExpr.forallE A B) B✝
ih1 :
  ∀ {A_1 B_1 : VExpr},
    VExpr.forallE A B = VExpr.forallE A_1 B_1 ∨ VExpr.forallE A B = VExpr.forallE A_1 B_1 →
      IsType env U (A✝ :: Γ✝) A_1 ∧ IsType env U (A_1 :: A✝ :: Γ✝) B_1
A1 : IsType env U (A✝ :: Γ✝) A
A2 : IsType env U (A :: A✝ :: Γ✝) B
⊢ IsType env U Γ✝ (inst A e'✝) ∧ IsType env U (inst A e'✝ :: Γ✝) (inst B e'✝ (0 + 1))
Tactic:
exact ⟨A1.instN henv .zero h2, A2.instN henv (.succ .zero) h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case beta.inr.lam
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 A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : ∀ {A B : VExpr}, e'✝ = VExpr.forallE A B ∨ e'✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B binderType✝ body✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (lam binderType✝ body✝) (lam binderType✝ body✝) B✝
ih1 :
  ∀ {A B : VExpr},
    lam binderType✝ body✝ = VExpr.forallE A B ∨ lam binderType✝ body✝ = VExpr.forallE A B →
      IsType env U (A✝ :: Γ✝) A ∧ IsType env U (A :: A✝ :: Γ✝) B
eq : inst (lam binderType✝ body✝) e'✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
cases eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case eta
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
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case eta.inr
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
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case eta.inr
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
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : ∀ {A B : VExpr}, e✝ = VExpr.forallE A B ∨ e✝ = VExpr.forallE A B → IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
A B : VExpr
eq : e✝ = VExpr.forallE A B
⊢ IsType env U Γ✝ A ∧ IsType env U (A :: Γ✝) B
Tactic:
exact ih (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra
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
⊢ IsType env U Γ A ∧ IsType env U (A :: Γ) B
Tactic:
suffices ∀ e, VExpr.instL ls e = VExpr.forallE A B →
    (∀ A B, 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 by
  have ⟨A1, A2⟩ := envIH.2 h1
  cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
case extra
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
⊢ ∀ (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
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra
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
⊢ ∀ (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
Tactic:
intro e eq IH
Proof state after:
case extra
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
e : VExpr
eq : VExpr.instL ls e = VExpr.forallE A B
IH : ∀ (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
Theorem: Lean4Lean.VEnv.IsDefEq.forallE_inv'
Proof state before:
case extra
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
e : VExpr
eq : VExpr.instL ls e = VExpr.forallE A B
IH : ∀ (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
Tactic:
cases e <;> cases eq
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
binderType✝ body✝ : VExpr
IH :
  ∀ (A B : VExpr),
    VExpr.forallE binderType✝ body✝ = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ IsType env U Γ (VExpr.instL ls binderType✝) ∧ IsType env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝)
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
binderType✝ body✝ : VExpr
IH :
  ∀ (A B : VExpr),
    VExpr.forallE binderType✝ body✝ = VExpr.forallE A B → IsType env df.uvars [] A ∧ IsType env df.uvars [A] B
eq :
  VExpr.instL ls df.lhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝) ∨
    VExpr.instL ls df.rhs = VExpr.forallE (VExpr.instL ls binderType✝) (VExpr.instL ls body✝)
⊢ IsType env U Γ (VExpr.instL ls binderType✝) ∧ IsType env U (VExpr.instL ls binderType✝ :: Γ) (VExpr.instL ls body✝)
Tactic:
rename_i A B
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)
⊢ IsType env U Γ (VExpr.instL ls A) ∧ IsType env U (VExpr.instL ls A :: Γ) (VExpr.instL ls B)