internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case forallE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
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.forallE name✝ ty✝ body✝ bi✝) dk
w✝¹ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2 : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (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.forallE name✝ ty✝ body✝ bi✝) e'
Tactic:
have htt := ht.uniq henv hΔ (ih1.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h1
Proof state after:
case forallE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
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.forallE name✝ ty✝ body✝ bi✝) dk
w✝¹ : VLevel
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
w✝ : VLevel
h2 : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (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₁
htt : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.liftN n ty₁ k) (VExpr.sort w✝¹)
⊢ ∃ e', TrExpr env Us Δ (Expr.forallE name✝ ty✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case forallE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
ty'✝ body'✝ : VExpr
Δ✝ : VLCtx
ty✝ body✝ : Expr
name✝ : Name
bi✝ : BinderInfo
h1✝¹ : IsType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝
h2✝¹ : IsType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝
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.forallE name✝ ty✝ body✝ bi✝) dk
w✝² : VLevel
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝²)
w✝¹ : VLevel
h2✝ : HasType env (List.length Us) (ty'✝ :: VLCtx.toCtx Δ✝) body'✝ (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₁
htt : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.liftN n ty₁ k) (VExpr.sort w✝²)
hΔ' :
  VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlam ty'✝) :: Δ✝)
    ((none, VLocalDecl.vlam (VExpr.liftN n ty₁ k)) :: Δ₂)
w✝ : VExpr
ih2 : TrExpr env Us ((none, VLocalDecl.vlam ty₁) :: Δ) body✝ w✝
h1' : IsDefEq env (List.length Us) (VLCtx.toCtx Δ₂) (VExpr.liftN n ty₁ k) (VExpr.liftN n ty₁ k) (VExpr.sort w✝²)
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ) ty₁ (VExpr.sort w✝²)
hΔ₂' : VLCtx.WF env (List.length Us) ((none, VLocalDecl.vlam (VExpr.liftN n ty₁ k)) :: Δ₂)
h2 : HasType env (List.length Us) (VLCtx.toCtx ((none, VLocalDecl.vlam ty₁) :: Δ)) w✝ (VExpr.sort w✝¹)
⊢ ∃ e', TrExpr env Us Δ (Expr.forallE name✝ ty✝ body✝ bi✝) e'
Tactic:
exact ⟨_, .forallE ⟨_, h1⟩ ⟨_, h2⟩ ih1 ih2⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
have hΔ₁ := hΔ.wf
Proof state after:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
have hΔ₂ := (hΔ.symm henv).wf
Proof state after:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
let ⟨ty₁, ih1⟩ := ih1 W hΔ hs.1
Proof state after:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
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.letE name✝ ty✝ val✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
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.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
let ⟨val₁, ih2⟩ := ih2 W hΔ hs.2.1
Proof state after:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
ty₁ : VExpr
ih1 : TrExpr env Us Δ ty✝ ty₁
val₁ : VExpr
ih2 : TrExpr env Us Δ val✝ val₁
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
ty₁ : VExpr
ih1 : TrExpr env Us Δ ty✝ ty₁
val₁ : VExpr
ih2 : TrExpr env Us Δ val✝ val₁
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
have hvv := hv.uniq henv hΔ (ih2.weakN henv W hΔ₂) |>.of_l henv hΔ₁.toCtx h1
Proof state after:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3 :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
ty₁ : VExpr
ih1 : TrExpr env Us Δ ty✝ ty₁
val₁ : VExpr
ih2 : TrExpr env Us Δ val✝ val₁
hvv : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ (VExpr.liftN n val₁ k) ty'✝
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case letE
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
val'✝ ty'✝ : VExpr
Δ✝ : VLCtx
ty✝ val✝ body✝ : Expr
body'✝ : VExpr
name✝ : Name
bi✝ : Bool
h1✝ : HasType env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ ty'✝
ht : TrExpr env Us Δ✝ ty✝ ty'✝
hv : TrExpr env Us Δ✝ val✝ val'✝
hb : TrExpr env Us ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) 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) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) val✝ dk → ∃ e', TrExpr env Us Δ val✝ e'
ih3✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) ((none, VLocalDecl.vlet ty'✝ val'✝) :: Δ✝) Δ₂ →
        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.letE name✝ ty✝ val✝ body✝ bi✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
ty₁ : VExpr
ih1 : TrExpr env Us Δ ty✝ ty₁
val₁ : VExpr
ih2 : TrExpr env Us Δ val✝ val₁
hvv : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) val'✝ (VExpr.liftN n val₁ k) ty'✝
w✝¹ : VLevel
h2 : HasType env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.sort w✝¹)
htt : IsDefEq env (List.length Us) (VLCtx.toCtx Δ✝) ty'✝ (VExpr.liftN n ty₁ k) (VExpr.sort w✝¹)
w✝ : VExpr
ih3 : TrExpr env Us ((none, VLocalDecl.vlet ty₁ val₁) :: Δ) body✝ w✝
h1 : HasType env (List.length Us) (VLCtx.toCtx Δ) val₁ ty₁
⊢ ∃ e', TrExpr env Us Δ (Expr.letE name✝ ty✝ val✝ body✝ bi✝) e'
Tactic:
exact ⟨_, .letE h1 ih1 ih2 ih3⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lit
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) (Literal.toConstructor l✝) dk →
          ∃ e', TrExpr env Us Δ (Literal.toConstructor l✝) 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.lit l✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.lit l✝) e'
Tactic:
let ⟨_, ih⟩ := ih W hΔ .toConstructor
Proof state after:
case lit
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) (Literal.toConstructor l✝) dk →
          ∃ e', TrExpr env Us Δ (Literal.toConstructor l✝) 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.lit l✝) dk
w✝ : VExpr
ih : TrExpr env Us Δ (Literal.toConstructor l✝) w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.lit l✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case lit
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : VExpr
l✝ : Literal
a✝ : TrExpr env Us Δ✝ (Literal.toConstructor l✝) e✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) (Literal.toConstructor l✝) dk →
          ∃ e', TrExpr env Us Δ (Literal.toConstructor l✝) 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.lit l✝) dk
w✝ : VExpr
ih : TrExpr env Us Δ (Literal.toConstructor l✝) w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.lit l✝) e'
Tactic:
exact ⟨_, .lit ih⟩
Proof state after:
no goals