case nil
α : Type u_1
x : α
r : Ordnode α
hr : Balanced r
sr : Sized r
hl : Balanced nil
sl : Sized nil
⊢ balance nil x r = balance' nil x r

case node
α : Type u_1
x : α
r : Ordnode α
hr : Balanced r
sr : Sized r
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
⊢ balance (node ls ll lx lr) x r = balance' (node ls ll lx lr) x r
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
⊢ balance l x r = balance' l x r
cases' l with ls ll lx lr
case nil.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
hr : Balanced nil
sr : Sized nil
⊢ balance nil x nil = balance' nil x nil

case nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance nil x (node rs rl rx rr) = balance' nil x (node rs rl rx rr)
case nil
α : Type u_1
x : α
r : Ordnode α
hr : Balanced r
sr : Sized r
hl : Balanced nil
sl : Sized nil
⊢ balance nil x r = balance' nil x r
cases' r with rs rl rx rr
no goals
case nil.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
hr : Balanced nil
sr : Sized nil
⊢ balance nil x nil = balance' nil x nil
rfl
case nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node' rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance nil x (node' rl rx rr) = balance' nil x (node' rl rx rr)
case nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance nil x (node rs rl rx rr) = balance' nil x (node rs rl rx rr)
rw [sr.eq_node'] at hr ⊢
case nil.node.nil.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
hr : Balanced (node' nil rx nil)
sr : Sized (node rs nil rx nil)
⊢ node 2 nil x (node' nil rx nil) =
    if 0 + (0 + 1) ≤ 1 then node' nil x (node' nil rx nil)
    else
      if 0 + 1 > 0 then rotateL nil x (node' nil rx nil)
      else if 0 > delta * (0 + 1) then rotateR nil x (node' nil rx nil) else node' nil x (node' nil rx nil)

case nil.node.nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs rrl rrx rrr))
        else node' nil x (node' nil rx (node rrs rrl rrx rrr))

case nil.node.node.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx nil)
        else node' nil x (node' (node rls rll rlx rlr) rx nil)

case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
    else
      if rls + rrs + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (rls + rrs + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
        else node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
case nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node' rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance nil x (node' rl rx rr) = balance' nil x (node' rl rx rr)
cases' rl with rls rll rlx rlr <;> cases' rr with rrs rrl rrx rrr <;>
  dsimp [balance, balance']
no goals
case nil.node.nil.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
hr : Balanced (node' nil rx nil)
sr : Sized (node rs nil rx nil)
⊢ node 2 nil x (node' nil rx nil) =
    if 0 + (0 + 1) ≤ 1 then node' nil x (node' nil rx nil)
    else
      if 0 + 1 > 0 then rotateL nil x (node' nil rx nil)
      else if 0 > delta * (0 + 1) then rotateR nil x (node' nil rx nil) else node' nil x (node' nil rx nil)
rfl
case nil.node.nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
this : size rrl = 0 ∧ size rrr = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs rrl rrx rrr))
        else node' nil x (node' nil rx (node rrs rrl rrx rrr))
case nil.node.nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs rrl rrx rrr))
        else node' nil x (node' nil rx (node rrs rrl rrx rrr))
have : size rrl = 0 ∧ size rrr = 0 := by
  have := balancedSz_zero.1 hr.1.symm
  rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case nil.node.nil.node.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs nil rrx rrr))
sr : Sized (node rs nil rx (node rrs nil rrx rrr))
this : size nil = 0 ∧ size rrr = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs nil rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs nil rrx rrr))
        else node' nil x (node' nil rx (node rrs nil rrx rrr))
case nil.node.nil.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
this : size rrl = 0 ∧ size rrr = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs rrl rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs rrl rrx rrr))
        else node' nil x (node' nil rx (node rrs rrl rrx rrr))
cases sr.2.2.2.1.size_eq_zero.1 this.1
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
hr : Balanced (node' nil rx (node rrs nil rrx nil))
sr : Sized (node rs nil rx (node rrs nil rrx nil))
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx nil) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx nil))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs nil rrx nil))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs nil rrx nil))
        else node' nil x (node' nil rx (node rrs nil rrx nil))
case nil.node.nil.node.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs nil rrx rrr))
sr : Sized (node rs nil rx (node rrs nil rrx rrr))
this : size nil = 0 ∧ size rrr = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx rrr))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs nil rrx rrr))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs nil rrx rrr))
        else node' nil x (node' nil rx (node rrs nil rrx rrr))
cases sr.2.2.2.2.size_eq_zero.1 this.2
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) =
    if 0 + (0 + 1 + 1) ≤ 1 then node' nil x (node' nil rx (node 1 nil rrx nil))
    else
      if 0 + 1 + 1 > 0 then rotateL nil x (node' nil rx (node 1 nil rrx nil))
      else
        if 0 > delta * (0 + 1 + 1) then rotateR nil x (node' nil rx (node 1 nil rrx nil))
        else node' nil x (node' nil rx (node 1 nil rrx nil))
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
hr : Balanced (node' nil rx (node rrs nil rrx nil))
sr : Sized (node rs nil rx (node rrs nil rrx nil))
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx nil) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' nil x (node' nil rx (node rrs nil rrx nil))
    else
      if 0 + rrs + 1 > 0 then rotateL nil x (node' nil rx (node rrs nil rrx nil))
      else
        if 0 > delta * (0 + rrs + 1) then rotateR nil x (node' nil rx (node rrs nil rrx nil))
        else node' nil x (node' nil rx (node rrs nil rrx nil))
obtain rfl : rrs = 1 := sr.2.2.1
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = node3L nil x nil rx (node 1 nil rrx nil)

case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ size nil < ratio * size (node 1 nil rrx nil)

case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ 0 + 1 + 1 > 0

case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ ¬0 + (0 + 1 + 1) ≤ 1
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) =
    if 0 + (0 + 1 + 1) ≤ 1 then node' nil x (node' nil rx (node 1 nil rrx nil))
    else
      if 0 + 1 + 1 > 0 then rotateL nil x (node' nil rx (node 1 nil rrx nil))
      else
        if 0 > delta * (0 + 1 + 1) then rotateR nil x (node' nil rx (node 1 nil rrx nil))
        else node' nil x (node' nil rx (node 1 nil rrx nil))
rw [if_neg, if_pos, rotateL, if_pos]
no goals
case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ size nil < ratio * size (node 1 nil rrx nil)

case nil.node.nil.node.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ 0 + 1 + 1 > 0

case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ ¬0 + (0 + 1 + 1) ≤ 1
all_goals dsimp only [size]; decide
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
this : size (node rrs rrl rrx rrr) ≤ 1
⊢ size rrl = 0 ∧ size rrr = 0
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
⊢ size rrl = 0 ∧ size rrr = 0
have := balancedSz_zero.1 hr.1.symm
no goals
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' nil rx (node rrs rrl rrx rrr))
sr : Sized (node rs nil rx (node rrs rrl rrx rrr))
this : size (node rrs rrl rrx rrr) ≤ 1
⊢ size rrl = 0 ∧ size rrr = 0
rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
no goals
case nil.node.nil.node.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = node3L nil x nil rx (node 1 nil rrx nil)
rfl
case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ ¬0 + (0 + 1 + 1) ≤ 1
case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ ¬0 + (0 + 1 + 1) ≤ 1
dsimp only [size]
no goals
case nil.node.nil.node.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rrx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' nil rx (node 1 nil rrx nil))
sr : Sized (node rs nil rx (node 1 nil rrx nil))
⊢ ¬0 + (0 + 1 + 1) ≤ 1
decide
case nil.node.node.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
this : size rll = 0 ∧ size rlr = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx nil)
        else node' nil x (node' (node rls rll rlx rlr) rx nil)
case nil.node.node.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx nil)
        else node' nil x (node' (node rls rll rlx rlr) rx nil)
have : size rll = 0 ∧ size rlr = 0 := by
  have := balancedSz_zero.1 hr.1
  rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case nil.node.node.nil.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls nil rlx rlr) rx nil)
sr : Sized (node rs (node rls nil rlx rlr) rx nil)
this : size nil = 0 ∧ size rlr = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls nil rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls nil rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls nil rlx rlr) rx nil)
        else node' nil x (node' (node rls nil rlx rlr) rx nil)
case nil.node.node.nil
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
this : size rll = 0 ∧ size rlr = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx nil)
        else node' nil x (node' (node rls rll rlx rlr) rx nil)
cases sr.2.1.2.1.size_eq_zero.1 this.1
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
hr : Balanced (node' (node rls nil rlx nil) rx nil)
sr : Sized (node rs (node rls nil rlx nil) rx nil)
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls nil rlx nil) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls nil rlx nil) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls nil rlx nil) rx nil)
        else node' nil x (node' (node rls nil rlx nil) rx nil)
case nil.node.node.nil.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls nil rlx rlr) rx nil)
sr : Sized (node rs (node rls nil rlx rlr) rx nil)
this : size nil = 0 ∧ size rlr = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls nil rlx rlr) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls nil rlx rlr) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls nil rlx rlr) rx nil)
        else node' nil x (node' (node rls nil rlx rlr) rx nil)
cases sr.2.1.2.2.size_eq_zero.1 this.2
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (1 + 1) ≤ 1 then node' nil x (node' (node 1 nil rlx nil) rx nil)
    else
      if 1 + 1 > 0 then rotateL nil x (node' (node 1 nil rlx nil) rx nil)
      else
        if 0 > delta * (1 + 1) then rotateR nil x (node' (node 1 nil rlx nil) rx nil)
        else node' nil x (node' (node 1 nil rlx nil) rx nil)
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
hr : Balanced (node' (node rls nil rlx nil) rx nil)
sr : Sized (node rs (node rls nil rlx nil) rx nil)
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' nil x (node' (node rls nil rlx nil) rx nil)
    else
      if rls + 1 > 0 then rotateL nil x (node' (node rls nil rlx nil) rx nil)
      else
        if 0 > delta * (rls + 1) then rotateR nil x (node' (node rls nil rlx nil) rx nil)
        else node' nil x (node' (node rls nil rlx nil) rx nil)
obtain rfl : rls = 1 := sr.2.1.1
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = node4L nil x (node 1 nil rlx nil) rx nil

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬size (node 1 nil rlx nil) < ratio * size nil

case nil.node.node.nil.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ 1 + 1 > 0

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬0 + (1 + 1) ≤ 1
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (1 + 1) ≤ 1 then node' nil x (node' (node 1 nil rlx nil) rx nil)
    else
      if 1 + 1 > 0 then rotateL nil x (node' (node 1 nil rlx nil) rx nil)
      else
        if 0 > delta * (1 + 1) then rotateR nil x (node' (node 1 nil rlx nil) rx nil)
        else node' nil x (node' (node 1 nil rlx nil) rx nil)
rw [if_neg, if_pos, rotateL, if_neg]
no goals
case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬size (node 1 nil rlx nil) < ratio * size nil

case nil.node.node.nil.refl.refl.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ 1 + 1 > 0

case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬0 + (1 + 1) ≤ 1
all_goals dsimp only [size]; decide
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
this : size (node rls rll rlx rlr) ≤ 1
⊢ size rll = 0 ∧ size rlr = 0
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
⊢ size rll = 0 ∧ size rlr = 0
have := balancedSz_zero.1 hr.1
no goals
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
this : size (node rls rll rlx rlr) ≤ 1
⊢ size rll = 0 ∧ size rlr = 0
rwa [size, sr.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
no goals
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = node4L nil x (node 1 nil rlx nil) rx nil
rfl
case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬0 + (1 + 1) ≤ 1
case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬0 + (1 + 1) ≤ 1
dsimp only [size]
no goals
case nil.node.node.nil.refl.refl.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx rlx : α
this : size nil = 0 ∧ size nil = 0
hr : Balanced (node' (node 1 nil rlx nil) rx nil)
sr : Sized (node rs (node 1 nil rlx nil) rx nil)
⊢ ¬0 + (1 + 1) ≤ 1
decide
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if 0 + (rls + rrs + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
    else
      if rls + rrs + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (rls + rrs + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
        else node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
    else
      if rls + rrs + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (rls + rrs + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
        else node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
symm
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if size (node rls rll rlx rlr) < ratio * size (node rrs rrl rrx rrr) then
      node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))

case nil.node.node.node.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ rls + rrs + 1 > 0

case nil.node.node.node.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ ¬rls + rrs + 1 ≤ 1
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if 0 + (rls + rrs + 1) ≤ 1 then node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
    else
      if rls + rrs + 1 > 0 then rotateL nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
      else
        if 0 > delta * (rls + rrs + 1) then rotateR nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
        else node' nil x (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
rw [zero_add, if_neg, if_pos, rotateL]
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if size (node rls rll rlx rlr) < ratio * size (node rrs rrl rrx rrr) then
      node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
dsimp only [size_node]
case nil.node.node.node.inl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : rls < ratio * rrs
⊢ node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

case nil.node.node.node.inr
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : ¬rls < ratio * rrs
⊢ node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
      (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
case nil.node.node.node
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
split_ifs
case nil.node.node.node.inl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : rls < ratio * rrs
⊢ rls + 1 + rrs = rls + rrs + 1
case nil.node.node.node.inl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : rls < ratio * rrs
⊢ node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
simp [node3L, node']
no goals
case nil.node.node.node.inl
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : rls < ratio * rrs
⊢ rls + 1 + rrs = rls + rrs + 1
abel
case nil.node.node.node.inr
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : ¬rls < ratio * rrs
⊢ size rll + 1 + (size rlr + rrs + 1) = size rll + size rlr + 1 + rrs + 1
case nil.node.node.node.inr
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : ¬rls < ratio * rrs
⊢ node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (size rll + 1) nil x rll) rlx
      (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
simp [node4L, node', sr.2.1.1]
no goals
case nil.node.node.node.inr
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
h✝ : ¬rls < ratio * rrs
⊢ size rll + 1 + (size rlr + rrs + 1) = size rll + size rlr + 1 + rrs + 1
abel
no goals
case nil.node.node.node.hc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ rls + rrs + 1 > 0
apply Nat.zero_lt_succ
no goals
case nil.node.node.node.hnc
α : Type u_1
x : α
hl : Balanced nil
sl : Sized nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node' (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
⊢ ¬rls + rrs + 1 ≤ 1
exact not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
hr : Balanced nil
sr : Sized nil
⊢ balance (node ls ll lx lr) x nil = balance' (node ls ll lx lr) x nil

case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance (node ls ll lx lr) x (node rs rl rx rr) = balance' (node ls ll lx lr) x (node rs rl rx rr)
case node
α : Type u_1
x : α
r : Ordnode α
hr : Balanced r
sr : Sized r
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
⊢ balance (node ls ll lx lr) x r = balance' (node ls ll lx lr) x r
cases' r with rs rl rx rr
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node' ll lx lr)
sl : Sized (node ls ll lx lr)
hr : Balanced nil
sr : Sized nil
⊢ balance (node' ll lx lr) x nil = balance' (node' ll lx lr) x nil
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
hr : Balanced nil
sr : Sized nil
⊢ balance (node ls ll lx lr) x nil = balance' (node ls ll lx lr) x nil
rw [sl.eq_node'] at hl ⊢
case node.nil.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
hl : Balanced (node' nil lx nil)
sl : Sized (node ls nil lx nil)
⊢ node 2 (node' nil lx nil) x nil =
    if 1 ≤ 1 then node' (node' nil lx nil) x nil
    else
      if 0 > delta * (0 + 1) then rotateL (node' nil lx nil) x nil
      else if 0 + 1 > 0 then rotateR (node' nil lx nil) x nil else node' (node' nil lx nil) x nil

case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs lrl lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs lrl lrx lrr)) x nil
        else node' (node' nil lx (node lrs lrl lrx lrr)) x nil

case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls lll llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls lll llx llr) lx nil) x nil
        else node' (node' (node lls lll llx llr) lx nil) x nil

case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)) =
    if lls + lrs + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (lls + lrs + 1) then rotateL (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
      else
        if lls + lrs + 1 > 0 then rotateR (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
        else node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node' ll lx lr)
sl : Sized (node ls ll lx lr)
hr : Balanced nil
sr : Sized nil
⊢ balance (node' ll lx lr) x nil = balance' (node' ll lx lr) x nil
cases' ll with lls lll llx llr <;> cases' lr with lrs lrl lrx lrr <;>
  dsimp [balance, balance']
no goals
case node.nil.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
hl : Balanced (node' nil lx nil)
sl : Sized (node ls nil lx nil)
⊢ node 2 (node' nil lx nil) x nil =
    if 1 ≤ 1 then node' (node' nil lx nil) x nil
    else
      if 0 > delta * (0 + 1) then rotateL (node' nil lx nil) x nil
      else if 0 + 1 > 0 then rotateR (node' nil lx nil) x nil else node' (node' nil lx nil) x nil
rfl
case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
this : size lrl = 0 ∧ size lrr = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs lrl lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs lrl lrx lrr)) x nil
        else node' (node' nil lx (node lrs lrl lrx lrr)) x nil
case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs lrl lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs lrl lrx lrr)) x nil
        else node' (node' nil lx (node lrs lrl lrx lrr)) x nil
have : size lrl = 0 ∧ size lrr = 0 := by
  have := balancedSz_zero.1 hl.1.symm
  rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case node.nil.nil.node.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs nil lrx lrr))
sl : Sized (node ls nil lx (node lrs nil lrx lrr))
this : size nil = 0 ∧ size lrr = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs nil lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs nil lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs nil lrx lrr)) x nil
        else node' (node' nil lx (node lrs nil lrx lrr)) x nil
case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
this : size lrl = 0 ∧ size lrr = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs lrl lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs lrl lrx lrr)) x nil
        else node' (node' nil lx (node lrs lrl lrx lrr)) x nil
cases sl.2.2.2.1.size_eq_zero.1 this.1
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrx : α
hl : Balanced (node' nil lx (node lrs nil lrx nil))
sl : Sized (node ls nil lx (node lrs nil lrx nil))
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs nil lrx nil)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs nil lrx nil)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs nil lrx nil)) x nil
        else node' (node' nil lx (node lrs nil lrx nil)) x nil
case node.nil.nil.node.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs nil lrx lrr))
sl : Sized (node ls nil lx (node lrs nil lrx lrr))
this : size nil = 0 ∧ size lrr = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs nil lrx lrr)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs nil lrx lrr)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs nil lrx lrr)) x nil
        else node' (node' nil lx (node lrs nil lrx lrr)) x nil
cases sl.2.2.2.2.size_eq_zero.1 this.2
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + 1 + 1 ≤ 1 then node' (node' nil lx (node 1 nil lrx nil)) x nil
    else
      if 0 > delta * (0 + 1 + 1) then rotateL (node' nil lx (node 1 nil lrx nil)) x nil
      else
        if 0 + 1 + 1 > 0 then rotateR (node' nil lx (node 1 nil lrx nil)) x nil
        else node' (node' nil lx (node 1 nil lrx nil)) x nil
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrx : α
hl : Balanced (node' nil lx (node lrs nil lrx nil))
sl : Sized (node ls nil lx (node lrs nil lrx nil))
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then node' (node' nil lx (node lrs nil lrx nil)) x nil
    else
      if 0 > delta * (0 + lrs + 1) then rotateL (node' nil lx (node lrs nil lrx nil)) x nil
      else
        if 0 + lrs + 1 > 0 then rotateR (node' nil lx (node lrs nil lrx nil)) x nil
        else node' (node' nil lx (node lrs nil lrx nil)) x nil
obtain rfl : lrs = 1 := sl.2.2.1
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (node 1 nil lrx nil) x nil

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬size (node 1 nil lrx nil) < ratio * size nil

case node.nil.nil.node.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ 0 + 1 + 1 > 0

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 > delta * (0 + 1 + 1)

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 + 1 + 1 ≤ 1
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + 1 + 1 ≤ 1 then node' (node' nil lx (node 1 nil lrx nil)) x nil
    else
      if 0 > delta * (0 + 1 + 1) then rotateL (node' nil lx (node 1 nil lrx nil)) x nil
      else
        if 0 + 1 + 1 > 0 then rotateR (node' nil lx (node 1 nil lrx nil)) x nil
        else node' (node' nil lx (node 1 nil lrx nil)) x nil
rw [if_neg, if_neg, if_pos, rotateR, if_neg]
no goals
case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬size (node 1 nil lrx nil) < ratio * size nil

case node.nil.nil.node.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ 0 + 1 + 1 > 0

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 > delta * (0 + 1 + 1)

case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 + 1 + 1 ≤ 1
all_goals dsimp only [size]; decide
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
this : size (node lrs lrl lrx lrr) ≤ 1
⊢ size lrl = 0 ∧ size lrr = 0
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
⊢ size lrl = 0 ∧ size lrr = 0
have := balancedSz_zero.1 hl.1.symm
no goals
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' nil lx (node lrs lrl lrx lrr))
sl : Sized (node ls nil lx (node lrs lrl lrx lrr))
this : size (node lrs lrl lrx lrr) ≤ 1
⊢ size lrl = 0 ∧ size lrr = 0
rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
no goals
case node.nil.nil.node.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (node 1 nil lrx nil) x nil
rfl
case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 + 1 + 1 ≤ 1
case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 + 1 + 1 ≤ 1
dsimp only [size]
no goals
case node.nil.nil.node.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lrx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' nil lx (node 1 nil lrx nil))
sl : Sized (node ls nil lx (node 1 nil lrx nil))
⊢ ¬0 + 1 + 1 ≤ 1
decide
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
this : size lll = 0 ∧ size llr = 0
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls lll llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls lll llx llr) lx nil) x nil
        else node' (node' (node lls lll llx llr) lx nil) x nil
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls lll llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls lll llx llr) lx nil) x nil
        else node' (node' (node lls lll llx llr) lx nil) x nil
have : size lll = 0 ∧ size llr = 0 := by
  have := balancedSz_zero.1 hl.1
  rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case node.nil.node.nil.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls nil llx llr) lx nil)
sl : Sized (node ls (node lls nil llx llr) lx nil)
this : size nil = 0 ∧ size llr = 0
⊢ node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls nil llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls nil llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls nil llx llr) lx nil) x nil
        else node' (node' (node lls nil llx llr) lx nil) x nil
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
this : size lll = 0 ∧ size llr = 0
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls lll llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls lll llx llr) lx nil) x nil
        else node' (node' (node lls lll llx llr) lx nil) x nil
cases sl.2.1.2.1.size_eq_zero.1 this.1
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
llx : α
hl : Balanced (node' (node lls nil llx nil) lx nil)
sl : Sized (node ls (node lls nil llx nil) lx nil)
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls nil llx nil) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls nil llx nil) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls nil llx nil) lx nil) x nil
        else node' (node' (node lls nil llx nil) lx nil) x nil
case node.nil.node.nil.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls nil llx llr) lx nil)
sl : Sized (node ls (node lls nil llx llr) lx nil)
this : size nil = 0 ∧ size llr = 0
⊢ node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls nil llx llr) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls nil llx llr) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls nil llx llr) lx nil) x nil
        else node' (node' (node lls nil llx llr) lx nil) x nil
cases sl.2.1.2.2.size_eq_zero.1 this.2
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) =
    if 1 + 1 ≤ 1 then node' (node' (node 1 nil llx nil) lx nil) x nil
    else
      if 0 > delta * (1 + 1) then rotateL (node' (node 1 nil llx nil) lx nil) x nil
      else
        if 1 + 1 > 0 then rotateR (node' (node 1 nil llx nil) lx nil) x nil
        else node' (node' (node 1 nil llx nil) lx nil) x nil
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
llx : α
hl : Balanced (node' (node lls nil llx nil) lx nil)
sl : Sized (node ls (node lls nil llx nil) lx nil)
this : size nil = 0 ∧ size nil = 0
⊢ node 3 (node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then node' (node' (node lls nil llx nil) lx nil) x nil
    else
      if 0 > delta * (lls + 1) then rotateL (node' (node lls nil llx nil) lx nil) x nil
      else
        if lls + 1 > 0 then rotateR (node' (node lls nil llx nil) lx nil) x nil
        else node' (node' (node lls nil llx nil) lx nil) x nil
obtain rfl : lls = 1 := sl.2.1.1
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = node3R (node 1 nil llx nil) lx nil x nil

case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ size nil < ratio * size (node 1 nil llx nil)

case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ 1 + 1 > 0

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬0 > delta * (1 + 1)

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬1 + 1 ≤ 1
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) =
    if 1 + 1 ≤ 1 then node' (node' (node 1 nil llx nil) lx nil) x nil
    else
      if 0 > delta * (1 + 1) then rotateL (node' (node 1 nil llx nil) lx nil) x nil
      else
        if 1 + 1 > 0 then rotateR (node' (node 1 nil llx nil) lx nil) x nil
        else node' (node' (node 1 nil llx nil) lx nil) x nil
rw [if_neg, if_neg, if_pos, rotateR, if_pos]
no goals
case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ size nil < ratio * size (node 1 nil llx nil)

case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ 1 + 1 > 0

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬0 > delta * (1 + 1)

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬1 + 1 ≤ 1
all_goals dsimp only [size]; decide
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
this : size (node lls lll llx llr) ≤ 1
⊢ size lll = 0 ∧ size llr = 0
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
⊢ size lll = 0 ∧ size llr = 0
have := balancedSz_zero.1 hl.1
no goals
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
this : size (node lls lll llx llr) ≤ 1
⊢ size lll = 0 ∧ size llr = 0
rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
no goals
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = node3R (node 1 nil llx nil) lx nil x nil
rfl
case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬1 + 1 ≤ 1
case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬1 + 1 ≤ 1
dsimp only [size]
no goals
case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
llx : α
this : size nil = 0 ∧ size nil = 0
hl : Balanced (node' (node 1 nil llx nil) lx nil)
sl : Sized (node ls (node 1 nil llx nil) lx nil)
⊢ ¬1 + 1 ≤ 1
decide
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lls + lrs + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (lls + lrs + 1) then rotateL (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
      else
        if lls + lrs + 1 > 0 then rotateR (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
        else node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)) =
    if lls + lrs + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (lls + lrs + 1) then rotateL (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
      else
        if lls + lrs + 1 > 0 then rotateR (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
        else node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
symm
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if size (node lrs lrl lrx lrr) < ratio * size (node lls lll llx llr) then
      node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)

case node.nil.node.node.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ lls + lrs + 1 > 0

case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ ¬0 > delta * (lls + lrs + 1)

case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ ¬lls + lrs + 1 ≤ 1
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lls + lrs + 1 ≤ 1 then node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
    else
      if 0 > delta * (lls + lrs + 1) then rotateL (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
      else
        if lls + lrs + 1 > 0 then rotateR (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil
        else node' (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)
rw [if_neg, if_neg, if_pos, rotateR]
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lrs < ratio * lls then node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if size (node lrs lrl lrx lrr) < ratio * size (node lls lll llx llr) then
      node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)
dsimp only [size_node]
case node.nil.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : lrs < ratio * lls
⊢ node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)

case node.nil.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : ¬lrs < ratio * lls
⊢ node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
      (node (size lrr + 1) lrr x nil)
case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ (if lrs < ratio * lls then node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + 1) lrr x nil)
split_ifs
case node.nil.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : lrs < ratio * lls
⊢ lls + (lrs + 1) = lls + lrs + 1
case node.nil.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : lrs < ratio * lls
⊢ node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
simp [node3R, node']
no goals
case node.nil.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : lrs < ratio * lls
⊢ lls + (lrs + 1) = lls + lrs + 1
abel
case node.nil.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : ¬lrs < ratio * lls
⊢ lls + size lrl + 1 + (size lrr + 1) = lls + (size lrl + size lrr + 1) + 1
case node.nil.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : ¬lrs < ratio * lls
⊢ node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
      (node (size lrr + 1) lrr x nil)
simp [node4R, node', sl.2.2.1]
no goals
case node.nil.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
h✝ : ¬lrs < ratio * lls
⊢ lls + size lrl + 1 + (size lrr + 1) = lls + (size lrl + size lrr + 1) + 1
abel
no goals
case node.nil.node.node.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ lls + lrs + 1 > 0
apply Nat.zero_lt_succ
no goals
case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ ¬0 > delta * (lls + lrs + 1)
apply Nat.not_lt_zero
no goals
case node.nil.node.node.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced nil
sr : Sized nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node' (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
⊢ ¬lls + lrs + 1 ≤ 1
exact not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if ls + rs ≤ 1 then node' (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
      else
        if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
        else node' (node ls ll lx lr) x (node rs rl rx rr)
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ balance (node ls ll lx lr) x (node rs rl rx rr) = balance' (node ls ll lx lr) x (node rs rl rx rr)
simp [balance, balance']
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if ls + rs ≤ 1 then node' (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
      else
        if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
        else node' (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if ls + rs ≤ 1 then node' (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
      else
        if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
        else node' (node ls ll lx lr) x (node rs rl rx rr)
symm
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
      else node' (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

case node.node.hnc
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ ¬ls + rs ≤ 1
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if ls + rs ≤ 1 then node' (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
      else
        if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
        else node' (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
rw [if_neg]
case node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
⊢ rotateL (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      rl (_ : id rl = id rl)

case node.node.inr.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ rotateR (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            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 + Ordnode.size l + 1) ll lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      ll (_ : id ll = id ll)

case node.node.inr.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : ¬delta * rs < ls
⊢ node' (node ls ll lx lr) x (node rs rl rx rr) = node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ (if delta * ls < rs then rotateL (node ls ll lx lr) x (node rs rl rx rr)
    else
      if delta * rs < ls then rotateR (node ls ll lx lr) x (node rs rl rx rr)
      else node' (node ls ll lx lr) x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
        (fun size l x_1 r l_ih r_ih h =>
          rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
            (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
              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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                  (node (Ordnode.size r + size_1 + 1) r rx rr))
            rr (_ : id rr = id rr))
        rl (_ : id rl = id rl)
    else
      if delta * rs < ls then
        rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
          (fun size l x_1 r l_ih r_ih h =>
            rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
              (fun size_1 l x_2 r l_ih r_ih h =>
                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 + Ordnode.size l + 1) ll lx l) x_2
                    (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
              lr (_ : id lr = id lr))
          ll (_ : id ll = id ll)
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
split_ifs with h h_1
case node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
rd : delta ≤ size rl + size rr
⊢ rotateL (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      rl (_ : id rl = id rl)
case node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
⊢ rotateL (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      rl (_ : id rl = id rl)
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
case node.node.inl.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : Balanced (node rs nil rx rr)
sr : Sized (node rs nil rx rr)
rd : delta ≤ size nil + size rr
⊢ rotateL (node ls ll lx lr) x (node rs nil rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      nil (_ : id nil = id nil)

case node.node.inl.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx rr)
sr : Sized (node rs (node rls rll rlx rlr) rx rr)
rd : delta ≤ size (node rls rll rlx rlr) + size rr
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx rr) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))
case node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
rd : delta ≤ size rl + size rr
⊢ rotateL (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => rl = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            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 + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      rl (_ : id rl = id rl)
cases' rl with rls rll rlx rlr
case node.node.inl.node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
rd : delta ≤ size (node rls rll rlx rlr) + size nil
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx nil) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx nil
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx nil))
          nil (_ : id nil = id nil))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))

case node.node.inl.node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => node rrs rrl rrx rrr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx
                (node rrs rrl rrx rrr)
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx (node rrs rrl rrx rrr)))
          (node rrs rrl rrx rrr) (_ : id (node rrs rrl rrx rrr) = id (node rrs rrl rrx rrr)))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))
case node.node.inl.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx rr)
sr : Sized (node rs (node rls rll rlx rlr) rx rr)
rd : delta ≤ size (node rls rll rlx rlr) + size rr
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx rr) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))
cases' rr with rrs rrl rrx rrr
case node.node.inl.node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
⊢ (if rls < ratio * rrs then node3L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (ls + rs + 1) (node (ls + size rll + 1) (node ls ll lx lr) x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
case node.node.inl.node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => node rrs rrl rrx rrr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx
                (node rrs rrl rrx rrr)
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx (node rrs rrl rrx rrr)))
          (node rrs rrl rrx rrr) (_ : id (node rrs rrl rrx rrr) = id (node rrs rrl rrx rrr)))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))
dsimp [rotateL]
case node.node.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : rls < ratio * rrs
⊢ node3L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

case node.node.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : ¬rls < ratio * rrs
⊢ node4L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + size rll + 1) (node ls ll lx lr) x rll) rlx
      (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
case node.node.inl.node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
⊢ (if rls < ratio * rrs then node3L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (ls + rs + 1) (node (ls + size rll + 1) (node ls ll lx lr) x rll) rlx
        (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
split_ifs
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
this : delta * Nat.succ 0 < rs
⊢ delta ≤ size rl + size rr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
⊢ delta ≤ size rl + size rr
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
no goals
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : delta * ls < rs
this : delta * Nat.succ 0 < rs
⊢ delta ≤ size rl + size rr
rwa [sr.1, Nat.lt_succ_iff] at this
case node.node.inl.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : Balanced (node rs nil rx rr)
sr : Sized (node rs nil rx rr)
rd : delta ≤ size rr
⊢ rotateL (node ls ll lx lr) x (node rs nil rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      nil (_ : id nil = id nil)
case node.node.inl.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : Balanced (node rs nil rx rr)
sr : Sized (node rs nil rx rr)
rd : delta ≤ size nil + size rr
⊢ rotateL (node ls ll lx lr) x (node rs nil rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      nil (_ : id nil = id nil)
rw [size, zero_add] at rd
no goals
case node.node.inl.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : Balanced (node rs nil rx rr)
sr : Sized (node rs nil rx rr)
rd : delta ≤ size rr
⊢ rotateL (node ls ll lx lr) x (node rs nil rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => rr = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x nil) rx rr
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx rr))
          rr (_ : id rr = id rr))
      nil (_ : id nil = id nil)
exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)
no goals
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : Balanced (node rs nil rx rr)
sr : Sized (node rs nil rx rr)
rd : delta ≤ size rr
⊢ ¬delta ≤ 1
decide
no goals
case node.node.inl.node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
rd : delta ≤ size (node rls rll rlx rlr) + size nil
⊢ rotateL (node ls ll lx lr) x (node rs (node rls rll rlx rlr) rx nil) =
    rec (motive := fun t => node rls rll rlx rlr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
          (fun size_1 l_1 x_2 r_1 l_ih r_ih h =>
            if size < ratio * size_1 then
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx nil
            else
              node (ls + rs + 1) (node (ls + Ordnode.size l + 1) (node ls ll lx lr) x l) x_1
                (node (Ordnode.size r + size_1 + 1) r rx nil))
          nil (_ : id nil = id nil))
      (node rls rll rlx rlr) (_ : id (node rls rll rlx rlr) = id (node rls rll rlx rlr))
exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)
no goals
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx nil)
sr : Sized (node rs (node rls rll rlx rlr) rx nil)
rd : delta ≤ size (node rls rll rlx rlr) + size nil
⊢ ¬delta ≤ 1
decide
case node.node.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : rls < ratio * rrs
⊢ ls + rls + 1 + rrs = ls + (rls + rrs + 1)
case node.node.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : rls < ratio * rrs
⊢ node3L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
simp [node3L, node', sr.1]
no goals
case node.node.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : rls < ratio * rrs
⊢ ls + rls + 1 + rrs = ls + (rls + rrs + 1)
abel
case node.node.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : ¬rls < ratio * rrs
⊢ ls + size rll + 1 + (size rlr + rrs + 1) = ls + (size rll + size rlr + 1 + rrs + 1)
case node.node.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : ¬rls < ratio * rrs
⊢ node4L (node ls ll lx lr) x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + size rll + 1) (node ls ll lx lr) x rll) rlx
      (node (size rlr + rrs + 1) rlr rx (node rrs rrl rrx rrr))
simp [node4L, node', sr.1, sr.2.1.1]
no goals
case node.node.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : Balanced (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
sr : Sized (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr))
rd : delta ≤ size (node rls rll rlx rlr) + size (node rrs rrl rrx rrr)
h✝ : ¬rls < ratio * rrs
⊢ ls + size rll + 1 + (size rlr + rrs + 1) = ls + (size rll + size rlr + 1 + rrs + 1)
abel
case node.node.inr.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
ld : delta ≤ size ll + size lr
⊢ rotateR (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            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 + Ordnode.size l + 1) ll lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      ll (_ : id ll = id ll)
case node.node.inr.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ rotateR (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            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 + Ordnode.size l + 1) ll lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      ll (_ : id ll = id ll)
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
case node.node.inr.inl.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : Balanced (node ls nil lx lr)
sl : Sized (node ls nil lx lr)
ld : delta ≤ size nil + size lr
⊢ rotateR (node ls nil lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) nil lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      nil (_ : id nil = id nil)

case node.node.inr.inl.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx lr)
sl : Sized (node ls (node lls lll llx llr) lx lr)
ld : delta ≤ size (node lls lll llx llr) + size lr
⊢ rotateR (node ls (node lls lll llx llr) lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))
case node.node.inr.inl
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
ld : delta ≤ size ll + size lr
⊢ rotateR (node ls ll lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => ll = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            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 + Ordnode.size l + 1) ll lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      ll (_ : id ll = id ll)
cases' ll with lls lll llx llr
case node.node.inr.inl.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
ld : delta ≤ size (node lls lll llx llr) + size nil
⊢ rotateR (node ls (node lls lll llx llr) lx nil) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) nil x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          nil (_ : id nil = id nil))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))

case node.node.inr.inl.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
⊢ rotateR (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => node lrs lrl lrx lrr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx
                (node (size_1 + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          (node lrs lrl lrx lrr) (_ : id (node lrs lrl lrx lrr) = id (node lrs lrl lrx lrr)))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))
case node.node.inr.inl.node
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx lr)
sl : Sized (node ls (node lls lll llx llr) lx lr)
ld : delta ≤ size (node lls lll llx llr) + size lr
⊢ rotateR (node ls (node lls lll llx llr) lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))
cases' lr with lrs lrl lrx lrr
case node.node.inr.inl.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
⊢ (if lrs < ratio * lls then node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr)) =
    if lrs < ratio * lls then
      node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
    else
      node (ls + rs + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + rs + 1) lrr x (node rs rl rx rr))
case node.node.inr.inl.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
⊢ rotateR (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => node lrs lrl lrx lrr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx
                (node (size_1 + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          (node lrs lrl lrx lrr) (_ : id (node lrs lrl lrx lrr) = id (node lrs lrl lrx lrr)))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))
dsimp [rotateR]
case node.node.inr.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : lrs < ratio * lls
⊢ node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))

case node.node.inr.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : ¬lrs < ratio * lls
⊢ node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
      (node (size lrr + rs + 1) lrr x (node rs rl rx rr))
case node.node.inr.inl.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
⊢ (if lrs < ratio * lls then node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr)) =
    if lrs < ratio * lls then
      node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
    else
      node (ls + rs + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
        (node (size lrr + rs + 1) lrr x (node rs rl rx rr))
split_ifs
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ls
⊢ delta ≤ size ll + size lr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ delta ≤ size ll + size lr
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
no goals
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ls
⊢ delta ≤ size ll + size lr
rwa [sl.1, Nat.lt_succ_iff] at this
case node.node.inr.inl.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : Balanced (node ls nil lx lr)
sl : Sized (node ls nil lx lr)
ld : delta ≤ size lr
⊢ rotateR (node ls nil lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) nil lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      nil (_ : id nil = id nil)
case node.node.inr.inl.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : Balanced (node ls nil lx lr)
sl : Sized (node ls nil lx lr)
ld : delta ≤ size nil + size lr
⊢ rotateR (node ls nil lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) nil lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      nil (_ : id nil = id nil)
rw [size, zero_add] at ld
no goals
case node.node.inr.inl.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : Balanced (node ls nil lx lr)
sl : Sized (node ls nil lx lr)
ld : delta ≤ size lr
⊢ rotateR (node ls nil lx lr) x (node rs rl rx rr) =
    rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => lr = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then node (ls + rs + 1) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) nil lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          lr (_ : id lr = id lr))
      nil (_ : id nil = id nil)
exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)
no goals
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
hl : Balanced (node ls nil lx lr)
sl : Sized (node ls nil lx lr)
ld : delta ≤ size lr
⊢ ¬delta ≤ 1
decide
no goals
case node.node.inr.inl.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
ld : delta ≤ size (node lls lll llx llr) + size nil
⊢ rotateR (node ls (node lls lll llx llr) lx nil) x (node rs rl rx rr) =
    rec (motive := fun t => node lls lll llx llr = t → Ordnode α) (fun h => nil)
      (fun size l x_1 r l_ih r_ih h =>
        rec (motive := fun t => nil = t → Ordnode α) (fun h => nil)
          (fun size_1 l x_2 r l_ih r_ih h =>
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) nil x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + Ordnode.size l + 1) (node lls lll llx llr) lx l) x_2
                (node (Ordnode.size r + rs + 1) r x (node rs rl rx rr)))
          nil (_ : id nil = id nil))
      (node lls lll llx llr) (_ : id (node lls lll llx llr) = id (node lls lll llx llr))
exact absurd (le_trans ld (balancedSz_zero.1 hl.1)) (by decide)
no goals
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx nil)
sl : Sized (node ls (node lls lll llx llr) lx nil)
ld : delta ≤ size (node lls lll llx llr) + size nil
⊢ ¬delta ≤ 1
decide
case node.node.inr.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : lrs < ratio * lls
⊢ lls + (lrs + rs + 1) = lls + lrs + 1 + rs
case node.node.inr.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : lrs < ratio * lls
⊢ node3R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
simp [node3R, node', sl.1]
no goals
case node.node.inr.inl.node.node.inl
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : lrs < ratio * lls
⊢ lls + (lrs + rs + 1) = lls + lrs + 1 + rs
abel
case node.node.inr.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : ¬lrs < ratio * lls
⊢ lls + size lrl + 1 + (size lrr + rs + 1) = lls + (size lrl + size lrr + 1) + 1 + rs
case node.node.inr.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : ¬lrs < ratio * lls
⊢ node4R (node lls lll llx llr) lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node (lls + size lrl + 1) (node lls lll llx llr) lx lrl) lrx
      (node (size lrr + rs + 1) lrr x (node rs rl rx rr))
simp [node4R, node', sl.1, sl.2.2.1]
no goals
case node.node.inr.inl.node.node.inr
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : Balanced (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
sl : Sized (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr))
ld : delta ≤ size (node lls lll llx llr) + size (node lrs lrl lrx lrr)
h✝ : ¬lrs < ratio * lls
⊢ lls + size lrl + 1 + (size lrr + rs + 1) = lls + (size lrl + size lrr + 1) + 1 + rs
abel
no goals
case node.node.inr.inr
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
h : ¬delta * ls < rs
h_1 : ¬delta * rs < ls
⊢ node' (node ls ll lx lr) x (node rs rl rx rr) = node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
simp [node']
no goals
case node.node.hnc
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Balanced (node ls ll lx lr)
sl : Sized (node ls ll lx lr)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Balanced (node rs rl rx rr)
sr : Sized (node rs rl rx rr)
⊢ ¬ls + rs ≤ 1
exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))