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 = comp l' (consN (skipN 1) k)
Tactic:
let ⟨l', k, h1, h2⟩ := depth_succ H
State after:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ ∃ l' k, depth l' = n ∧ l = comp l' (consN (skipN 1) k)

State before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ ∃ l' k, depth l' = n ∧ l = comp l' (consN (skipN 1) k)
Tactic:
exact ⟨.consN l' k, k, by simp [h1], by rwa [← consN_skip_eq]⟩
State after:
no goals

State before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ depth (consN l' k) = n
Tactic:
simp [h1]
State after:
no goals

State before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ l = comp (consN l' k) (consN (skipN 1) k)
Tactic:
rwa [← consN_skip_eq]
State after:
no goals