Theorem: Lean4Lean.Ctx.LiftN.isSuffix (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
n k : Nat
Γ Γ' : List VExpr
H : LiftN n k Γ Γ'
⊢ ∃ Γ₀ As Δ Δ', List.length As = n ∧ List.length Δ = k ∧ List.length Δ' = k ∧ Γ = Δ ++ Γ₀ ∧ Γ' = Δ' ++ As ++ Γ₀
Tactic:
induction H with
| @zero Γ As h => exact ⟨Γ, As, [], [], h, rfl, rfl, rfl, rfl⟩
| succ _ ih =>
  obtain ⟨_, _, Δ, Δ', hn, hΔ, hΔ', rfl, rfl⟩ := ih
  exact ⟨_, _, _ :: Δ, _ :: Δ', hn, by simp [hΔ], by simp [hΔ'], rfl, rfl⟩
State after:
no goals

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⟩
State after:
no goals

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
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 ++ Γ₀

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⟩
State after:
no goals

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Δ]
State after:
no goals

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Δ']
State after:
no goals