internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
case zero
n k : Nat
Γ✝ Γ' Γ As : List VExpr
h : List.length As = n
⊢ ∃ Γ₀ As_1 Δ Δ',
    List.length As_1 = n ∧ List.length Δ = 0 ∧ List.length Δ' = 0 ∧ Γ = Δ ++ Γ₀ ∧ As ++ Γ = Δ' ++ As_1 ++ Γ₀
Tactic:
exact ⟨Γ, As, [], [], h, rfl, rfl, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
case succ
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : LiftN n k✝ Γ✝ Γ'✝
ih : ∃ Γ₀ As Δ Δ', List.length As = n ∧ List.length Δ = k✝ ∧ List.length Δ' = k✝ ∧ Γ✝ = Δ ++ Γ₀ ∧ Γ'✝ = Δ' ++ As ++ Γ₀
⊢ ∃ Γ₀ As Δ Δ',
    List.length As = n ∧
      List.length Δ = k✝ + 1 ∧ List.length Δ' = k✝ + 1 ∧ A✝ :: Γ✝ = Δ ++ Γ₀ ∧ liftN n A✝ k✝ :: Γ'✝ = Δ' ++ As ++ Γ₀
Tactic:
obtain ⟨_, _, Δ, Δ', hn, hΔ, hΔ', rfl, rfl⟩ := ih
Proof state after:
case succ.intro.intro.intro.intro.intro.intro.intro.intro
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
A✝ : VExpr
w✝¹ w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n
hΔ : List.length Δ = k✝
hΔ' : List.length Δ' = k✝
a✝ : LiftN n k✝ (Δ ++ w✝¹) (Δ' ++ w✝ ++ w✝¹)
⊢ ∃ Γ₀ As Δ_1 Δ'_1,
    List.length As = n ∧
      List.length Δ_1 = k✝ + 1 ∧
        List.length Δ'_1 = k✝ + 1 ∧ A✝ :: (Δ ++ w✝¹) = Δ_1 ++ Γ₀ ∧ liftN n A✝ k✝ :: (Δ' ++ w✝ ++ w✝¹) = Δ'_1 ++ As ++ Γ₀
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
case succ.intro.intro.intro.intro.intro.intro.intro.intro
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
A✝ : VExpr
w✝¹ w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n
hΔ : List.length Δ = k✝
hΔ' : List.length Δ' = k✝
a✝ : LiftN n k✝ (Δ ++ w✝¹) (Δ' ++ w✝ ++ w✝¹)
⊢ ∃ Γ₀ As Δ_1 Δ'_1,
    List.length As = n ∧
      List.length Δ_1 = k✝ + 1 ∧
        List.length Δ'_1 = k✝ + 1 ∧ A✝ :: (Δ ++ w✝¹) = Δ_1 ++ Γ₀ ∧ liftN n A✝ k✝ :: (Δ' ++ w✝ ++ w✝¹) = Δ'_1 ++ As ++ Γ₀
Tactic:
exact ⟨_, _, _ :: Δ, _ :: Δ', hn, by simp [hΔ], by simp [hΔ'], rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
A✝ : VExpr
w✝¹ w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n
hΔ : List.length Δ = k✝
hΔ' : List.length Δ' = k✝
a✝ : LiftN n k✝ (Δ ++ w✝¹) (Δ' ++ w✝ ++ w✝¹)
⊢ List.length (A✝ :: Δ) = k✝ + 1
Tactic:
simp [hΔ]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.isSuffix
Proof state before:
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
A✝ : VExpr
w✝¹ w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n
hΔ : List.length Δ = k✝
hΔ' : List.length Δ' = k✝
a✝ : LiftN n k✝ (Δ ++ w✝¹) (Δ' ++ w✝ ++ w✝¹)
⊢ List.length (liftN n A✝ k✝ :: Δ') = k✝ + 1
Tactic:
simp [hΔ']
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂✝ Γ₂ : List VExpr
k2 : Nat
Γ₀ As : List VExpr
h : List.length As = n1
H2 : LiftN n2 k2 (As ++ Γ₀) Γ₂
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
⊢ LiftN (n1 + n2) 0 Γ₀ Γ₂
Tactic:
obtain ⟨Γ₀', _, Δ, Δ', hn, hΔ, hΔ', eq, rfl⟩ := H2.isSuffix
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ As : List VExpr
h : List.length As = n1
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
Γ₀' w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
eq : As ++ Γ₀ = Δ ++ Γ₀'
H2 : LiftN n2 k2 (As ++ Γ₀) (Δ' ++ w✝ ++ Γ₀')
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ Γ₀')
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ As : List VExpr
h : List.length As = n1
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
Γ₀' w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
eq : As ++ Γ₀ = Δ ++ Γ₀'
H2 : LiftN n2 k2 (As ++ Γ₀) (Δ' ++ w✝ ++ Γ₀')
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ Γ₀')
Tactic:
obtain ⟨As, rfl, rfl⟩ := (List.append_eq_append_of_length_le (by rwa [h, hΔ])).1 eq.symm
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ : List VExpr
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
As : List VExpr
h : List.length (Δ ++ As) = n1
eq : Δ ++ As ++ Γ₀ = Δ ++ (As ++ Γ₀)
H2 : LiftN n2 k2 (Δ ++ As ++ Γ₀) (Δ' ++ w✝ ++ (As ++ Γ₀))
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ (As ++ Γ₀))
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ : List VExpr
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
As : List VExpr
h : List.length (Δ ++ As) = n1
eq : Δ ++ As ++ Γ₀ = Δ ++ (As ++ Γ₀)
H2 : LiftN n2 k2 (Δ ++ As ++ Γ₀) (Δ' ++ w✝ ++ (As ++ Γ₀))
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ (As ++ Γ₀))
Tactic:
rw [← List.append_assoc]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ : List VExpr
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
As : List VExpr
h : List.length (Δ ++ As) = n1
eq : Δ ++ As ++ Γ₀ = Δ ++ (As ++ Γ₀)
H2 : LiftN n2 k2 (Δ ++ As ++ Γ₀) (Δ' ++ w✝ ++ (As ++ Γ₀))
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ As ++ Γ₀)
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ : List VExpr
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
As : List VExpr
h : List.length (Δ ++ As) = n1
eq : Δ ++ As ++ Γ₀ = Δ ++ (As ++ Γ₀)
H2 : LiftN n2 k2 (Δ ++ As ++ Γ₀) (Δ' ++ w✝ ++ (As ++ Γ₀))
⊢ LiftN (n1 + n2) 0 Γ₀ (Δ' ++ w✝ ++ As ++ Γ₀)
Tactic:
exact .zero _ (by simp [← h, hΔ, hΔ', hn, Nat.add_left_comm, Nat.add_comm])
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ As : List VExpr
h : List.length As = n1
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
Γ₀' w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
eq : As ++ Γ₀ = Δ ++ Γ₀'
H2 : LiftN n2 k2 (As ++ Γ₀) (Δ' ++ w✝ ++ Γ₀')
⊢ List.length Δ ≤ List.length As
Tactic:
rwa [h, hΔ]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.comp
Proof state before:
k1 k2✝ n1 : Nat
Γ₀✝ Γ₁ : List VExpr
n2 : Nat
Γ₂ : List VExpr
k2 : Nat
Γ₀ : List VExpr
h1 : 0 ≤ k2
h2 : k2 ≤ n1 + 0
w✝ Δ Δ' : List VExpr
hn : List.length w✝ = n2
hΔ : List.length Δ = k2
hΔ' : List.length Δ' = k2
As : List VExpr
h : List.length (Δ ++ As) = n1
eq : Δ ++ As ++ Γ₀ = Δ ++ (As ++ Γ₀)
H2 : LiftN n2 k2 (Δ ++ As ++ Γ₀) (Δ' ++ w✝ ++ (As ++ Γ₀))
⊢ List.length (Δ' ++ w✝ ++ As) = n1 + n2
Tactic:
simp [← h, hΔ, hΔ', hn, Nat.add_left_comm, Nat.add_comm]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
n k : Nat
Γ Γ' : List VExpr
⊢ LiftN n k Γ Γ' ↔ Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'
Tactic:
constructor <;> intro h
Proof state after:
case mp
n k : Nat
Γ Γ' : List VExpr
h : LiftN n k Γ Γ'
⊢ Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'

case mpr
n k : Nat
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'
⊢ LiftN n k Γ Γ'
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp
n k : Nat
Γ Γ' : List VExpr
h : LiftN n k Γ Γ'
⊢ Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'
Tactic:
induction h with
| zero As =>
  subst n
  induction As with
  | nil => simp [Lift'.refl]
  | cons _ _ ih => exact .skip ih
| succ _ ih => rw [← lift'_consN_skipN]; exact .cons ih
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.zero
n k : Nat
Γ Γ' Γ✝ As : List VExpr
h✝ : List.length As = n
⊢ Lift' (Lift.consN (Lift.skipN n) 0) Γ✝ (As ++ Γ✝)
Tactic:
subst n
Proof state after:
case mp.zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
⊢ Lift' (Lift.consN (Lift.skipN (List.length As)) 0) Γ✝ (As ++ Γ✝)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
⊢ Lift' (Lift.consN (Lift.skipN (List.length As)) 0) Γ✝ (As ++ Γ✝)
Tactic:
induction As with
| nil => simp [Lift'.refl]
| cons _ _ ih => exact .skip ih
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.zero.nil
k : Nat
Γ Γ' Γ✝ : List VExpr
⊢ Lift' (Lift.consN (Lift.skipN (List.length [])) 0) Γ✝ ([] ++ Γ✝)
Tactic:
simp [Lift'.refl]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.zero.cons
k : Nat
Γ Γ' Γ✝ : List VExpr
head✝ : VExpr
tail✝ : List VExpr
ih : Lift' (Lift.consN (Lift.skipN (List.length tail✝)) 0) Γ✝ (tail✝ ++ Γ✝)
⊢ Lift' (Lift.consN (Lift.skipN (List.length (head✝ :: tail✝))) 0) Γ✝ (head✝ :: tail✝ ++ Γ✝)
Tactic:
exact .skip ih
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.succ
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : LiftN n k✝ Γ✝ Γ'✝
ih : Lift' (Lift.consN (Lift.skipN n) k✝) Γ✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN n) (k✝ + 1)) (A✝ :: Γ✝) (liftN n A✝ k✝ :: Γ'✝)
Tactic:
rw [← lift'_consN_skipN]
Proof state after:
case mp.succ
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : LiftN n k✝ Γ✝ Γ'✝
ih : Lift' (Lift.consN (Lift.skipN n) k✝) Γ✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN n) (k✝ + 1)) (A✝ :: Γ✝) (lift' A✝ (Lift.consN (Lift.skipN n) k✝) :: Γ'✝)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mp.succ
n k : Nat
Γ Γ' : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : LiftN n k✝ Γ✝ Γ'✝
ih : Lift' (Lift.consN (Lift.skipN n) k✝) Γ✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN n) (k✝ + 1)) (A✝ :: Γ✝) (lift' A✝ (Lift.consN (Lift.skipN n) k✝) :: Γ'✝)
Tactic:
exact .cons ih
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr
n k : Nat
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'
⊢ LiftN n k Γ Γ'
Tactic:
induction k generalizing Γ Γ' with
| zero =>
  obtain ⟨_, rfl, eq⟩ : ∃ As, Γ' = As ++ Γ ∧ As.length = n := by
    induction n generalizing Γ' with
    | zero => cases h; exact ⟨[], rfl, rfl⟩
    | succ n ih => let .skip h := h; obtain ⟨_, rfl, rfl⟩ := ih h; exact ⟨_::_, rfl, rfl⟩
  exact .zero _ eq
| succ k ih => let .cons h := h; rw [lift'_consN_skipN]; exact .succ (ih h)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr.zero
n : Nat
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ Γ'
⊢ LiftN n Nat.zero Γ Γ'
Tactic:
obtain ⟨_, rfl, eq⟩ : ∃ As, Γ' = As ++ Γ ∧ As.length = n := by
  induction n generalizing Γ' with
  | zero => cases h; exact ⟨[], rfl, rfl⟩
  | succ n ih => let .skip h := h; obtain ⟨_, rfl, rfl⟩ := ih h; exact ⟨_::_, rfl, rfl⟩
Proof state after:
case mpr.zero.intro.intro
n : Nat
Γ w✝ : List VExpr
eq : List.length w✝ = n
h : Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ (w✝ ++ Γ)
⊢ LiftN n Nat.zero Γ (w✝ ++ Γ)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr.zero.intro.intro
n : Nat
Γ w✝ : List VExpr
eq : List.length w✝ = n
h : Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ (w✝ ++ Γ)
⊢ LiftN n Nat.zero Γ (w✝ ++ Γ)
Tactic:
exact .zero _ eq
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
n : Nat
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ Γ'
⊢ ∃ As, Γ' = As ++ Γ ∧ List.length As = n
Tactic:
induction n generalizing Γ' with
| zero => cases h; exact ⟨[], rfl, rfl⟩
| succ n ih => let .skip h := h; obtain ⟨_, rfl, rfl⟩ := ih h; exact ⟨_::_, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case zero
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN Nat.zero) Nat.zero) Γ Γ'
⊢ ∃ As, Γ' = As ++ Γ ∧ List.length As = Nat.zero
Tactic:
cases h
Proof state after:
case zero.refl
Γ : List VExpr
⊢ ∃ As, Γ = As ++ Γ ∧ List.length As = Nat.zero
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case zero.refl
Γ : List VExpr
⊢ ∃ As, Γ = As ++ Γ ∧ List.length As = Nat.zero
Tactic:
exact ⟨[], rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case succ
Γ : List VExpr
n : Nat
ih : ∀ {Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ Γ' → ∃ As, Γ' = As ++ Γ ∧ List.length As = n
Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN (Nat.succ n)) Nat.zero) Γ Γ'
⊢ ∃ As, Γ' = As ++ Γ ∧ List.length As = Nat.succ n
Tactic:
let .skip h := h
Proof state after:
case succ
Γ : List VExpr
n : Nat
ih : ∀ {Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ Γ' → ∃ As, Γ' = As ++ Γ ∧ List.length As = n
Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN (Nat.succ n)) Nat.zero) Γ Γ'
Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.skipN n) Γ Γ'✝
⊢ ∃ As, A✝ :: Γ'✝ = As ++ Γ ∧ List.length As = Nat.succ n
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case succ
Γ : List VExpr
n : Nat
ih : ∀ {Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) Nat.zero) Γ Γ' → ∃ As, Γ' = As ++ Γ ∧ List.length As = n
Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN (Nat.succ n)) Nat.zero) Γ Γ'
Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.skipN n) Γ Γ'✝
⊢ ∃ As, A✝ :: Γ'✝ = As ++ Γ ∧ List.length As = Nat.succ n
Tactic:
obtain ⟨_, rfl, rfl⟩ := ih h
Proof state after:
case succ.intro.intro
Γ Γ' : List VExpr
A✝ : VExpr
w✝ : List VExpr
ih :
  ∀ {Γ' : List VExpr},
    Lift' (Lift.consN (Lift.skipN (List.length w✝)) Nat.zero) Γ Γ' →
      ∃ As, Γ' = As ++ Γ ∧ List.length As = List.length w✝
h✝ : Lift' (Lift.consN (Lift.skipN (Nat.succ (List.length w✝))) Nat.zero) Γ Γ'
h : Lift' (Lift.skipN (List.length w✝)) Γ (w✝ ++ Γ)
⊢ ∃ As, A✝ :: (w✝ ++ Γ) = As ++ Γ ∧ List.length As = Nat.succ (List.length w✝)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case succ.intro.intro
Γ Γ' : List VExpr
A✝ : VExpr
w✝ : List VExpr
ih :
  ∀ {Γ' : List VExpr},
    Lift' (Lift.consN (Lift.skipN (List.length w✝)) Nat.zero) Γ Γ' →
      ∃ As, Γ' = As ++ Γ ∧ List.length As = List.length w✝
h✝ : Lift' (Lift.consN (Lift.skipN (Nat.succ (List.length w✝))) Nat.zero) Γ Γ'
h : Lift' (Lift.skipN (List.length w✝)) Γ (w✝ ++ Γ)
⊢ ∃ As, A✝ :: (w✝ ++ Γ) = As ++ Γ ∧ List.length As = Nat.succ (List.length w✝)
Tactic:
exact ⟨_::_, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr.succ
n k : Nat
ih : ∀ {Γ Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) k) Γ Γ' → LiftN n k Γ Γ'
Γ Γ' : List VExpr
h : Lift' (Lift.consN (Lift.skipN n) (Nat.succ k)) Γ Γ'
⊢ LiftN n (Nat.succ k) Γ Γ'
Tactic:
let .cons h := h
Proof state after:
case mpr.succ
n k : Nat
ih : ∀ {Γ Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) k) Γ Γ' → LiftN n k Γ Γ'
Γ Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN n) (Nat.succ k)) Γ Γ'
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ✝ Γ'✝
⊢ LiftN n (Nat.succ k) (A✝ :: Γ✝) (lift' A✝ (Lift.consN (Lift.skipN n) k) :: Γ'✝)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr.succ
n k : Nat
ih : ∀ {Γ Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) k) Γ Γ' → LiftN n k Γ Γ'
Γ Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN n) (Nat.succ k)) Γ Γ'
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ✝ Γ'✝
⊢ LiftN n (Nat.succ k) (A✝ :: Γ✝) (lift' A✝ (Lift.consN (Lift.skipN n) k) :: Γ'✝)
Tactic:
rw [lift'_consN_skipN]
Proof state after:
case mpr.succ
n k : Nat
ih : ∀ {Γ Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) k) Γ Γ' → LiftN n k Γ Γ'
Γ Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN n) (Nat.succ k)) Γ Γ'
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ✝ Γ'✝
⊢ LiftN n (Nat.succ k) (A✝ :: Γ✝) (liftN n A✝ k :: Γ'✝)
Theorem: Lean4Lean.Ctx.liftN_iff_lift'
Proof state before:
case mpr.succ
n k : Nat
ih : ∀ {Γ Γ' : List VExpr}, Lift' (Lift.consN (Lift.skipN n) k) Γ Γ' → LiftN n k Γ Γ'
Γ Γ' : List VExpr
h✝ : Lift' (Lift.consN (Lift.skipN n) (Nat.succ k)) Γ Γ'
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
h : Lift' (Lift.consN (Lift.skipN n) k) Γ✝ Γ'✝
⊢ LiftN n (Nat.succ k) (A✝ :: Γ✝) (liftN n A✝ k :: Γ'✝)
Tactic:
exact .succ (ih h)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
l₁ : Lift
Γ₁ Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
H1 : Lift' l₁ Γ₁ Γ₂
H2 : Lift' l₂ Γ₂ Γ₃
⊢ Lift' (Lift.comp l₁ l₂) Γ₁ Γ₃
Tactic:
induction H2 generalizing l₁ Γ₁ with
| refl => exact H1
| skip _ ih => exact .skip (ih H1)
| cons H2 ih =>
  cases H1 with
  | refl => exact .cons H2
  | skip H1 => exact .skip (ih H1)
  | cons H1 => rw [← VExpr.lift'_comp]; exact .cons (ih H1)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case refl
Γ₂ : List VExpr
l₂ : Lift
Γ₃ Γ✝ : List VExpr
l₁ : Lift
Γ₁ : List VExpr
H1 : Lift' l₁ Γ₁ Γ✝
⊢ Lift' (Lift.comp l₁ Lift.refl) Γ₁ Γ✝
Tactic:
exact H1
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case skip
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝ : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Lift' l✝ Γ✝ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝ → Lift' (Lift.comp l₁ l✝) Γ₁ Γ'✝
l₁ : Lift
Γ₁ : List VExpr
H1 : Lift' l₁ Γ₁ Γ✝
⊢ Lift' (Lift.comp l₁ (Lift.skip l✝)) Γ₁ (A✝ :: Γ'✝)
Tactic:
exact .skip (ih H1)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case cons
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝ : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
H2 : Lift' l✝ Γ✝ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝ → Lift' (Lift.comp l₁ l✝) Γ₁ Γ'✝
l₁ : Lift
Γ₁ : List VExpr
H1 : Lift' l₁ Γ₁ (A✝ :: Γ✝)
⊢ Lift' (Lift.comp l₁ (Lift.cons l✝)) Γ₁ (lift' A✝ l✝ :: Γ'✝)
Tactic:
cases H1 with
| refl => exact .cons H2
| skip H1 => exact .skip (ih H1)
| cons H1 => rw [← VExpr.lift'_comp]; exact .cons (ih H1)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case cons.refl
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝ : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
H2 : Lift' l✝ Γ✝ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝ → Lift' (Lift.comp l₁ l✝) Γ₁ Γ'✝
⊢ Lift' (Lift.comp Lift.refl (Lift.cons l✝)) (A✝ :: Γ✝) (lift' A✝ l✝ :: Γ'✝)
Tactic:
exact .cons H2
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case cons.skip
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝¹ : Lift
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
H2 : Lift' l✝¹ Γ✝ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝ → Lift' (Lift.comp l₁ l✝¹) Γ₁ Γ'✝
Γ₁ : List VExpr
l✝ : Lift
H1 : Lift' l✝ Γ₁ Γ✝
⊢ Lift' (Lift.comp (Lift.skip l✝) (Lift.cons l✝¹)) Γ₁ (lift' A✝ l✝¹ :: Γ'✝)
Tactic:
exact .skip (ih H1)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case cons.cons
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝¹ : Lift
Γ✝¹ Γ'✝ : List VExpr
H2 : Lift' l✝¹ Γ✝¹ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝¹ → Lift' (Lift.comp l₁ l✝¹) Γ₁ Γ'✝
l✝ : Lift
Γ✝ : List VExpr
A✝ : VExpr
H1 : Lift' l✝ Γ✝ Γ✝¹
⊢ Lift' (Lift.comp (Lift.cons l✝) (Lift.cons l✝¹)) (A✝ :: Γ✝) (lift' (lift' A✝ l✝) l✝¹ :: Γ'✝)
Tactic:
rw [← VExpr.lift'_comp]
Proof state after:
case cons.cons
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝¹ : Lift
Γ✝¹ Γ'✝ : List VExpr
H2 : Lift' l✝¹ Γ✝¹ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝¹ → Lift' (Lift.comp l₁ l✝¹) Γ₁ Γ'✝
l✝ : Lift
Γ✝ : List VExpr
A✝ : VExpr
H1 : Lift' l✝ Γ✝ Γ✝¹
⊢ Lift' (Lift.comp (Lift.cons l✝) (Lift.cons l✝¹)) (A✝ :: Γ✝) (lift' A✝ (Lift.comp l✝ l✝¹) :: Γ'✝)
Theorem: Lean4Lean.Ctx.Lift'.comp
Proof state before:
case cons.cons
Γ₂ : List VExpr
l₂ : Lift
Γ₃ : List VExpr
l✝¹ : Lift
Γ✝¹ Γ'✝ : List VExpr
H2 : Lift' l✝¹ Γ✝¹ Γ'✝
ih : ∀ {l₁ : Lift} {Γ₁ : List VExpr}, Lift' l₁ Γ₁ Γ✝¹ → Lift' (Lift.comp l₁ l✝¹) Γ₁ Γ'✝
l✝ : Lift
Γ✝ : List VExpr
A✝ : VExpr
H1 : Lift' l✝ Γ✝ Γ✝¹
⊢ Lift' (Lift.comp (Lift.cons l✝) (Lift.cons l✝¹)) (A✝ :: Γ✝) (lift' A✝ (Lift.comp l✝ l✝¹) :: Γ'✝)
Tactic:
exact .cons (ih H1)
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
l : Lift
k : Nat
Γ₁ Γ₃ : List VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃
⊢ ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Tactic:
induction k generalizing Γ₁ Γ₃ with
| zero => let .skip H := H; exact ⟨_, H, .one⟩
| succ k ih =>
  let .cons (A := A) H := H
  let ⟨_, h1, h2⟩ := ih H
  refine ⟨_, .cons h1, ?_⟩
  simp only [Ctx.liftN_iff_lift'] at h2 ⊢
  simpa [← VExpr.lift'_comp, ← Lift.consN_comp] using h2.cons (A := lift' A (.consN l k))
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case zero
l : Lift
Γ₁ Γ₃ : List VExpr
H : Lift' (Lift.consN (Lift.skip l) Nat.zero) Γ₁ Γ₃
⊢ ∃ Γ₂, Lift' (Lift.consN l Nat.zero) Γ₁ Γ₂ ∧ LiftN 1 Nat.zero Γ₂ Γ₃
Tactic:
let .skip H := H
Proof state after:
case zero
l : Lift
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) Nat.zero) Γ₁ Γ₃
Γ'✝ : List VExpr
A✝ : VExpr
H : Lift' l Γ₁ Γ'✝
⊢ ∃ Γ₂, Lift' (Lift.consN l Nat.zero) Γ₁ Γ₂ ∧ LiftN 1 Nat.zero Γ₂ (A✝ :: Γ'✝)
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case zero
l : Lift
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) Nat.zero) Γ₁ Γ₃
Γ'✝ : List VExpr
A✝ : VExpr
H : Lift' l Γ₁ Γ'✝
⊢ ∃ Γ₂, Lift' (Lift.consN l Nat.zero) Γ₁ Γ₂ ∧ LiftN 1 Nat.zero Γ₂ (A✝ :: Γ'✝)
Tactic:
exact ⟨_, H, .one⟩
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
⊢ ∃ Γ₂, Lift' (Lift.consN l (Nat.succ k)) Γ₁ Γ₂ ∧ LiftN 1 (Nat.succ k) Γ₂ Γ₃
Tactic:
let .cons (A := A) H := H
Proof state after:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
⊢ ∃ Γ₂,
    Lift' (Lift.consN l (Nat.succ k)) (A :: Γ✝) Γ₂ ∧
      LiftN 1 (Nat.succ k) Γ₂ (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip
Proof state before:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
⊢ ∃ Γ₂,
    Lift' (Lift.consN l (Nat.succ k)) (A :: Γ✝) Γ₂ ∧
      LiftN 1 (Nat.succ k) Γ₂ (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
let ⟨_, h1, h2⟩ := ih H
Proof state after:
case succ
l : Lift
k : Nat
ih :
  ∀ {Γ₁ Γ₃ : List VExpr},
    Lift' (Lift.consN (Lift.skip l) k) Γ₁ Γ₃ → ∃ Γ₂, Lift' (Lift.consN l k) Γ₁ Γ₂ ∧ LiftN 1 k Γ₂ Γ₃
Γ₁ Γ₃ : List VExpr
H✝ : Lift' (Lift.consN (Lift.skip l) (Nat.succ k)) Γ₁ Γ₃
Γ✝ Γ'✝ : List VExpr
A : VExpr
H : Lift' (Lift.consN (Lift.skip l) k) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : LiftN 1 k w✝ Γ'✝
⊢ ∃ Γ₂,
    Lift' (Lift.consN l (Nat.succ k)) (A :: Γ✝) Γ₂ ∧
      LiftN 1 (Nat.succ k) Γ₂ (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)