internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar.intro.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
i : Nat
hs : i < dk✝ + 1
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
h1 : VLCtx.find? ((none, d) :: Δ₂) (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
⊢ ∃ p, VLCtx.find? ((none, d✝) :: Δ✝) (Sum.inl i) = some p
Tactic:
simp [VLCtx.find?] at h1 ⊢
Proof state after:
case bvar.cons_bvar.intro.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
i : Nat
hs : i < dk✝ + 1
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
h1 :
  (match VLCtx.next none (Sum.inl i) with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ₂ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
⊢ ∃ p,
    (match VLCtx.next none (Sum.inl i) with
      | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
      | some v =>
        Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
      some p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar.intro.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
i : Nat
hs : i < dk✝ + 1
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
h1 :
  (match VLCtx.next none (Sum.inl i) with
    | none => some (VLocalDecl.value d, VLocalDecl.type d)
    | some v =>
      Option.bind (VLCtx.find? Δ₂ v) fun __discr =>
        some (VExpr.liftN (VLocalDecl.depth d) __discr.fst, VExpr.liftN (VLocalDecl.depth d) __discr.snd)) =
    some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
⊢ ∃ p,
    (match VLCtx.next none (Sum.inl i) with
      | none => some (VLocalDecl.value d✝, VLocalDecl.type d✝)
      | some v =>
        Option.bind (VLCtx.find? Δ✝ v) fun __discr =>
          some (VExpr.liftN (VLocalDecl.depth d✝) __discr.fst, VExpr.liftN (VLocalDecl.depth d✝) __discr.snd)) =
      some p
Tactic:
rcases i with _ | i <;> simp [VLCtx.next, bind] at h1 ⊢
Proof state after:
case bvar.cons_bvar.intro.intro.intro.succ
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
h1 :
  ∃ a,
    VLCtx.find? Δ₂ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar.intro.intro.intro.succ
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
h1 :
  ∃ a,
    VLCtx.find? Δ₂ (Sum.inl i) = some a ∧
      VExpr.liftN (VLocalDecl.depth d) a.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) a.snd = A
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Tactic:
obtain ⟨_, h1, _⟩ := h1
Proof state after:
case bvar.cons_bvar.intro.intro.intro.succ.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
w✝ : VExpr × VExpr
h1 : VLCtx.find? Δ₂ (Sum.inl i) = some w✝
right✝ : VExpr.liftN (VLocalDecl.depth d) w✝.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) w✝.snd = A
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar.intro.intro.intro.succ.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
w✝ : VExpr × VExpr
h1 : VLCtx.find? Δ₂ (Sum.inl i) = some w✝
right✝ : VExpr.liftN (VLocalDecl.depth d) w✝.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) w✝.snd = A
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Tactic:
have ⟨_, h1⟩ := ih h1 hΔ₁ (Nat.lt_of_succ_lt_succ hs)
Proof state after:
case bvar.cons_bvar.intro.intro.intro.succ.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
w✝¹ : VExpr × VExpr
h1✝ : VLCtx.find? Δ₂ (Sum.inl i) = some w✝¹
right✝ : VExpr.liftN (VLocalDecl.depth d) w✝¹.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) w✝¹.snd = A
w✝ : VExpr × VExpr
h1 : VLCtx.find? Δ✝ (Sum.inl i) = some w✝
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.cons_bvar.intro.intro.intro.succ.intro.intro
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝¹ : VLCtx
dk k : Nat
Δ✝ Δ₂✝ : VLCtx
dk✝ n✝ k✝ : Nat
d✝ : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂✝ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂✝ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
d : VLocalDecl
Δ₂ : List (Option FVarId × VLocalDecl)
hΔ₁ : VLCtx.IsDefEq env (List.length Us) Δ₂ Δ₂✝
hΔ : VLCtx.IsDefEq env (List.length Us) ((none, d) :: Δ₂) ((none, VLocalDecl.liftN d✝ n✝ k✝) :: Δ₂✝)
i : Nat
hs : Nat.succ i < dk✝ + 1
w✝¹ : VExpr × VExpr
h1✝ : VLCtx.find? Δ₂ (Sum.inl i) = some w✝¹
right✝ : VExpr.liftN (VLocalDecl.depth d) w✝¹.fst = e ∧ VExpr.liftN (VLocalDecl.depth d) w✝¹.snd = A
w✝ : VExpr × VExpr
h1 : VLCtx.find? Δ✝ (Sum.inl i) = some w✝
⊢ ∃ p a,
    VLCtx.find? Δ✝ (Sum.inl i) = some a ∧
      (VExpr.liftN (VLocalDecl.depth d✝) a.fst, VExpr.liftN (VLocalDecl.depth d✝) a.snd) = p
Tactic:
exact ⟨_, _, h1, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case bvar.skip_fvar
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂ : VLCtx
dk k : Nat
Δ✝ Δ'✝ : VLCtx
n✝ : Nat
fv✝ : FVarId
d✝ : VLocalDecl
a✝ : VLCtx.LiftN Δ✝ Δ'✝ 0 n✝ 0
a_ih✝ :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ'✝ → i < 0 → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ ((some fv✝, d✝) :: Δ'✝)
hs : i < 0
⊢ ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
Tactic:
cases hs
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
env : VEnv
n : Nat
Δ₁✝ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
Δ Δ₂✝ : VLCtx
dk k : Nat
Δ✝ Δ₂ : VLCtx
dk✝ n✝ k✝ : Nat
d : VLocalDecl
W : VLCtx.LiftN Δ✝ Δ₂ dk✝ n✝ k✝
ih :
  ∀ {e A : VExpr} {Δ₁ : VLCtx} {i : Nat},
    VLCtx.find? Δ₁ (Sum.inl i) = some (e, A) →
      VLCtx.IsDefEq env (List.length Us) Δ₁ Δ₂ → i < dk✝ → ∃ p, VLCtx.find? Δ✝ (Sum.inl i) = some p
e A : VExpr
Δ₁ : VLCtx
i : Nat
h1 : VLCtx.find? Δ₁ (Sum.inl i) = some (e, A)
hΔ : VLCtx.IsDefEq env (List.length Us) Δ₁ ((none, VLocalDecl.liftN d n✝ k✝) :: Δ₂)
hs : i < dk✝ + 1
⊢ ∃ d Δ₁', Δ₁ = (none, d) :: Δ₁' ∧ VLCtx.IsDefEq env (List.length Us) Δ₁' Δ₂
Tactic:
cases d <;> cases hΔ <;> exact ⟨_, _, rfl, ‹_›⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case fvar
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ✝ : VLCtx
fv : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
Δ Δ₂ : 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.fvar fv) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.fvar fv) e'
Tactic:
let ⟨_, h⟩ := VLCtx.find?_eq_some.2 hs
Proof state after:
case fvar
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ✝ : VLCtx
fv : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
Δ Δ₂ : 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.fvar fv) dk
w✝ : VExpr × VExpr
h : VLCtx.find? Δ (Sum.inr fv) = some w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.fvar fv) e'
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case fvar
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e✝ : Expr
e' : VExpr
henv : Ordered env
e A : VExpr
Δ✝ : VLCtx
fv : FVarId
h1 : VLCtx.find? Δ✝ (Sum.inr fv) = some (e, A)
Δ Δ₂ : 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.fvar fv) dk
w✝ : VExpr × VExpr
h : VLCtx.find? Δ (Sum.inr fv) = some w✝
⊢ ∃ e', TrExpr env Us Δ (Expr.fvar fv) e'
Tactic:
exact ⟨_, .fvar h⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case sort
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
u✝ : Level
u'✝ : VLevel
Δ✝ : VLCtx
h1 : VLevel.ofLevel Us u✝ = some u'✝
Δ Δ₂ : 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.sort u✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.sort u✝) e'
Tactic:
exact ⟨_, .sort h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.TrExpr.weakN_inv
Proof state before:
case const
env : VEnv
n : Nat
Δ₁ : VLCtx
Us : List Name
e : Expr
e' : VExpr
henv : Ordered env
c✝ : Name
ci✝ : VConstant
us'✝ : List VLevel
Δ✝ : VLCtx
us✝ : List Level
h1 : env.constants c✝ = some (some ci✝)
h2 : List.mapM (VLevel.ofLevel Us) us✝ = some us'✝
h3 : List.length us✝ = ci✝.uvars
Δ Δ₂ : 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.const c✝ us✝) dk
⊢ ∃ e', TrExpr env Us Δ (Expr.const c✝ us✝) e'
Tactic:
exact ⟨_, .const h1 h2 h3⟩
Proof state after:
no goals
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
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have hΔ₁ := hΔ.wf
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) Δ✝
⊢ ∃ 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) Δ✝
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
have hΔ₂ := (hΔ.symm henv).wf
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) Δ₂
⊢ ∃ 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) Δ₂
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
let ⟨f₁, ih1⟩ := ih1 W hΔ hs.1
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₁
⊢ ∃ 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₁
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'
Tactic:
let ⟨a₁, ih2⟩ := ih2 W hΔ hs.2
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₁
⊢ ∃ e', TrExpr env Us Δ (Expr.app f✝ a✝) e'