awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (node ls ll lx lr).balance x (node rs rl rx rr) = (node ls ll lx lr).balance' x (node rs rl rx rr)
have 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 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
  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 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
    else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
  if ls + rs ≤ 1 then (node ls ll lx lr).node' x (node rs rl rx rr)
  else
    if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
    else
      if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
      else (node ls ll lx lr).node' x (node rs rl rx rr)
Tactic: simp only [balance, id_eq, balance', size_node, gt_iff_lt]
-- 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
⊢ (if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
    else
      if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
      else (node ls ll lx lr).node' x (node rs rl rx rr)) =
    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 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
    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 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
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)
have pos : ∀ (h : delta * ls < rs),
  (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: split_ifs with h h_1
-- 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
⊢ delta ≤ rl.size + rr.size
have this : delta * Nat.succ 0 < rs
Tactic: have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sl.pos) h
-- 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
this : delta * Nat.succ 0 < rs
⊢ delta ≤ rl.size + rr.size
have rwa : ∀ (this : delta * Nat.succ 0 < rl.size + rr.size + 1), delta ≤ rl.size + rr.size
Tactic: rwa [sr.1, Nat.lt_succ_iff] at this
Cleared hypotheses: 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
this : delta * Nat.succ 0 < rs
rwa : ∀ (this : delta * Nat.succ 0 < rl.size + rr.size + 1), delta ≤ rl.size + rr.size
⊢ delta ≤ rl.size + rr.size
have rwa₁ : ∀ (this : delta * Nat.succ 0 ≤ rl.size + rr.size), delta ≤ rl.size + rr.size
Tactic: rwa [sr.1, Nat.lt_succ_iff] at this
Cleared hypotheses: this
-- 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
⊢ (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
have rd : 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
-- 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
rd : delta ≤ rl.size + rr.size
⊢ (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
have 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
Tactic: obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
Cleared hypotheses: rl, hr, sr, rd
-- 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
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
⊢ (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
have 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)
Tactic: obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
Cleared hypotheses: rl, hr, sr, rd
-- 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 : ℕ
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
⊢ (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
have rd₁ : delta ≤ rr.size
Tactic: rw [size, zero_add] at rd
Cleared hypotheses: rd
-- 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 : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
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)
have pos : ∀ (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: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr, rd
-- 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 : ℕ
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
⊢ (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)
have 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))
Tactic: dsimp [rotateL]
-- 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 : ℕ
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
⊢ (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))
have 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)
Tactic: split_ifs
-- 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 : ℕ
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)
⊢ (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))
have 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))
Tactic: split_ifs
-- 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 : ℕ
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
⊢ (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)
have pos : ls + rls + 1 + rrs = ls + (rls + rrs + 1)
Tactic: simp [node3L, node', sr.1]
-- 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 : ℕ
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
⊢ (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))
have neg : ls + rll.size + 1 + (rlr.size + rrs + 1) = ls + (rll.size + rlr.size + 1 + rrs + 1)
Tactic: simp [node4L, node', sr.1, sr.2.1.1]
-- 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
⊢ delta ≤ ll.size + lr.size
have this : delta * Nat.succ 0 < ls
Tactic: have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
-- 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
this : delta * Nat.succ 0 < ls
⊢ delta ≤ ll.size + lr.size
have rwa : ∀ (this : delta * Nat.succ 0 < ll.size + lr.size + 1), delta ≤ ll.size + lr.size
Tactic: rwa [sl.1, Nat.lt_succ_iff] at this
Cleared hypotheses: 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
this : delta * Nat.succ 0 < ls
rwa : ∀ (this : delta * Nat.succ 0 < ll.size + lr.size + 1), delta ≤ ll.size + lr.size
⊢ delta ≤ ll.size + lr.size
have rwa₁ : ∀ (this : delta * Nat.succ 0 ≤ ll.size + lr.size), delta ≤ ll.size + lr.size
Tactic: rwa [sl.1, Nat.lt_succ_iff] at this
Cleared hypotheses: this