Theorem: Lean4Lean.Lift.depth_succ (Lean4Lean/Theory/VExpr.lean)

State before:
n : Nat
l : Lift
H : depth l = n + 1
⊢ ∃ l' k, depth l' = n ∧ l = consN (skip l') k
Tactic:
match l with
| .skip l => cases H; exact ⟨l, 0, rfl, rfl⟩
| .cons l =>
  obtain ⟨l, k, rfl, ⟨⟩⟩ := depth_succ (l := l) H
  exact ⟨l, k+1, rfl, rfl⟩
State after:
no goals

State before:
n : Nat
l✝ l : Lift
H : depth (skip l) = n + 1
⊢ ∃ l' k, depth l' = n ∧ skip l = consN (skip l') k
Tactic:
cases H
State after:
case refl
l✝ l : Lift
⊢ ∃ l' k, depth l' = depth l ∧ skip l = consN (skip l') k

State before:
case refl
l✝ l : Lift
⊢ ∃ l' k, depth l' = depth l ∧ skip l = consN (skip l') k
Tactic:
exact ⟨l, 0, rfl, rfl⟩
State after:
no goals

State before:
n : Nat
l✝ l : Lift
H : depth (cons l) = n + 1
⊢ ∃ l' k, depth l' = n ∧ cons l = consN (skip l') k
Tactic:
obtain ⟨l, k, rfl, ⟨⟩⟩ := depth_succ (l := l) H
State after:
case intro.intro.intro.refl
l✝ l : Lift
k : Nat
H : depth (cons (consN (skip l) k)) = depth l + 1
⊢ ∃ l' k_1, depth l' = depth l ∧ cons (consN (skip l) k) = consN (skip l') k_1

State before:
case intro.intro.intro.refl
l✝ l : Lift
k : Nat
H : depth (cons (consN (skip l) k)) = depth l + 1
⊢ ∃ l' k_1, depth l' = depth l ∧ cons (consN (skip l) k) = consN (skip l') k_1
Tactic:
exact ⟨l, k+1, rfl, rfl⟩
State after:
no goals