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

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
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✝ ++ Γ₀')

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

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

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

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

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