awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else rotateL nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
have nil : (if 0 + (rls + rrs + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
  else rotateL nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))) =
  if rls < ratio * rrs then
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
  else
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if 0 + (rls + rrs + 1) ≤ 1 then node' nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else rotateL nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have nil : (if (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
    node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
  else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
  if rls < ratio * rrs then
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
  else
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Tactic: rw [zero_add, if_neg, rotateL]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
nil :
  (if (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      node3L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) Ordnode.nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
⊢ (if 0 + (rls + rrs + 1) ≤ 1 then node' Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else rotateL Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) Ordnode.nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have nil₁ : ¬rls + rrs + 1 ≤ 1
Tactic: rw [zero_add, if_neg, rotateL]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have nil : (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
  else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
  if rls < ratio * rrs then
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
  else
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Tactic: dsimp only [size_node]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
⊢ (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have pos : rls < ratio * rrs →
  node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
pos :
  rls < ratio * rrs →
    node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
⊢ (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have neg : ¬rls < ratio * rrs →
  node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h : rls < ratio * rrs
⊢ node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
have pos : rls + 1 + rrs = rls + rrs + 1
Tactic: simp [node3L, node']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h : ¬rls < ratio * rrs
⊢ node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
have neg : rll.size + 1 + (rlr.size + rrs + 1) = rll.size + rlr.size + 1 + rrs + 1
Tactic: simp [node4L, node', sr.2.1.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
⊢ (node ls ll lx lr).balance x r = (node ls ll lx lr).balance' x r
have node : ∀ (hr : Balanced.{u_1} (α := α) nil) (sr : Sized.{u_1} (α := α) nil),
  (node ls ll lx lr).balance x nil = (node ls ll lx lr).balance' x nil
Tactic: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (Ordnode.node ls ll lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
node :
  ∀ (hr : Balanced.{u_1} (α := α) nil) (sr : Sized.{u_1} (α := α) nil),
    (Ordnode.node ls ll lx lr).balance x nil = (Ordnode.node ls ll lx lr).balance' x nil
⊢ (Ordnode.node ls ll lx lr).balance x r = (Ordnode.node ls ll lx lr).balance' x r
have node₁ : ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (hr : (Ordnode.node rs rl rx rr).Balanced)
  (sr : (Ordnode.node rs rl rx rr).Sized),
  (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: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
⊢ (node ls ll lx lr).balance x nil = (node ls ll lx lr).balance' x nil
have node : ∀ (hl : (ll.node' lx lr).Balanced) (sl : (node ls ll lx lr).Sized) (hr : Balanced.{u_1} (α := α) nil)
  (sr : Sized.{u_1} (α := α) nil), (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil
Tactic: rw [sl.eq_node'] at hl ⊢
Cleared hypotheses: hl, sl, hr, sr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (ll.node' lx lr).Balanced
sl : (node ls ll lx lr).Sized
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
⊢ (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil
have node : ∀ (hl : (node' nil lx lr).Balanced) (sl : (node ls nil lx lr).Sized),
  (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil
Tactic: obtain - | ⟨lls, lll, llx, llr⟩ := ll
Cleared hypotheses: ll, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (ll.node' lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
node :
  ∀ (hl : (node' nil lx lr).Balanced) (sl : (Ordnode.node ls nil lx lr).Sized),
    (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil
⊢ (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil
have node₁ : ∀ (lls : ℕ) (lll : Ordnode α) (llx : α) (llr : Ordnode α) (hl : ((Ordnode.node lls lll llx llr).node' lx lr).Balanced)
  (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx lr).Sized),
  ((Ordnode.node lls lll llx llr).node' lx lr).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx lr).balance' x nil
Tactic: obtain - | ⟨lls, lll, llx, llr⟩ := ll
Cleared hypotheses: ll, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
hl : (node' nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
⊢ (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil
have node : ∀ (hl : (node' nil lx nil).Balanced) (sl : (node ls nil lx nil).Sized),
  (node' nil lx nil).balance x nil = (node' nil lx nil).balance' x nil
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
hl : (node' nil lx lr).Balanced
sl : (Ordnode.node ls nil lx lr).Sized
node :
  ∀ (hl : (node' nil lx nil).Balanced) (sl : (Ordnode.node ls nil lx nil).Sized),
    (node' nil lx nil).balance x nil = (node' nil lx nil).balance' x nil
⊢ (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil
have node₁ : ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) (hl : (node' nil lx (Ordnode.node lrs lrl lrx lrr)).Balanced)
  (sl : (Ordnode.node ls nil lx (Ordnode.node lrs lrl lrx lrr)).Sized),
  (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
    (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
⊢ ((node lls lll llx llr).node' lx lr).balance x nil = ((node lls lll llx llr).node' lx lr).balance' x nil
have node : ∀ (hl : ((node lls lll llx llr).node' lx nil).Balanced) (sl : (node ls (node lls lll llx llr) lx nil).Sized),
  ((node lls lll llx llr).node' lx nil).balance x nil = ((node lls lll llx llr).node' lx nil).balance' x nil
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx lr).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx lr).Sized
node :
  ∀ (hl : ((Ordnode.node lls lll llx llr).node' lx nil).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx nil).Sized),
    ((Ordnode.node lls lll llx llr).node' lx nil).balance x nil =
      ((Ordnode.node lls lll llx llr).node' lx nil).balance' x nil
⊢ ((Ordnode.node lls lll llx llr).node' lx lr).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx lr).balance' x nil
have node₁ : ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α)
  (hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced)
  (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized),
  ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr, hl, sl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ (node' nil lx (node lrs lrl lrx lrr)).balance x nil = (node' nil lx (node lrs lrl lrx lrr)).balance' x nil
have node : node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
  if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs lrl lrx lrr)).node' x nil
  else (node' nil lx (node lrs lrl lrx lrr)).rotateR x nil
Tactic: dsimp [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ ((node lls lll llx llr).node' lx nil).balance x nil = ((node lls lll llx llr).node' lx nil).balance' x nil
have node : node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
  if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
  else ((node lls lll llx llr).node' lx nil).rotateR x nil
Tactic: dsimp [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).balance x nil =
    ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).balance' x nil
have node : (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)) =
  if lls + lrs + 1 ≤ 1 then ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).node' x nil
  else ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).rotateR x nil
Tactic: dsimp [balance, balance']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ lrl.size = 0 ∧ lrr.size = 0
have this : (node lrs lrl lrx lrr).size ≤ 1
Tactic: have := balancedSz_zero.1 hl.1.symm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0
have rwa : ∀ (this : lrs ≤ 1), lrl.size = 0 ∧ lrr.size = 0
Tactic: rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
rwa : ∀ (this : lrs ≤ 1), lrl.size = 0 ∧ lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0
have rwa₁ : ∀ (this : lrl.size + lrr.size + 1 ≤ 1), lrl.size = 0 ∧ lrr.size = 0
Tactic: rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
rwa : ∀ (this : lrs ≤ 1), lrl.size = 0 ∧ lrr.size = 0
rwa₁ : ∀ (this : lrl.size + lrr.size + 1 ≤ 1), lrl.size = 0 ∧ lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0
have rwa₂ : ∀ (this : lrl.size + lrr.size ≤ 0), lrl.size = 0 ∧ lrr.size = 0
Tactic: rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
rwa : ∀ (this : lrs ≤ 1), lrl.size = 0 ∧ lrr.size = 0
rwa₁ : ∀ (this : lrl.size + lrr.size + 1 ≤ 1), lrl.size = 0 ∧ lrr.size = 0
rwa₂ : ∀ (this : lrl.size + lrr.size ≤ 0), lrl.size = 0 ∧ lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0
have rwa₃ : ∀ (this : lrl.size + lrr.size = 0), lrl.size = 0 ∧ lrr.size = 0
Tactic: rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
rwa : ∀ (this : lrs ≤ 1), lrl.size = 0 ∧ lrr.size = 0
rwa₁ : ∀ (this : lrl.size + lrr.size + 1 ≤ 1), lrl.size = 0 ∧ lrr.size = 0
rwa₂ : ∀ (this : lrl.size + lrr.size ≤ 0), lrl.size = 0 ∧ lrr.size = 0
rwa₃ : ∀ (this : lrl.size + lrr.size = 0), lrl.size = 0 ∧ lrr.size = 0
⊢ lrl.size = 0 ∧ lrr.size = 0
have rwa₄ : ∀ (this : lrl.size = 0 ∧ lrr.size = 0), lrl.size = 0 ∧ lrr.size = 0
Tactic: rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs lrl lrx lrr)).node' x nil
    else (node' nil lx (node lrs lrl lrx lrr)).rotateR x nil
have this : lrl.size = 0 ∧ lrr.size = 0
Tactic: have : size lrl = 0 ∧ size lrr = 0 := by
          have := balancedSz_zero.1 hl.1.symm
          rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : lrl.size = 0 ∧ lrr.size = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs lrl lrx lrr)).node' x nil
    else (node' nil lx (node lrs lrl lrx lrr)).rotateR x nil
have node : ∀ (hl : (node' nil lx (node lrs nil lrx lrr)).Balanced) (sl : (node ls nil lx (node lrs nil lrx lrr)).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ lrr.size = 0),
  node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs nil lrx lrr)).node' x nil
    else (node' nil lx (node lrs nil lrx lrr)).rotateR x nil
Tactic: cases sl.2.2.2.1.size_eq_zero.1 this.1
Cleared hypotheses: lrl, hl, sl, this