-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
sl : (node ls ll lx lr).Sized
H1 : (node ls ll lx lr).size = 0 → (node rs rl rx rr).size ≤ 1
H2 : ¬rs > delta * ls
pos :
  delta * rs < ls →
    Eq (α := Ordnode α)
      (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                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 + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll :
        Ordnode α)
      (rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll :
        Ordnode α)
neg :
  ¬delta * rs < ls →
    node (ls + rs + 1) (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)
⊢ Eq (α := Ordnode α)
    (if delta * rs < ls then
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                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 + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr) :
      Ordnode α)
    (if delta * rs < ls then
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr) :
      Ordnode α)

Tactic:
split_ifs