internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨e'', he⟩ := TrExpr.weakN_inv henv W (.refl henv hΔ) h2 H4
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
⊢ TrHasType env Us Δ e A
Tactic:
have ee := h2.uniq henv (.refl henv hΔ) <| he.weakN henv W hΔ
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
⊢ TrHasType env Us Δ e A
Tactic:
have ⟨_, hA⟩ := TrExpr.weakN_inv henv W (.refl henv hΔ) h3 <| h1 _ this H4
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
⊢ TrHasType env Us Δ e A
Tactic:
have AA := h3.uniq henv (.refl henv hΔ) <| hA.weakN henv W hΔ
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4 : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Tactic:
have h4 := h4.defeqU_r henv hΔ.toCtx AA |>.defeqU_l henv hΔ.toCtx ee
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
⊢ TrHasType env Us Δ e A
Tactic:
have h4 := (HasType.weakN_iff henv hΔ.toCtx W.toCtx).1 h4
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
⊢ TrHasType env Us Δ e A
Theorem: Lean4Lean.ConditionallyHasType.weakN_inv
Proof state before:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
⊢ TrHasType env Us Δ e A
Tactic:
refine ⟨fun P hP he' => ?_, _, _, he, hA, h4⟩
Proof state after:
env : VEnv
fv : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some fv, d) :: Δ)
H : ConditionallyHasType ngen env Us ((some fv, d) :: Δ) e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars ((some fv, d) :: Δ)) e → TrHasType env Us ((some fv, d) :: Δ) e A
H4 : InScope (fun x => x ∈ VLCtx.fvars Δ) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P ((some fv, d) :: Δ) → InScope P e → InScope P A
e' A' : VExpr
h2 : TrExpr env Us ((some fv, d) :: Δ) e e'
h3 : TrExpr env Us ((some fv, d) :: Δ) A A'
h4✝¹ : HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' A'
W : VLCtx.LiftN Δ ((some fv, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
e'' : VExpr
he : TrExpr env Us Δ e e''
ee : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) e' (VExpr.liftN (0 + VLocalDecl.depth d) e'')
this : IsFVarUpSet (fun x => x ∈ VLCtx.fvars Δ) ((some fv, d) :: Δ)
w✝ : VExpr
hA : TrExpr env Us Δ A w✝
AA : IsDefEqU env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) A' (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4✝ :
  HasType env (List.length Us) (VLCtx.toCtx ((some fv, d) :: Δ)) (VExpr.liftN (0 + VLocalDecl.depth d) e'')
    (VExpr.liftN (0 + VLocalDecl.depth d) w✝)
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) e'' w✝
P : FVarId → Prop
hP : IsFVarUpSet P Δ
he' : InScope P e
⊢ InScope P A
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
⊢ ConditionallyHasType ngen env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
refine have ⟨H1, H2, H3⟩ := H; ⟨H1, H2, fun H4 => ?_⟩
Proof state after:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
have ⟨h1, _, _, h2, h3, h4⟩ := H3 (H4.mp ?_ H1)
Proof state after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A

case refine_1
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
⊢ ∀ (fv : FVarId),
    fv ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ) →
      NameGenerator.Reserves ngen fv → fv ∈ VLCtx.fvars Δ
Theorem: Lean4Lean.ConditionallyHasType.fresh
Proof state before:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A
Tactic:
have W : VLCtx.LiftN Δ ((some ⟨ngen.curr⟩, d) :: Δ) 0 (0 + d.depth) 0 := .skip_fvar _ _ .refl
Proof state after:
case refine_2
env : VEnv
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
ngen : NameGenerator
Us : List Name
e A : Expr
henv : Ordered env
hΔ : VLCtx.WF env (List.length Us) ((some { name := NameGenerator.curr ngen }, d) :: Δ)
H : ConditionallyHasType ngen env Us Δ e A
H1 : InScope (NameGenerator.Reserves ngen) e
H2 : InScope (NameGenerator.Reserves ngen) A
H3 : InScope (fun x => x ∈ VLCtx.fvars Δ) e → TrHasType env Us Δ e A
H4 : InScope (fun x => x ∈ VLCtx.fvars ((some { name := NameGenerator.curr ngen }, d) :: Δ)) e
h1 : ∀ (P : FVarId → Prop), IsFVarUpSet P Δ → InScope P e → InScope P A
w✝¹ w✝ : VExpr
h2 : TrExpr env Us Δ e w✝¹
h3 : TrExpr env Us Δ A w✝
h4 : HasType env (List.length Us) (VLCtx.toCtx Δ) w✝¹ w✝
W : VLCtx.LiftN Δ ((some { name := NameGenerator.curr ngen }, d) :: Δ) 0 (0 + VLocalDecl.depth d) 0
⊢ TrHasType env Us ((some { name := NameGenerator.curr ngen }, d) :: Δ) e A