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

State before:
case bvar
n1 n2 i k1 k2 : Nat
h : k2 ≤ 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 (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
split <;> rename_i h'
State after:
case bvar.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i

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

State before:
case bvar.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
rw [if_pos (c := _ < n2 + k1)]
State after:
case bvar.inl.hc
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) < n2 + k1

State before:
case bvar.inl.hc
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
⊢ (if i < k2 then i else n2 + i) < n2 + k1
Tactic:
split
State after:
case bvar.inl.hc.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : i < k2
⊢ i < n2 + k1

case bvar.inl.hc.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : ¬i < k2
⊢ n2 + i < n2 + k1

State before:
case bvar.inl.hc.inl
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : i < k2
⊢ i < n2 + k1
Tactic:
exact Nat.lt_add_left _ h'
State after:
no goals

State before:
case bvar.inl.hc.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : i < k1
h✝ : ¬i < k2
⊢ n2 + i < n2 + k1
Tactic:
exact Nat.add_lt_add_left h' _
State after:
no goals

State before:
case bvar.inr
n1 n2 i k1 k2 : Nat
h : k2 ≤ k1
h' : ¬i < k1
this : ¬i < k2
⊢ (if n1 + i < k2 then n1 + i else n2 + (n1 + i)) =
    if (if i < k2 then i else n2 + i) < n2 + k1 then if i < k2 then i else n2 + i else n1 + if i < k2 then i else n2 + i
Tactic:
rw [if_neg (mt (Nat.lt_of_le_of_lt (Nat.le_add_left _ n1)) this),
  if_neg this, if_neg (mt (Nat.add_lt_add_iff_left ..).1 h'), Nat.add_left_comm]
State after:
no goals