Theorem: Lean4Lean.VExpr.liftN'_liftN' (Lean4Lean/Theory/VExpr.lean)

State before:
case bvar
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
⊢ (if (if i < k1 then i else n1 + i) < k2 then if i < k1 then i else n1 + i else n2 + if i < k1 then i else n1 + i) =
    if i < k1 then i else n1 + (n2 + i)
Tactic:
split <;> rename_i h
State after:
case bvar.inl
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : i < k1
⊢ (if i < k2 then i else n2 + i) = i

case bvar.inr
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : ¬i < k1
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) = n1 + (n2 + i)

State before:
case bvar.inl
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : i < k1
⊢ (if i < k2 then i else n2 + i) = i
Tactic:
rw [if_pos (Nat.lt_of_lt_of_le h h1)]
State after:
no goals

State before:
case bvar.inr
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h : ¬i < k1
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) = n1 + (n2 + i)
Tactic:
rw [if_neg (mt (fun h => ?_) h), Nat.add_left_comm]
State after:
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h✝ : ¬i < k1
h : n1 + i < k2
⊢ i < k1

State before:
n1 n2 i k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
h✝ : ¬i < k1
h : n1 + i < k2
⊢ i < k1
Tactic:
exact (Nat.add_lt_add_iff_left ..).1 (Nat.lt_of_lt_of_le h h2)
State after:
no goals

State before:
case forallE
n1 n2 : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ {k1 k2 : Nat}, k1 ≤ k2 → k2 ≤ n1 + k1 → liftN n2 (liftN n1 binderType✝ k1) k2 = liftN (n1 + n2) binderType✝ k1
IH2 : ∀ {k1 k2 : Nat}, k1 ≤ k2 → k2 ≤ n1 + k1 → liftN n2 (liftN n1 body✝ k1) k2 = liftN (n1 + n2) body✝ k1
k1 k2 : Nat
h1 : k1 ≤ k2
h2 : k2 ≤ n1 + k1
⊢ liftN n2 (liftN n1 body✝ (k1 + 1)) (k2 + 1) = liftN (n1 + n2) body✝ (k1 + 1)
Tactic:
rw [IH2 (Nat.succ_le_succ h1) (Nat.succ_le_succ h2)]
State after:
no goals