Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
    else
      if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
      else (node ls ll lx lr).node' x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
              if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        rec nil
          (fun size l x_1 r l_ih r_ih ↦
            rec nil
              (fun size_1 l x_2 r l_ih r_ih ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

pp: case node.node.hnc
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ ¬ls + rs ≤ 1

Tactic:
· split_ifs with h h_1
        · have rd : delta ≤ size rl + size rr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
            rwa [sr.1, Nat.lt_succ_iff] at this
          obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
          · rw [size, zero_add] at rd
            exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
          obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
          · exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
          dsimp [rotateL]; split_ifs
          · simp [node3L, node', sr.1]; abel
          · simp [node4L, node', sr.1, sr.2.1.1]; abel
        · have ld : delta ≤ size ll + size lr := by
            have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
            rwa [sl.1, Nat.lt_succ_iff] at this
          obtain - | ⟨lls, lll, llx, llr⟩ := ll
          · rw [size, zero_add] at ld
            exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)
          obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
          · exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)
          dsimp [rotateR]; split_ifs
          · simp [node3R, node', sl.1]; abel
          · simp [node4R, node', sl.1, sl.2.2.1]; abel
        · simp [node']

Goal state after:
case node.node.hnc
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ ¬ls + rs ≤ 1