internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case proofIrrel
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
a✝¹ : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
ih1 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ → IsDefEqStrong env U Γ (inst p✝ e₀ k) (inst p✝ e₀ k) (inst (sort VLevel.zero) e₀ k)
ih2 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst h✝ e₀ k) (inst h✝ e₀ k) (inst p✝ e₀ k)
ih3 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ → CtxStrong env U Γ → IsDefEqStrong env U Γ (inst h'✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
⊢ IsDefEqStrong env U Γ (inst h✝ e₀ k) (inst h'✝ e₀ k) (inst p✝ e₀ k)
Tactic:
exact .proofIrrel (ih1 W hΓ) (ih2 W hΓ) (ih3 W hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.instN
Proof state before:
case extra
env : VEnv
U : Nat
Γ₀ : List VExpr
e₀ A₀ : VExpr
henv : Ordered env
h₀ : IsDefEqStrong env U Γ₀ e₀ e₀ A₀
hΓ₀ : CtxStrong env U Γ₀
Γ₁ : List VExpr
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
h4 : VLevel.WF U u✝
h5 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (sort u✝)
h6 : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
h7 : 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✝² :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.type) e₀ k) (inst (VExpr.instL ls✝ df✝.type) e₀ k)
          (inst (sort u✝) e₀ k)
a_ih✝¹ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.lhs) e₀ k) (inst (VExpr.instL ls✝ df✝.lhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
a_ih✝ :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k [] Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (inst (VExpr.instL ls✝ df✝.rhs) e₀ k) (inst (VExpr.instL ls✝ df✝.rhs) e₀ k)
          (inst (VExpr.instL ls✝ df✝.type) e₀ k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ
hΓ : CtxStrong env U Γ
hA1 : ClosedN df✝.lhs
right✝ : ClosedN df✝.type
hA2 : ClosedN df✝.rhs
hA3 : ClosedN df✝.type
ih4 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
ih5 :
  ∀ {k : Nat} {Γ : List VExpr},
    Ctx.InstN Γ₀ e₀ A₀ k Γ✝ Γ →
      CtxStrong env U Γ →
        IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
⊢ IsDefEqStrong env U Γ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3 h4 h5 h6 h7 (ih4 W hΓ) (ih5 W hΓ)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.defeqDF_l
Proof state before:
env : VEnv
U : Nat
Γ : List VExpr
A A' : VExpr
u : VLevel
e1 e2 B : VExpr
henv : Ordered env
hΓ : CtxStrong env U Γ
h1 : IsDefEqStrong env U Γ A A' (sort u)
h2 : IsDefEqStrong env U (A :: Γ) e1 e2 B
⊢ IsDefEqStrong env U (A' :: Γ) e1 e2 B
Tactic:
simpa [instN_bvar0] using
  have hu := h1.defeq.sort_r henv hΓ.defeq
  have hΓ' := ⟨hΓ, _, h1.hasType.2⟩
  h1.weakN henv (.one (A := A'))
    |>.symm.defeqDF hu (.bvar .zero hu (h1.hasType.2.weakN henv .one))
    |>.instN henv hΓ' .zero (h2.weakN henv (.succ (.one (A := A')))) hΓ'
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e'✝ = 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 : e'✝ = forallE A B ∨ e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih hΓ eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case proofIrrel.inl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = 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 : h✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih1 hΓ (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case proofIrrel.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ p✝ p✝ (sort VLevel.zero)
h1 : IsDefEqStrong env U Γ✝ h✝ h✝ p✝
h2 : IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      p✝ = forallE A B ∨ p✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih1 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h✝ = forallE A B ∨ h✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      h'✝ = forallE A B ∨ h'✝ = 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 : h'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih2 hΓ (.inr eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case forallEDF.inl.refl
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
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
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✝ :: Γ✝) →
      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)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A✝ A✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A✝ :: Γ✝) body✝ body✝ (sort v)
Tactic:
exact ⟨⟨_, h1.hasType.1⟩, _, h2.hasType.1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case forallEDF.inr.refl
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
body✝ body'✝ : VExpr
v✝ : VLevel
a✝² : VLevel.WF U u✝
a✝¹ : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (sort v✝)
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✝ :: Γ✝) →
      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)
hΓ : CtxStrong env U Γ✝
⊢ (∃ u, IsDefEqStrong env U Γ✝ A'✝ A'✝ (sort u)) ∧ ∃ v, IsDefEqStrong env U (A'✝ :: Γ✝) body'✝ body'✝ (sort v)
Tactic:
exact ⟨⟨_, h1.hasType.2⟩, _, h1.defeqDF_l henv hΓ h2.hasType.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case defeqDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
a_ih✝ :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      A✝ = forallE A B ∨ B✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
ih2 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e1✝ = forallE A B ∨ e2✝ = 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 : e1✝ = forallE A B ∨ e2✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih2 hΓ eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h3 : IsDefEqStrong env U (A✝ :: Γ✝) e e B✝
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e e'✝) (inst e e'✝) (inst B✝ e'✝)
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)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      e = forallE A B ∨ e = forallE A B →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort v)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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 Γ✝ →
      inst e e'✝ = forallE A B ∨ inst e e'✝ = 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 : inst e e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases e with
| bvar i =>
  cases i with simp [inst] at eq
  | zero => exact ih4 hΓ (.inl eq)
| forallE A B =>
  cases eq
  let ⟨⟨_, A1⟩, _, A2⟩ := ih3 ⟨hΓ, _, h1⟩ (.inl rfl)
  refine ⟨⟨_, h4.instN henv hΓ .zero A1 hΓ⟩, _, h4.instN henv hΓ (.succ .zero) A2 ?_⟩
  exact ⟨hΓ, _, h4.instN henv hΓ .zero A1 hΓ⟩
| _ => cases eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr.bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
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)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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 Γ✝
i : Nat
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (VExpr.bvar i) (VExpr.bvar i) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (VExpr.bvar i) e'✝) (inst (VExpr.bvar i) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      VExpr.bvar i = forallE A B ∨ VExpr.bvar i = 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 Γ✝ →
      inst (VExpr.bvar i) e'✝ = forallE A B ∨ inst (VExpr.bvar i) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : inst (VExpr.bvar i) e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases i with simp [inst] at eq
| zero => exact ih4 hΓ (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr.bvar.zero
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
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)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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 Γ✝
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (VExpr.bvar Nat.zero) (VExpr.bvar Nat.zero) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (VExpr.bvar Nat.zero) e'✝) (inst (VExpr.bvar Nat.zero) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      VExpr.bvar Nat.zero = forallE A B ∨ VExpr.bvar Nat.zero = 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 Γ✝ →
      inst (VExpr.bvar Nat.zero) e'✝ = forallE A B ∨ inst (VExpr.bvar Nat.zero) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih4 hΓ (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr.forallE.refl
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
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)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (forallE A B) (forallE A B) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (forallE A B) e'✝) (inst (forallE A B) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      forallE A B = forallE A_1 B_1 ∨ forallE A B = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U (A✝ :: Γ✝) A_1 A_1 (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A_1 :: A✝ :: Γ✝) B_1 B_1 (sort v)
a_ih✝ :
  ∀ {A_1 B_1 : VExpr},
    CtxStrong env U Γ✝ →
      inst (forallE A B) e'✝ = forallE A_1 B_1 ∨ inst (forallE A B) e'✝ = forallE A_1 B_1 →
        (∃ u, IsDefEqStrong env U Γ✝ A_1 A_1 (sort u)) ∧ ∃ v, IsDefEqStrong env U (A_1 :: Γ✝) B_1 B_1 (sort v)
w✝¹ : VLevel
A1 : IsDefEqStrong env U (A✝ :: Γ✝) A A (sort w✝¹)
w✝ : VLevel
A2 : IsDefEqStrong env U (A :: A✝ :: Γ✝) B B (sort w✝)
⊢ CtxStrong env U (inst A e'✝ :: Γ✝)
Tactic:
exact ⟨hΓ, _, h4.instN henv hΓ .zero A1 hΓ⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case beta.inr.lam
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e'✝ : VExpr
hu : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A✝ (sort u✝)
h2 : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (sort v✝)
h4 : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (sort v✝)
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)
ih4 :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e'✝ = forallE A B ∨ e'✝ = 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 Γ✝ →
      inst B✝ e'✝ = forallE A B ∨ inst B✝ e'✝ = 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 Γ✝
binderType✝ body✝ : VExpr
h3 : IsDefEqStrong env U (A✝ :: Γ✝) (lam binderType✝ body✝) (lam binderType✝ body✝) B✝
a✝ : IsDefEqStrong env U Γ✝ (inst (lam binderType✝ body✝) e'✝) (inst (lam binderType✝ body✝) e'✝) (inst B✝ e'✝)
ih3 :
  ∀ {A B : VExpr},
    CtxStrong env U (A✝ :: Γ✝) →
      lam binderType✝ body✝ = forallE A B ∨ lam binderType✝ 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 Γ✝ →
      inst (lam binderType✝ body✝) e'✝ = forallE A B ∨ inst (lam binderType✝ body✝) e'✝ = forallE A B →
        (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
eq : inst (lam binderType✝ body✝) e'✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
cases eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEqStrong.forallE_inv'
Proof state before:
case eta.inr
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : 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 (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (forallE (lift A✝) (liftN 1 B✝ 1))
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 (lift A✝ :: A✝ :: Γ✝) →
      liftN 1 B✝ 1 = forallE A B ∨ liftN 1 B✝ 1 = forallE A B →
        (∃ u, IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) A A (sort u)) ∧
          ∃ v, IsDefEqStrong env U (A :: lift A✝ :: A✝ :: Γ✝) B B (sort v)
ih :
  ∀ {A B : VExpr},
    CtxStrong env U Γ✝ →
      e✝ = forallE A B ∨ e✝ = 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✝ :: Γ✝) →
      lift e✝ = forallE A B ∨ lift e✝ = 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 : e✝ = forallE A B
⊢ (∃ u, IsDefEqStrong env U Γ✝ A A (sort u)) ∧ ∃ v, IsDefEqStrong env U (A :: Γ✝) B B (sort v)
Tactic:
exact ih hΓ (.inl eq)
Proof state after:
no goals