awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
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).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
have ld : 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
-- 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
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
⊢ (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
have 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
Tactic: obtain - | ⟨lls, lll, llx, llr⟩ := ll
Cleared hypotheses: ll, hl, sl, ld
-- 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
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
⊢ (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
have 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)
Tactic: obtain - | ⟨lls, lll, llx, llr⟩ := ll
Cleared hypotheses: ll, hl, sl, ld
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
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
⊢ (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
have ld₁ : delta ≤ lr.size
Tactic: rw [size, zero_add] at ld
Cleared hypotheses: ld
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
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)
have pos : ∀ (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: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr, hl, sl, ld
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ (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)
have 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))
Tactic: dsimp [rotateR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ (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))
have 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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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))
⊢ (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))
have 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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ (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))
have pos : lls + (lrs + rs + 1) = lls + lrs + 1 + rs
Tactic: simp [node3R, node', sl.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ (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))
have neg : lls + lrl.size + 1 + (lrr.size + rs + 1) = lls + (lrl.size + lrr.size + 1) + 1 + rs
Tactic: simp [node4R, node', sl.1, sl.2.2.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ l.balanceL x r = l.balance x r
have nil : ∀ (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: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, sr, H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ l.balanceL x r = l.balance x r
have node : ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (sr : (node rs rl rx rr).Sized)
  (H1 : l.size = 0 → (node rs rl rx rr).size ≤ 1)
  (H2 : 1 ≤ l.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * l.size),
  l.balanceL x (node rs rl rx rr) = l.balance x (node rs rl rx rr)
Tactic: obtain - | ⟨rs, rl, rx, rr⟩ := r
Cleared hypotheses: r, sr, H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
sl : l.Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
H1 : l.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ l.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * l.size
⊢ l.balanceL x (node rs rl rx rr) = l.balance x (node rs rl rx rr)
have node : ∀ (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),
  balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, sl, H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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)
⊢ l.balanceL x (Ordnode.node rs rl rx rr) = l.balance x (Ordnode.node rs rl rx rr)
have 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)
Tactic: obtain - | ⟨ls, ll, lx, lr⟩ := l
Cleared hypotheses: l, sl, H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
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
have this : (node rs rl rx rr).size ≤ 1
Tactic: have := H1 rfl
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ rl.size = 0 ∧ rr.size = 0
have rwa : ∀ (this : rs ≤ 1), rl.size = 0 ∧ rr.size = 0
Tactic: rwa [size, sr.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 : α
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
⊢ rl.size = 0 ∧ rr.size = 0
have rwa₁ : ∀ (this : rl.size + rr.size + 1 ≤ 1), rl.size = 0 ∧ rr.size = 0
Tactic: rwa [size, sr.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 : α
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
⊢ rl.size = 0 ∧ rr.size = 0
have rwa₂ : ∀ (this : rl.size + 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ rl.size = 0 ∧ rr.size = 0
have rwa₃ : ∀ (this : rl.size + 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
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
⊢ rl.size = 0 ∧ rr.size = 0
have rwa₄ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (hypothesis)
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
⊢ balanceL nil x (node rs rl rx rr) = balance nil x (node rs rl rx rr)
have this : 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