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

State before:
n k : Nat
Γ Γ' : List VExpr
⊢ LiftN n k Γ Γ' ↔ Lift' (Lift.consN (Lift.skipN n) k) Γ Γ'
Tactic:
constructor <;> intro h
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 Γ Γ'

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

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
State after:
case mp.zero
k : Nat
Γ Γ' Γ✝ As : List VExpr
⊢ Lift' (Lift.consN (Lift.skipN (List.length As)) 0) Γ✝ (As ++ Γ✝)

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

State before:
case mp.zero.nil
k : Nat
Γ Γ' Γ✝ : List VExpr
⊢ Lift' (Lift.consN (Lift.skipN (List.length [])) 0) Γ✝ ([] ++ Γ✝)
Tactic:
simp [Lift'.refl]
State after:
no goals

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

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

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

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

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

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

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

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
State after:
case zero.refl
Γ : List VExpr
⊢ ∃ As, Γ = As ++ Γ ∧ List.length As = Nat.zero

State before:
case zero.refl
Γ : List VExpr
⊢ ∃ As, Γ = As ++ Γ ∧ List.length As = Nat.zero
Tactic:
exact ⟨[], rfl, rfl⟩
State after:
no goals

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
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

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
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✝)

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

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

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

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