case nil
α : Type u_1
l : Ordnode α
x : α
sl : Sized l
sr : Sized nil
H1 : size l = 0 → size nil ≤ 1
H2 : 1 ≤ size l → 1 ≤ size nil → size nil ≤ delta * size l
⊢ balanceL l x nil = balance l x nil

case node
α : Type u_1
l : Ordnode α
x : α
sl : Sized l
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
H1 : size l = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size l → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size l
⊢ balanceL l x (node rs rl rx rr) = balance l x (node rs rl rx rr)
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
sl : Sized l
sr : Sized r
H1 : size l = 0 → size r ≤ 1
H2 : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
⊢ balanceL l x r = balance l x r
cases' r with rs rl rx rr
no goals
case nil
α : Type u_1
l : Ordnode α
x : α
sl : Sized l
sr : Sized nil
H1 : size l = 0 → size nil ≤ 1
H2 : 1 ≤ size l → 1 ≤ size nil → size nil ≤ delta * size l
⊢ balanceL l x nil = balance l x nil
rfl
case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)

case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 :
  1 ≤ size (node ls ll lx lr) → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size (node ls ll lx lr)
⊢ balanceL (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
l : Ordnode α
x : α
sl : Sized l
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
H1 : size l = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size l → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size l
⊢ balanceL l x (node rs rl rx rr) = balance l x (node rs rl rx rr)
cases' l with ls ll lx lr
case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
this : size rl = 0 ∧ size rr = 0
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
have : size rl = 0 ∧ size rr = 0 := by
  have := H1 rfl
  rwa [size, sr.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case node.nil.refl
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : Sized nil
sr : Sized (node rs nil rx rr)
H1 : size nil = 0 → size (node rs nil rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx rr) → size (node rs nil rx rr) ≤ delta * size nil
this : size nil = 0 ∧ size rr = 0
⊢ balanceL nil x (node rs nil rx rr) = balance nil x (node rs nil rx rr)
case node.nil
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
this : size rl = 0 ∧ size rr = 0
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
cases sr.2.1.size_eq_zero.1 this.1
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized nil
sr : Sized (node rs nil rx nil)
H1 : size nil = 0 → size (node rs nil rx nil) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx nil) → size (node rs nil rx nil) ≤ delta * size nil
this : size nil = 0 ∧ size nil = 0
⊢ balanceL nil x (node rs nil rx nil) = balance nil x (node rs nil rx nil)
case node.nil.refl
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : Sized nil
sr : Sized (node rs nil rx rr)
H1 : size nil = 0 → size (node rs nil rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx rr) → size (node rs nil rx rr) ≤ delta * size nil
this : size nil = 0 ∧ size rr = 0
⊢ balanceL nil x (node rs nil rx rr) = balance nil x (node rs nil rx rr)
cases sr.2.2.size_eq_zero.1 this.2
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized nil
sr : Sized (node rs nil rx nil)
H1 : size nil = 0 → size (node rs nil rx nil) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx nil) → size (node rs nil rx nil) ≤ delta * size nil
this : size nil = 0 ∧ size nil = 0
⊢ balanceL nil x (node' nil rx nil) = balance nil x (node' nil rx nil)
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized nil
sr : Sized (node rs nil rx nil)
H1 : size nil = 0 → size (node rs nil rx nil) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx nil) → size (node rs nil rx nil) ≤ delta * size nil
this : size nil = 0 ∧ size nil = 0
⊢ balanceL nil x (node rs nil rx nil) = balance nil x (node rs nil rx nil)
rw [sr.eq_node']
no goals
case node.nil.refl.refl
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized nil
sr : Sized (node rs nil rx nil)
H1 : size nil = 0 → size (node rs nil rx nil) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs nil rx nil) → size (node rs nil rx nil) ≤ delta * size nil
this : size nil = 0 ∧ size nil = 0
⊢ balanceL nil x (node' nil rx nil) = balance nil x (node' nil rx nil)
rfl
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
this : size (node rs rl rx rr) ≤ 1
⊢ size rl = 0 ∧ size rr = 0
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
⊢ size rl = 0 ∧ size rr = 0
have := H1 rfl
no goals
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
sl : Sized nil
H1 : size nil = 0 → size (node rs rl rx rr) ≤ 1
H2 : 1 ≤ size nil → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size nil
this : size (node rs rl rx rr) ≤ 1
⊢ size rl = 0 ∧ size rr = 0
rwa [size, sr.1, Nat.succ_le_succ_iff, le_zero_iff, add_eq_zero_iff] at this
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 : ¬rs > delta * ls
⊢ balanceL (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.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 :
  1 ≤ size (node ls ll lx lr) → 1 ≤ size (node rs rl rx rr) → size (node rs rl rx rr) ≤ delta * size (node ls ll lx lr)
⊢ balanceL (node ls ll lx lr) x (node rs rl rx rr) = balance (node ls ll lx lr) x (node rs rl rx rr)
replace H2 : ¬rs > delta * ls := not_lt_of_le (H2 sl.pos sr.pos)
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 : ¬rs > delta * ls
⊢ (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 (rs + size_1 + 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 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 : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 : ¬rs > delta * ls
⊢ balanceL (node ls ll lx lr) x (node rs rl rx rr) = balance (node ls ll lx lr) x (node rs rl rx rr)
simp [balanceL, balance, H2]
no goals
case node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : Sized (node rs rl rx rr)
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : Sized (node ls ll lx lr)
H1 : size (node ls ll lx lr) = 0 → size (node rs rl rx rr) ≤ 1
H2 : ¬rs > delta * ls
⊢ (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 (rs + size_1 + 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 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 <;> simp [add_comm]