-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
node :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (if ls > delta * rs 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
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (rs + size_1 + 1) lr x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (size + l.size + 1) ll lx l) x_2
                    (Ordnode.node (r.size + rs + 1) r x (Ordnode.node rs rl rx rr)))
              lr)
          ll
      else Ordnode.node (ls + rs + 1) (Ordnode.node ls ll lx lr) x (Ordnode.node rs rl rx rr)))
    (if ls > delta * rs 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
                Ordnode.node (rs + ls + 1)
                  (Ordnode.node (rs + size_1 + 1) (Ordnode.node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
              else
                Ordnode.node (rs + ls + 1) (Ordnode.node (rs + l.size + 1) (Ordnode.node rs rr.dual rx rl.dual) x l) x_2
                  (Ordnode.node (r.size + size + 1) r lx ll.dual))
            lr.dual)
        ll.dual
    else Ordnode.node (rs + ls + 1) (Ordnode.node rs rr.dual rx rl.dual) x (Ordnode.node ls lr.dual lx ll.dual))
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node rs rl rx rr))
        (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node ls ll lx lr)) (Ordnode.singleton x)
          fun (ls_1 : ℕ) (ll_1 : Ordnode α) (lx_1 : α) (lr_1 : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll_1)
            (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) lr_1 (Ordnode.node 2 (Ordnode.node ls ll lx lr) x nil)
              fun (size : ℕ) (l : Ordnode α) (lrx : α) (r : Ordnode α) ↦
              Ordnode.node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun (lls : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr_1)
              (Ordnode.node 3 ll_1 lx_1 (Ordnode.singleton x))
              fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
              if lrs < ratio * lls then Ordnode.node (ls_1 + 1) ll_1 lx_1 (Ordnode.node (lrs + 1) lr_1 x nil)
              else
                Ordnode.node (ls_1 + 1) (Ordnode.node (lls + lrl.size + 1) ll_1 lx_1 lrl) lrx
                  (Ordnode.node (lrr.size + 1) lrr x nil))
        fun (rs_1 : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node ls ll lx lr))
          (Ordnode.node (rs_1 + 1) nil x (Ordnode.node rs rl rx rr))
          fun (ls_1 : ℕ) (ll_1 : Ordnode α) (lx_1 : α) (lr_1 : Ordnode α) ↦
          if ls_1 > delta * rs_1 then
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll_1) nil
              fun (lls : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
              casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr_1) nil
                fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
                if lrs < ratio * lls then
                  Ordnode.node (ls_1 + rs_1 + 1) ll_1 lx_1
                    (Ordnode.node (rs_1 + lrs + 1) lr_1 x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls_1 + rs_1 + 1) (Ordnode.node (lls + lrl.size + 1) ll_1 lx_1 lrl) lrx
                    (Ordnode.node (lrr.size + rs_1 + 1) lrr x (Ordnode.node rs rl rx rr))
          else Ordnode.node (ls_1 + rs_1 + 1) (Ordnode.node ls ll lx lr) x (Ordnode.node rs rl rx rr)))
    (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node rs rl rx rr).dual)
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node ls ll lx lr).dual) (Ordnode.singleton x)
        fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr)
          (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) rl (Ordnode.node 2 nil x (Ordnode.node ls ll lx lr).dual)
            fun (size : ℕ) (l : Ordnode α) (rlx : α) (r : Ordnode α) ↦
            Ordnode.node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun (rrs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) (Ordnode.node 3 (Ordnode.singleton x) rx rr)
            fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
            if rls < ratio * rrs then Ordnode.node (rs + 1) (Ordnode.node (rls + 1) nil x rl) rx rr
            else
              Ordnode.node (rs + 1) (Ordnode.node (rll.size + 1) nil x rll) rlx
                (Ordnode.node (rlr.size + rrs + 1) rlr rx rr))
      fun (ls_1 : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
      casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (Ordnode.node ls ll lx lr).dual)
        (Ordnode.node (ls_1 + 1) (Ordnode.node rs rl rx rr).dual x nil)
        fun (rs_1 : ℕ) (rl_1 : Ordnode α) (rx_1 : α) (rr_1 : Ordnode α) ↦
        if rs_1 > delta * ls_1 then
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr_1) nil
            fun (rrs : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl_1) nil
              fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
              if rls < ratio * rrs then
                Ordnode.node (ls_1 + rs_1 + 1) (Ordnode.node (ls_1 + rls + 1) (Ordnode.node rs rl rx rr).dual x rl_1)
                  rx_1 rr_1
              else
                Ordnode.node (ls_1 + rs_1 + 1)
                  (Ordnode.node (ls_1 + rll.size + 1) (Ordnode.node rs rl rx rr).dual x rll) rlx
                  (Ordnode.node (rlr.size + rrs + 1) rlr rx_1 rr_1)
        else Ordnode.node (ls_1 + rs_1 + 1) (Ordnode.node rs rl rx rr).dual x (Ordnode.node ls ll lx lr).dual)

Tactic:
dsimp only [dual, id]

Premises used: id, Ordnode.dual