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

State before:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)
Tactic:
have : (liftN n1 e1 (k1+n2+k2)).Skips n2 k2 := h ▸ .liftN
State after:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 e1 (k1 + n2 + k2)) n2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)

State before:
n1 : Nat
e1 : VExpr
k1 n2 k2 : Nat
e2 : VExpr
h : liftN n1 e1 (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 e1 (k1 + n2 + k2)) n2 k2
⊢ ∃ e', e1 = liftN n2 e' k2 ∧ e2 = liftN n1 e' (k1 + k2)
Tactic:
obtain ⟨e', rfl⟩ := skips_iff_exists.1 <|
  this.of_liftN_hi (Nat.add_assoc .. ▸ Nat.le_add_left ..)
State after:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ ∃ e'_1, liftN n2 e' k2 = liftN n2 e'_1 k2 ∧ e2 = liftN n1 e'_1 (k1 + k2)

State before:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ ∃ e'_1, liftN n2 e' k2 = liftN n2 e'_1 k2 ∧ e2 = liftN n1 e'_1 (k1 + k2)
Tactic:
refine ⟨e', rfl, ?_⟩
State after:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ e2 = liftN n1 e' (k1 + k2)

State before:
case intro
n1 k1 n2 k2 : Nat
e2 e' : VExpr
h : liftN n1 (liftN n2 e' k2) (k1 + n2 + k2) = liftN n2 e2 k2
this : Skips (liftN n1 (liftN n2 e' k2) (k1 + n2 + k2)) n2 k2
⊢ e2 = liftN n1 e' (k1 + k2)
Tactic:
rw [← liftN_inj, ← h, liftN'_comm (n1 := n1) (h := Nat.le_add_left ..),
  Nat.add_left_comm, Nat.add_assoc]
State after:
no goals