Theorem: Lean4Lean.VExpr.skips_add (Lean4Lean/Theory/VExpr.lean)

State before:
e : VExpr
n1 n2 k : Nat
⊢ Skips e (n1 + n2) k ↔ ∃ e', Skips e' n1 k ∧ e = liftN n2 e' k
Tactic:
simp [skips_iff_exists, ← liftN'_liftN_hi]
State after:
e : VExpr
n1 n2 k : Nat
⊢ (∃ e', e = liftN n2 (liftN n1 e' k) k) ↔ ∃ e', (∃ e'_1, e' = liftN n1 e'_1 k) ∧ e = liftN n2 e' k

State before:
e : VExpr
n1 n2 k : Nat
⊢ (∃ e', e = liftN n2 (liftN n1 e' k) k) ↔ ∃ e', (∃ e'_1, e' = liftN n1 e'_1 k) ∧ e = liftN n2 e' k
Tactic:
exact ⟨fun ⟨_, h⟩ => ⟨_, ⟨_, rfl⟩, h⟩, fun ⟨_, ⟨_, rfl⟩, h⟩ => ⟨_, h⟩⟩
State after:
no goals