awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ld : delta ≤ ll.size + lr.size
pos :
  ∀ (hl : (node ls nil lx lr).Balanced) (sl : (node ls nil lx lr).Sized)
    (ld : delta ≤ size.{u_1} (α := α) nil + lr.size),
    (node ls nil lx lr).rotateR 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              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 + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        nil
pos₁ :
  ∀ (lls : ℕ) (lll : Ordnode α) (llx : α) (llr : Ordnode α) (hl : (node ls (node lls lll llx llr) lx lr).Balanced)
    (sl : (node ls (node lls lll llx llr) lx lr).Sized) (ld : delta ≤ (node lls lll llx llr).size + lr.size),
    (node ls (node lls lll llx llr) lx lr).rotateR 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              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 + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        (node lls lll llx llr)
⊢ (node ls ll lx lr).rotateR 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 : 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

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
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
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ size.{u_1} (α := α) nil + lr.size
⊢ delta ≤ lr.size

Tactic:
rw [size, zero_add] at ld

Premises used: Ordnode.size, zero_add
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
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
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ lr.size
⊢ ¬delta ≤ 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
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
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ lr.size
⊢ (node ls nil lx lr).rotateR 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil

Tactic:
exact absurd (le_trans ld (balancedSz_zero.1 hl.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 : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
ld : delta ≤ (node lls lll llx llr).size + size.{u_1} (α := α) nil
⊢ ¬delta ≤ 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
ld : delta ≤ (node lls lll llx llr).size + size.{u_1} (α := α) nil
⊢ (node ls (node lls lll llx llr) lx nil).rotateR 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          nil)
      (node lls lll llx llr)

Tactic:
exact absurd (le_trans ld (balancedSz_zero.1 hl.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 : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
pos :
  (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else (node lls lll llx llr).node4R 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 + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))
⊢ (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).rotateR 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            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 + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          (node lrs lrl lrx lrr))
      (node lls lll llx llr)

Tactic:
dsimp [rotateR]

Premises used: Ordnode.rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
pos :
  lrs < ratio * lls →
    (node lls lll llx llr).node3R 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))
neg :
  ¬lrs < ratio * lls →
    (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
      node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else (node lls lll llx llr).node4R 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 + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h_2 : lrs < ratio * lls
pos : lls + (lrs + rs + 1) = lls + lrs + 1 + rs
⊢ (node lls lll llx llr).node3R 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))

Tactic:
simp [node3R, node', sl.1]

Premises used: Ordnode.node', Ordnode.node3R, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h_2 : lrs < ratio * lls
⊢ lls + (lrs + rs + 1) = lls + lrs + 1 + rs

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h_2 : ¬lrs < ratio * lls
neg : lls + lrl.size + 1 + (lrr.size + rs + 1) = lls + (lrl.size + lrr.size + 1) + 1 + rs
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))

Tactic:
simp [node4R, node', sl.1, 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 : α
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
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h_2 : ¬lrs < ratio * lls
⊢ lls + lrl.size + 1 + (lrr.size + rs + 1) = lls + (lrl.size + lrr.size + 1) + 1 + rs

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
⊢ (node ls ll lx lr).node' x (node rs rl rx rr) = node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Tactic:
simp [node']

Premises used: Ordnode.node'
-- 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
⊢ ¬ls + rs ≤ 1

Tactic:
not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

Premises used: Nat.succ_le_of_lt, add_le_add, Ordnode.Sized.pos, not_le_of_gt
-- 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
⊢ ¬ls + rs ≤ 1

Tactic:
exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

Premises used: not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
H1 : l.size = 0 → r.size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
nil :
  ∀ (sr : Sized.{u_1} (α := α) Ordnode.nil) (H1 : l.size = 0 → size.{u_1} (α := α) Ordnode.nil ≤ 1)
    (H2 : 1 ≤ l.size → 1 ≤ size.{u_1} (α := α) Ordnode.nil → size.{u_1} (α := α) Ordnode.nil ≤ delta * l.size),
    l.balanceL x Ordnode.nil = l.balance x Ordnode.nil
node :
  ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (sr : (Ordnode.node rs rl rx rr).Sized)
    (H1 : l.size = 0 → (Ordnode.node rs rl rx rr).size ≤ 1)
    (H2 : 1 ≤ l.size → 1 ≤ (Ordnode.node rs rl rx rr).size → (Ordnode.node rs rl rx rr).size ≤ delta * l.size),
    l.balanceL x (Ordnode.node rs rl rx rr) = l.balance x (Ordnode.node rs rl rx rr)
⊢ l.balanceL x r = l.balance x r

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
sr : Sized.{u_1} (α := α) nil
H1 : l.size = 0 → size.{u_1} (α := α) nil ≤ 1
H2 : 1 ≤ l.size → 1 ≤ size.{u_1} (α := α) nil → size.{u_1} (α := α) nil ≤ delta * l.size
⊢ l.balanceL x nil = l.balance x nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (Ordnode.node rs rl rx rr).Sized
H1 : l.size = 0 → (Ordnode.node rs rl rx rr).size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ (Ordnode.node rs rl rx rr).size → (Ordnode.node rs rl rx rr).size ≤ delta * l.size
node :
  ∀ (sl : Sized.{u_1} (α := α) nil) (H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs rl rx rr).size ≤ 1)
    (H2 :
      1 ≤ size.{u_1} (α := α) nil →
        1 ≤ (Ordnode.node rs rl rx rr).size → (Ordnode.node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil),
    balanceL nil x (Ordnode.node rs rl rx rr) = balance nil x (Ordnode.node rs rl rx rr)
node₁ :
  ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α) (sl : (Ordnode.node ls ll lx lr).Sized)
    (H1 : (Ordnode.node ls ll lx lr).size = 0 → (Ordnode.node rs rl rx rr).size ≤ 1)
    (H2 :
      1 ≤ (Ordnode.node ls ll lx lr).size →
        1 ≤ (Ordnode.node rs rl rx rr).size →
          (Ordnode.node rs rl rx rr).size ≤ delta * (Ordnode.node ls ll lx lr).size),
    (Ordnode.node ls ll lx lr).balanceL x (Ordnode.node rs rl rx rr) =
      (Ordnode.node ls ll lx lr).balance x (Ordnode.node rs rl rx rr)
⊢ l.balanceL x (Ordnode.node rs rl rx rr) = l.balance x (Ordnode.node rs rl rx rr)

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : Sized.{u_1} (α := α) nil
H1 : size.{u_1} (α := α) nil = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil
⊢ (node rs rl rx rr).size ≤ 1

Tactic:
have := H1 rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : Sized.{u_1} (α := α) nil
H1 : size.{u_1} (α := α) nil = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil
this : (node rs rl rx rr).size ≤ 1
rwa : ∀ (this : rs ≤ 1), rl.size = 0 ∧ rr.size = 0
rwa₁ : ∀ (this : rl.size + rr.size + 1 ≤ 1), rl.size = 0 ∧ rr.size = 0
rwa₂ : ∀ (this : rl.size + rr.size ≤ 0), rl.size = 0 ∧ rr.size = 0
rwa₃ : ∀ (this : rl.size + rr.size = 0), rl.size = 0 ∧ rr.size = 0
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : rl.size = 0 ∧ rr.size = 0), rl.size = 0 ∧ rr.size = 0
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Premises used: Nat.le_zero, Ordnode.size, And.left, Nat.succ_le_succ_iff, add_eq_zero
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : Sized.{u_1} (α := α) nil
H1 : size.{u_1} (α := α) nil = 0 → (node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
have : size rl = 0 ∧ size rr = 0 := by
        have := H1 rfl
        rwa [size, sr.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (Ordnode.node rs rl rx rr).Sized
sl : Sized.{u_1} (α := α) nil
H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs rl rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (Ordnode.node rs rl rx rr).size → (Ordnode.node rs rl rx rr).size ≤ delta * size.{u_1} (α := α) nil
this : rl.size = 0 ∧ rr.size = 0
node :
  ∀ (sr : (Ordnode.node rs nil rx rr).Sized) (H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs nil rx rr).size ≤ 1)
    (H2 :
      1 ≤ size.{u_1} (α := α) nil →
        1 ≤ (Ordnode.node rs nil rx rr).size → (Ordnode.node rs nil rx rr).size ≤ delta * size.{u_1} (α := α) nil)
    (this : size.{u_1} (α := α) nil = 0 ∧ rr.size = 0),
    balanceL nil x (Ordnode.node rs nil rx rr) = balance nil x (Ordnode.node rs nil rx rr)
⊢ balanceL nil x (Ordnode.node rs rl rx rr) = balance nil x (Ordnode.node rs rl rx rr)

Tactic:
cases sr.2.1.size_eq_zero.1 this.1

Premises used: Ordnode.Sized.size_eq_zero, And.right, And.left, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rx : α
rr : Ordnode α
sl : Sized.{u_1} (α := α) nil
sr : (Ordnode.node rs nil rx rr).Sized
H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs nil rx rr).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (Ordnode.node rs nil rx rr).size → (Ordnode.node rs nil rx rr).size ≤ delta * size.{u_1} (α := α) nil
this : size.{u_1} (α := α) nil = 0 ∧ rr.size = 0
node :
  ∀ (sr : (Ordnode.node rs nil rx nil).Sized) (H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs nil rx nil).size ≤ 1)
    (H2 :
      1 ≤ size.{u_1} (α := α) nil →
        1 ≤ (Ordnode.node rs nil rx nil).size → (Ordnode.node rs nil rx nil).size ≤ delta * size.{u_1} (α := α) nil)
    (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
    balanceL nil x (Ordnode.node rs nil rx nil) = balance nil x (Ordnode.node rs nil rx nil)
⊢ balanceL nil x (Ordnode.node rs nil rx rr) = balance nil x (Ordnode.node rs nil rx rr)

Tactic:
cases sr.2.2.size_eq_zero.1 this.2

Premises used: Ordnode.Sized.size_eq_zero, And.right, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized.{u_1} (α := α) nil
sr : (Ordnode.node rs nil rx nil).Sized
H1 : size.{u_1} (α := α) nil = 0 → (Ordnode.node rs nil rx nil).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (Ordnode.node rs nil rx nil).size → (Ordnode.node rs nil rx nil).size ≤ delta * size.{u_1} (α := α) nil
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
node : balanceL nil x (node' nil rx nil) = balance nil x (node' nil rx nil)
⊢ balanceL nil x (Ordnode.node rs nil rx nil) = balance nil x (Ordnode.node rs nil rx nil)

Tactic:
rw [sr.eq_node']

Premises used: Ordnode.Sized.eq_node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rx : α
sl : Sized.{u_1} (α := α) nil
sr : (node rs nil rx nil).Sized
H1 : size.{u_1} (α := α) nil = 0 → (node rs nil rx nil).size ≤ 1
H2 :
  1 ≤ size.{u_1} (α := α) nil →
    1 ≤ (node rs nil rx nil).size → (node rs nil rx nil).size ≤ delta * size.{u_1} (α := α) nil
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ balanceL nil x (node' nil rx nil) = balance nil x (node' nil rx nil)

Tactic:
rfl
-- 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 :
  1 ≤ (node ls ll lx lr).size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * (node ls ll lx lr).size
⊢ ¬rs > delta * ls

Tactic:
replace H2 : ¬rs > delta * ls := not_lt_of_ge (H2 sl.pos sr.pos)