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

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

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

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

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

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

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

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

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