awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
pos :
  lrs < ratio * lls →
    (node lls lll llx llr).node3R 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)
neg :
  ¬lrs < ratio * lls →
    (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
    else (node lls lll llx llr).node4R 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 + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h : lrs < ratio * lls
pos : lls + (lrs + 1) = lls + lrs + 1
⊢ (node lls lll llx llr).node3R 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)

Tactic:
simp [node3R, node']

Premises used: Ordnode.node', Ordnode.node3R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h : lrs < ratio * lls
⊢ lls + (lrs + 1) = lls + lrs + 1

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h : ¬lrs < ratio * lls
neg : lls + lrl.size + 1 + (lrr.size + 1) = lls + (lrl.size + lrr.size + 1) + 1
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)

Tactic:
simp [node4R, node', sl.2.2.1]

Premises used: Ordnode.node', And.right, And.left, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h : ¬lrs < ratio * lls
⊢ lls + lrl.size + 1 + (lrr.size + 1) = lls + (lrl.size + lrr.size + 1) + 1

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ¬lls + lrs + 1 ≤ 1

Tactic:
not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))

Premises used: add_pos, Nat.succ_lt_succ, Ordnode.Sized.pos, And.right, And.left, not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ ¬lls + lrs + 1 ≤ 1

Tactic:
exact not_le_of_gt (Nat.succ_lt_succ (add_pos sl.2.1.pos sl.2.2.pos))

Premises used: add_pos, Nat.succ_lt_succ, Ordnode.Sized.pos, And.right, And.left, not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (Ordnode.node ls ll lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (Ordnode.node rs rl rx rr).Balanced
sr : (Ordnode.node rs rl rx rr).Sized
node :
  (if delta * ls < 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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
              if size < ratio * size_1 then
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + size + 1) (Ordnode.node ls ll lx lr) x rl) rx rr
              else
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + l.size + 1) (Ordnode.node ls ll lx lr) x l) x_1
                  (Ordnode.node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      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
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (size_1 + rs + 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 + rs ≤ 1 then (Ordnode.node ls ll lx lr).node' x (Ordnode.node rs rl rx rr)
    else
      if delta * ls < rs then (Ordnode.node ls ll lx lr).rotateL x (Ordnode.node rs rl rx rr)
      else
        if delta * rs < ls then (Ordnode.node ls ll lx lr).rotateR x (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).node' x (Ordnode.node rs rl rx rr)
⊢ (Ordnode.node ls ll lx lr).balance x (Ordnode.node rs rl rx rr) =
    (Ordnode.node ls ll lx lr).balance' x (Ordnode.node rs rl rx rr)

Tactic:
simp only [balance, id_eq, balance', size_node, gt_iff_lt]

Premises used: Ordnode.size_node, gt_iff_lt, Ordnode.balance', Ordnode.balance, id_eq
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
⊢ delta * Nat.succ 0 < rs

Tactic:
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 < rs
rwa : ∀ (this : delta * Nat.succ 0 < rl.size + rr.size + 1), delta ≤ rl.size + rr.size
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : delta * Nat.succ 0 ≤ rl.size + rr.size), delta ≤ rl.size + rr.size
⊢ delta ≤ rl.size + rr.size

Tactic:
rwa [sr.1, Nat.lt_succ_iff] at this

Premises used: Nat.lt_succ_iff, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
⊢ delta ≤ rl.size + rr.size

Tactic:
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
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
rd : delta ≤ rl.size + rr.size
pos :
  ∀ (hr : (node rs nil rx rr).Balanced) (sr : (node rs nil rx rr).Sized)
    (rd : delta ≤ size.{u_1} (α := α) nil + rr.size),
    (node ls ll lx lr).rotateL x (node rs nil rx rr) =
      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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
              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 + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        nil
pos₁ :
  ∀ (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) (hr : (node rs (node rls rll rlx rlr) rx rr).Balanced)
    (sr : (node rs (node rls rll rlx rlr) rx rr).Sized) (rd : delta ≤ (node rls rll rlx rlr).size + rr.size),
    (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx rr) =
      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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
              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 + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        (node rls rll rlx rlr)
⊢ (node ls ll lx lr).rotateL x (node rs rl rx rr) =
    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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
            if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      rl

Tactic:
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ size.{u_1} (α := α) nil + rr.size
⊢ delta ≤ rr.size

Tactic:
rw [size, zero_add] at rd

Premises used: Ordnode.size, zero_add
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ ¬delta ≤ 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      nil

Tactic:
exact absurd (le_trans rd (balancedSz_zero.1 hr.1.symm)) (by decide)

Premises used: Ordnode.BalancedSz.symm, Ordnode.balancedSz_zero, absurd, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
rd : delta ≤ (node rls rll rlx rlr).size + size.{u_1} (α := α) nil
⊢ ¬delta ≤ 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
rd : delta ≤ (node rls rll rlx rlr).size + size.{u_1} (α := α) nil
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx nil) =
    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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx nil))
          nil)
      (node rls rll rlx rlr)

Tactic:
exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)

Premises used: Ordnode.balancedSz_zero, absurd, And.left, Iff.mp, le_trans
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
pos :
  (if rls < ratio * rrs then (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else (node ls ll lx lr).node4L 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 + rll.size + 1) (node ls ll lx lr) x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    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_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx (node rrs rrl rrx rrr)))
          (node rrs rrl rrx rrr))
      (node rls rll rlx rlr)

Tactic:
dsimp [rotateL]

Premises used: Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
pos :
  rls < ratio * rrs →
    (node ls ll lx lr).node3L 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)
neg :
  ¬rls < ratio * rrs →
    (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
      node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else (node ls ll lx lr).node4L 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 + rll.size + 1) (node ls ll lx lr) x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h_1 : rls < ratio * rrs
pos : ls + rls + 1 + rrs = ls + (rls + rrs + 1)
⊢ (node ls ll lx lr).node3L 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)

Tactic:
simp [node3L, node', sr.1]

Premises used: Ordnode.node', Ordnode.node3L, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h_1 : rls < ratio * rrs
⊢ ls + rls + 1 + rrs = ls + (rls + rrs + 1)

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h_1 : ¬rls < ratio * rrs
neg : ls + rll.size + 1 + (rlr.size + rrs + 1) = ls + (rll.size + rlr.size + 1 + rrs + 1)
⊢ (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
simp [node4L, node', sr.1, sr.2.1.1]

Premises used: Ordnode.node', And.right, And.left, Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h_1 : ¬rls < ratio * rrs
⊢ ls + rll.size + 1 + (rlr.size + rrs + 1) = ls + (rll.size + rlr.size + 1 + rrs + 1)

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ delta * Nat.succ 0 < ls

Tactic:
have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
this : delta * Nat.succ 0 < ls
rwa : ∀ (this : delta * Nat.succ 0 < ll.size + lr.size + 1), delta ≤ ll.size + lr.size
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : delta * Nat.succ 0 ≤ ll.size + lr.size), delta ≤ ll.size + lr.size
⊢ delta ≤ ll.size + lr.size

Tactic:
rwa [sl.1, Nat.lt_succ_iff] at this

Premises used: Nat.lt_succ_iff, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ delta ≤ ll.size + lr.size

Tactic:
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