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

State before:
k2 k1 n1 : Nat
e : VExpr
n2 : Nat
h : k2 ≤ k1
⊢ liftN n1 (unliftN e n2 k2) k1 = unliftN (liftN n1 e (k1 + n2)) n2 k2
Tactic:
obtain ⟨k1, rfl⟩ := Nat.le_iff_exists_add'.1 h
State after:
case intro
k2 n1 : Nat
e : VExpr
n2 k1 : Nat
h : k2 ≤ k1 + k2
⊢ liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2

State before:
case intro
k2 n1 : Nat
e : VExpr
n2 k1 : Nat
h : k2 ≤ k1 + k2
⊢ liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
Tactic:
induction n2 generalizing e with simp [unliftN]
| succ n2 ih =>
  rw [ih, Nat.add_right_comm, liftN_instN_hi e default n1 (k1+n2) k2,
    Nat.add_right_comm k1]; rfl
State after:
no goals

State before:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ liftN n1 (unliftN (inst e default k2) n2 k2) (k1 + k2) =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2
Tactic:
rw [ih, Nat.add_right_comm, liftN_instN_hi e default n1 (k1+n2) k2,
  Nat.add_right_comm k1]
State after:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ unliftN (inst (liftN n1 e (k1 + k2 + n2 + 1)) (liftN n1 default (k1 + n2)) k2) n2 k2 =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2

State before:
case intro.succ
k2 n1 k1 : Nat
h : k2 ≤ k1 + k2
n2 : Nat
ih : ∀ {e : VExpr}, liftN n1 (unliftN e n2 k2) (k1 + k2) = unliftN (liftN n1 e (k1 + k2 + n2)) n2 k2
e : VExpr
⊢ unliftN (inst (liftN n1 e (k1 + k2 + n2 + 1)) (liftN n1 default (k1 + n2)) k2) n2 k2 =
    unliftN (inst (liftN n1 e (k1 + k2 + Nat.succ n2)) default k2) n2 k2
Tactic:
rfl
State after:
no goals