internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have h1 := h1.defeqU_l henv hΔ₁.toCtx <| hf.uniq henv hΔ (ih1.weakN henv W hΔ₂)
Proof state after:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have h2 := h2.defeqU_l henv hΔ₁.toCtx <| ha.uniq henv hΔ (ih2.weakN henv W hΔ₂)
Proof state after:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have := VExpr.WF.weakN_iff henv hΔ₂.toCtx W.toCtx (e := f₁.app a₁)
Proof state after:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
this :
  VExpr.WF env (List.length Us) (VLCtx.toCtx Δ₂) (VExpr.liftN n (VExpr.app f₁ a₁) k) ↔
    VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
this :
  VExpr.WF env (List.length Us) (VLCtx.toCtx Δ₂) (VExpr.liftN n (VExpr.app f₁ a₁) k) ↔
    VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have := this.1 ⟨_, (h1.app h2).defeqDFC henv hΔ.defeqCtx⟩
Proof state after:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
this✝ :
  VExpr.WF env (List.length Us) (VLCtx.toCtx Δ₂) (VExpr.liftN n (VExpr.app f₁ a₁) k) ↔
    VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
this : VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case app
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
f'✝ A✝ B✝ a'✝ : VExpr
Δ✝ : VLCtx
f✝ a✝ : Expr
h1✝¹ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) f'✝ (VExpr.forallE A✝ B✝)
h2✝¹ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) a'✝ A✝
hf : TrExpr env Us Δ✝ f✝ f'✝
ha : TrExpr env Us Δ✝ a✝ a'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) f✝ dk → ∃ e', TrExpr env Us Δ f✝ e'
ih2✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) a✝ dk → ∃ e', TrExpr env Us Δ a✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.app f✝ a✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
f₁ : VExpr
ih1 : TrExpr env Us Δ f✝ f₁
a₁ : VExpr
ih2 : TrExpr env Us Δ a✝ a₁
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n f₁ k) (VExpr.forallE A✝ B✝)
h2✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) (VExpr.liftN n a₁ k) A✝
this✝ :
  VExpr.WF env (List.length Us) (VLCtx.toCtx Δ₂) (VExpr.liftN n (VExpr.app f₁ a₁) k) ↔
    VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
this : VExpr.WF env (List.length Us) (VLCtx.toCtx Δ) (VExpr.app f₁ a₁)
w✝¹ w✝ : VExpr
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ) f₁ (VExpr.forallE w✝¹ w✝)
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ) a₁ w✝¹
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
exact ⟨_, .app h1 h2 ih1 ih2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1 : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Tactic:
let ⟨_, h1⟩ := h1
Proof state after:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Tactic:
have hΔ₁ := hΔ.wf
Proof state after:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Tactic:
have hΔ₂ := (hΔ.symm henv).wf
Proof state after:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'
Tactic:
let ⟨ty₁, ih1⟩ := ih1 W hΔ hs.1
Proof state after:
case lam
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hb : TrExpr env Us ((none, VLocalDecl.vlam ty'✝) :: Δ✝) body✝ body'✝
ih1✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) ty✝ dk → ∃ e', TrExpr env Us Δ ty✝ e'
ih2 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝) Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) body✝ dk → ∃ e', TrExpr env Us Δ body✝ e'
Δ Δ₂ : VLCtx
dk k : Nat
W : VLCtx.LiftN Δ Δ₂ dk n k
hΔ : VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂
hs : InScope (fun x => x ∈ VLCtx.fvars Δ) (Expr.lam name✝ ty✝ body✝ bi✝) dk
w✝ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝)
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
ty₁ : VExpr
ih1 : TrExpr env Us Δ ty✝ ty₁
⊢ ∃ e', TrExpr env Us Δ (Expr.lam name✝ ty✝ body✝ bi✝) e'