internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case mdata
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.mdata d✝ e✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.mdata d✝ e✝) e'
Tactic:
let ⟨_, ih⟩ := ih W hΔ hs
Proof state after:
case mdata
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.mdata d✝ e✝) dk
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.mdata d✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case mdata
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
d✝ : MData
a✝ : TrExpr env Us Δ✝ e✝ e'✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.mdata d✝ e✝) dk
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.mdata d✝ e✝) e'
Tactic:
exact ⟨_, .mdata ih⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
have hΔ₁ := hΔ.wf
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
have hΔ₂ := (hΔ.symm henv).wf
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
let ⟨_, ih⟩ := ih W hΔ hs
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
have htt := h1.uniq henv hΔ (ih.weakN henv W hΔ₂)
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝ k)
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2 : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝ : VExpr
ih : TrExpr env Us Δ e✝ w✝
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝ k)
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
have ⟨_, h2⟩ := h2.defeqDFC henv hΔ.defeqCtx htt
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2✝ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝¹ : VExpr
ih : TrExpr env Us Δ e✝ w✝¹
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝¹ k)
w✝ : VExpr
h2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ (VExpr.liftN n w✝¹ k) w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2✝ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝¹ : VExpr
ih : TrExpr env Us Δ e✝ w✝¹
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝¹ k)
w✝ : VExpr
h2 : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ (VExpr.liftN n w✝¹ k) w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
have ⟨_, h2⟩ := h2.weakN_inv henv hΔ₂.toCtx W.toCtx
Proof state after:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2✝¹ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝² : VExpr
ih : TrExpr env Us Δ e✝ w✝²
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝² k)
w✝¹ : VExpr
h2✝ : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ (VExpr.liftN n w✝² k) w✝¹
w✝ : VExpr
h2 : TrProj (VLCtx.toCtx Δ) s✝ i✝ w✝² w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case proj
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
Δ✝ : VLCtx
e✝ : Expr
e'✝ : VExpr
s✝ : Name
i✝ : Nat
e''✝ : VExpr
h1 : TrExpr env Us Δ✝ e✝ e'✝
h2✝¹ : TrProj (VLCtx.toCtx Δ✝) s✝ i✝ e'✝ e''✝
ih✝ :
  ∀ {Δ Δ₂ : VLCtx} {dk k : Nat},
    VLCtx.LiftN Δ Δ₂ dk n k →
      VLCtx.IsDefEq env (List.length Us) Δ✝ Δ₂ →
        InScope (fun x => x ∈ VLCtx.fvars Δ) e✝ dk → ∃ e', TrExpr env Us Δ e✝ 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.proj s✝ i✝ e✝) dk
hΔ₁ : VLCtx.WF env (List.length Us) Δ✝
hΔ₂ : VLCtx.WF env (List.length Us) Δ₂
w✝² : VExpr
ih : TrExpr env Us Δ e✝ w✝²
htt : IsDefEqU env (List.length Us) (VLCtx.toCtx Δ✝) e'✝ (VExpr.liftN n w✝² k)
w✝¹ : VExpr
h2✝ : TrProj (VLCtx.toCtx Δ₂) s✝ i✝ (VExpr.liftN n w✝² k) w✝¹
w✝ : VExpr
h2 : TrProj (VLCtx.toCtx Δ) s✝ i✝ w✝² w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.proj s✝ i✝ e✝) e'
Tactic:
exact ⟨_, .proj ih h2⟩
Proof state after:
no goals
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ IsFVarUpSet P ((some fv, d) :: Δ) ↔ IsFVarUpSet Q ((some fv, d) :: Δ)
Tactic:
refine and_congr (imp_congr (H _ (.head _)) ?_) (congr fun fv h => H _ (.tail _ h))
Proof state after:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d ↔
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d ↔
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Tactic:
apply iff_of_eq
Proof state after:
case a
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d =
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
case a
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) d =
    VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv) d
Tactic:
congr
Proof state after:
case a.e_P
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) = fun i =>
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
case a.e_P
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
⊢ (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) = fun i =>
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
funext i
Proof state after:
case a.e_P.h
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
i : Nat
⊢ (∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) =
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
case a.e_P.h
P Q : FVarId → Prop
fv : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv_1 : FVarId), fv_1 ∈ VLCtx.fvars ((some fv, d) :: Δ) → (P fv_1 ↔ Q fv_1)
i : Nat
⊢ (∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → P fv) =
    ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
refine forall_congr fun fv => propext ?_
Proof state after:
case a.e_P.h
P Q : FVarId → Prop
fv✝ : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv : FVarId), fv ∈ VLCtx.fvars ((some fv✝, d) :: Δ) → (P fv ↔ Q fv)
i : Nat
fv : FVarId
⊢ VLCtx.vlamName Δ i = some (some fv) → P fv ↔ VLCtx.vlamName Δ i = some (some fv) → Q fv
Theorem: Lean4Lean.IsFVarUpSet.congr
Proof state before:
case a.e_P.h
P Q : FVarId → Prop
fv✝ : FVarId
d : VLocalDecl
Δ : VLCtx
H : ∀ (fv : FVarId), fv ∈ VLCtx.fvars ((some fv✝, d) :: Δ) → (P fv ↔ Q fv)
i : Nat
fv : FVarId
⊢ VLCtx.vlamName Δ i = some (some fv) → P fv ↔ VLCtx.vlamName Δ i = some (some fv) → Q fv
Tactic:
exact imp_congr_right fun ha => H _ (.tail _ (VLCtx.vlamName_mem_fvars ha))
Proof state after:
no goals
Theorem: Lean4Lean.IsFVarUpSet.trivial
Proof state before:
val✝ : FVarId
d : VLocalDecl
Δ : List (Option FVarId × VLocalDecl)
x✝ : (fun x => True) val✝
⊢ VLocalDecl.OnVars (fun i => ∀ (fv : FVarId), VLCtx.vlamName Δ i = some (some fv) → (fun x => True) fv) d
Tactic:
cases d <;> simp [VLocalDecl.OnVars, VExpr.OnVars]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ parentD (Array.set arr x v) i = if ↑x = i then v.parent else parentD arr i
Tactic:
rw [parentD]
Proof state after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).parent
    else i) =
    if ↑x = i then v.parent else parentD arr i
Theorem: Lean4Lean.UnionFind.parentD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).parent
    else i) =
    if ↑x = i then v.parent else parentD arr i
Tactic:
simp [Array.get_eq_getElem, parentD]
Proof state after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].parent else i) =
    if ↑x = i then v.parent else if h : i < Array.size arr then arr[i].parent else i
Theorem: Lean4Lean.UnionFind.parentD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].parent else i) =
    if ↑x = i then v.parent else if h : i < Array.size arr then arr[i].parent else i
Tactic:
split <;> [split <;> simp [Array.get_set, *]; split <;> [(subst i; cases ‹¬_› x.2); rfl]]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parentD_set
Proof state before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
h✝¹ : ¬i < Array.size arr
h✝ : ↑x = i
⊢ i = v.parent
Tactic:
subst i
Proof state after:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ ↑x = v.parent
Theorem: Lean4Lean.UnionFind.parentD_set
Proof state before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ ↑x = v.parent
Tactic:
cases ‹¬_› x.2
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ rankD (Array.set arr x v) i = if ↑x = i then v.rank else rankD arr i
Tactic:
rw [rankD]
Proof state after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).rank else 0) =
    if ↑x = i then v.rank else rankD arr i
Theorem: Lean4Lean.UnionFind.rankD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).rank else 0) =
    if ↑x = i then v.rank else rankD arr i
Tactic:
simp [Array.get_eq_getElem, rankD]
Proof state after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].rank else 0) =
    if ↑x = i then v.rank else if h : i < Array.size arr then arr[i].rank else 0
Theorem: Lean4Lean.UnionFind.rankD_set
Proof state before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].rank else 0) =
    if ↑x = i then v.rank else if h : i < Array.size arr then arr[i].rank else 0
Tactic:
split <;> [split <;> simp [Array.get_set, *]; split <;> [(subst i; cases ‹¬_› x.2); rfl]]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rankD_set
Proof state before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
h✝¹ : ¬i < Array.size arr
h✝ : ↑x = i
⊢ 0 = v.rank
Tactic:
subst i
Proof state after:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ 0 = v.rank
Theorem: Lean4Lean.UnionFind.rankD_set
Proof state before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ 0 = v.rank
Tactic:
cases ‹¬_› x.2
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent'_lt
Proof state before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).parent < size self
Tactic:
simp [← parentD_eq, parentD_lt]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.parent_lt
Proof state before:
self : UnionFind
i : Nat
⊢ parent self i < size self ↔ i < size self
Tactic:
simp [parentD]
Proof state after:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).parent else i) <
      Array.size self.arr ↔
    i < Array.size self.arr
Theorem: Lean4Lean.UnionFind.parent_lt
Proof state before:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).parent else i) <
      Array.size self.arr ↔
    i < Array.size self.arr
Tactic:
split <;> simp [*, parent'_lt]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rank_lt
Proof state before:
self : UnionFind
i : Nat
⊢ parent self i ≠ i → rank self i < rank self (parent self i)
Tactic:
simpa [rank] using self.rankD_lt
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rank'_lt
Proof state before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).parent ≠ ↑i → rank self ↑i < rank self (Array.get self.arr i).parent
Tactic:
simpa [← parentD_eq] using self.rankD_lt
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < rankMax self
Tactic:
simp [rankMax, Array.foldr_eq_foldr_data]
Proof state after:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < List.foldr (fun x => max x.rank) 0 self.arr.data + 1
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).rank < List.foldr (fun x => max x.rank) 0 self.arr.data + 1
Tactic:
exact Nat.lt_succ.2 <| go (self.arr.data.get_mem i.1 i.2)
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)
Tactic:
dsimp
Proof state after:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Theorem: Lean4Lean.UnionFind.rank'_lt_rankMax
Proof state before:
self : UnionFind
i : Fin (size self)
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)
Tactic:
apply Nat.le_max_left
Proof state after:
no goals