Theorem: Lean4Lean.Ctx.Lift'.of_cons_skip (Lean4Lean/Theory/Typing/Lemmas.lean)

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

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

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

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

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

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) Γ✝ Γ'✝
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) :: Γ'✝)
Tactic:
refine ⟨_, .cons h1, ?_⟩
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✝ Γ'✝
⊢ LiftN 1 (Nat.succ k) (lift' A (Lift.consN l k) :: w✝) (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)

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) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : LiftN 1 k w✝ Γ'✝
⊢ LiftN 1 (Nat.succ k) (lift' A (Lift.consN l k) :: w✝) (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
simp only [Ctx.liftN_iff_lift'] at h2 ⊢
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 : Lift' (Lift.consN (Lift.skipN 1) k) w✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN 1) (Nat.succ k)) (lift' A (Lift.consN l k) :: w✝)
    (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)

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) Γ✝ Γ'✝
w✝ : List VExpr
h1 : Lift' (Lift.consN l k) Γ✝ w✝
h2 : Lift' (Lift.consN (Lift.skipN 1) k) w✝ Γ'✝
⊢ Lift' (Lift.consN (Lift.skipN 1) (Nat.succ k)) (lift' A (Lift.consN l k) :: w✝)
    (lift' A (Lift.consN (Lift.skip l) k) :: Γ'✝)
Tactic:
simpa [← VExpr.lift'_comp, ← Lift.consN_comp] using h2.cons (A := lift' A (.consN l k))
State after:
no goals