awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
lrx : α
lrr : Ordnode α
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
have node : ∀ (hl : (node' nil lx (node lrs nil lrx nil)).Balanced) (sl : (node ls nil lx (node lrs nil lrx nil)).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
  node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs nil lrx nil)).node' x nil
    else (node' nil lx (node lrs nil lrx nil)).rotateR x nil
Tactic: cases sl.2.2.2.2.size_eq_zero.1 this.2
Cleared hypotheses: lrr, hl, sl, 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 : ℕ
lrx : α
hl : (node' nil lx (node lrs nil lrx nil)).Balanced
sl : (node ls nil lx (node lrs nil lrx nil)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (node lrs nil lrx nil)).node' x nil
    else (node' nil lx (node lrs nil lrx nil)).rotateR x nil
have node : ∀ (hl : (node' nil lx (node 1 nil lrx nil)).Balanced) (sl : (node ls nil lx (node 1 nil lrx nil)).Sized),
  node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1 then (node' nil lx (node 1 nil lrx nil)).node' x nil
    else (node' nil lx (node 1 nil lrx nil)).rotateR x nil
Tactic: obtain rfl : lrs = 1 := sl.2.2.1
Cleared hypotheses: lrs, 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
lrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : (node' nil lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1 then (node' nil lx (node 1 nil lrx nil)).node' x nil
    else (node' nil lx (node 1 nil lrx nil)).rotateR x nil
have node : node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (node 1 nil lrx nil) x nil
Tactic: rw [if_neg, rotateR_node, if_neg]
-- 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
lrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : (node' nil lx (Ordnode.node 1 nil lrx nil)).Balanced
sl : (Ordnode.node ls nil lx (Ordnode.node 1 nil lrx nil)).Sized
node :
  Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (Ordnode.node 1 nil lrx nil) x nil
⊢ Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1 then (node' nil lx (Ordnode.node 1 nil lrx nil)).node' x nil
    else (node' nil lx (Ordnode.node 1 nil lrx nil)).rotateR x nil
have node₁ : ¬(Ordnode.node 1 nil lrx nil).size < ratio * size.{u_1} (α := α) nil
Tactic: rw [if_neg, rotateR_node, if_neg]
-- 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
lrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : (node' nil lx (Ordnode.node 1 nil lrx nil)).Balanced
sl : (Ordnode.node ls nil lx (Ordnode.node 1 nil lrx nil)).Sized
node :
  Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (Ordnode.node 1 nil lrx nil) x nil
node₁ : ¬(Ordnode.node 1 nil lrx nil).size < ratio * size.{u_1} (α := α) nil
⊢ Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1 then (node' nil lx (Ordnode.node 1 nil lrx nil)).node' x nil
    else (node' nil lx (Ordnode.node 1 nil lrx nil)).rotateR x nil
have node₂ : ¬HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1
Tactic: rw [if_neg, rotateR_node, if_neg]
-- 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
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
⊢ lll.size = 0 ∧ llr.size = 0
have this : (node lls lll llx llr).size ≤ 1
Tactic: have := balancedSz_zero.1 hl.1
-- 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
this : (node lls lll llx llr).size ≤ 1
⊢ lll.size = 0 ∧ llr.size = 0
have rwa : ∀ (this : lls ≤ 1), lll.size = 0 ∧ llr.size = 0
Tactic: rwa [size, sl.2.1.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
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
this : (node lls lll llx llr).size ≤ 1
rwa : ∀ (this : lls ≤ 1), lll.size = 0 ∧ llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0
have rwa₁ : ∀ (this : lll.size + llr.size + 1 ≤ 1), lll.size = 0 ∧ llr.size = 0
Tactic: rwa [size, sl.2.1.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
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
this : (node lls lll llx llr).size ≤ 1
rwa : ∀ (this : lls ≤ 1), lll.size = 0 ∧ llr.size = 0
rwa₁ : ∀ (this : lll.size + llr.size + 1 ≤ 1), lll.size = 0 ∧ llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0
have rwa₂ : ∀ (this : lll.size + llr.size ≤ 0), lll.size = 0 ∧ llr.size = 0
Tactic: rwa [size, sl.2.1.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
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
this : (node lls lll llx llr).size ≤ 1
rwa : ∀ (this : lls ≤ 1), lll.size = 0 ∧ llr.size = 0
rwa₁ : ∀ (this : lll.size + llr.size + 1 ≤ 1), lll.size = 0 ∧ llr.size = 0
rwa₂ : ∀ (this : lll.size + llr.size ≤ 0), lll.size = 0 ∧ llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0
have rwa₃ : ∀ (this : lll.size + llr.size = 0), lll.size = 0 ∧ llr.size = 0
Tactic: rwa [size, sl.2.1.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
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
this : (node lls lll llx llr).size ≤ 1
rwa : ∀ (this : lls ≤ 1), lll.size = 0 ∧ llr.size = 0
rwa₁ : ∀ (this : lll.size + llr.size + 1 ≤ 1), lll.size = 0 ∧ llr.size = 0
rwa₂ : ∀ (this : lll.size + llr.size ≤ 0), lll.size = 0 ∧ llr.size = 0
rwa₃ : ∀ (this : lll.size + llr.size = 0), lll.size = 0 ∧ llr.size = 0
⊢ lll.size = 0 ∧ llr.size = 0
have rwa₄ : ∀ (this : lll.size = 0 ∧ llr.size = 0), lll.size = 0 ∧ llr.size = 0
Tactic: rwa [size, sl.2.1.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
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 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
have this : lll.size = 0 ∧ llr.size = 0
Tactic: have : size lll = 0 ∧ size llr = 0 := by
          have := balancedSz_zero.1 hl.1
          rwa [size, sl.2.1.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
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
this : lll.size = 0 ∧ llr.size = 0
⊢ 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
have node : ∀ (hl : ((node lls nil llx llr).node' lx nil).Balanced) (sl : (node ls (node lls nil llx llr) lx nil).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ llr.size = 0),
  node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx llr).node' lx nil).node' x nil
    else ((node lls nil llx llr).node' lx nil).rotateR x nil
Tactic: cases sl.2.1.2.1.size_eq_zero.1 this.1
Cleared hypotheses: lll, hl, sl, 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
lls : ℕ
llx : α
llr : Ordnode α
hl : ((node lls nil llx llr).node' lx nil).Balanced
sl : (node ls (node lls nil llx llr) lx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ llr.size = 0
⊢ node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx llr).node' lx nil).node' x nil
    else ((node lls nil llx llr).node' lx nil).rotateR x nil
have node : ∀ (hl : ((node lls nil llx nil).node' lx nil).Balanced) (sl : (node ls (node lls nil llx nil) lx nil).Sized)
  (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
  node 3 (node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx nil).node' lx nil).node' x nil
    else ((node lls nil llx nil).node' lx nil).rotateR x nil
Tactic: cases sl.2.1.2.2.size_eq_zero.1 this.2
Cleared hypotheses: llr, hl, sl, 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
lls : ℕ
llx : α
hl : ((node lls nil llx nil).node' lx nil).Balanced
sl : (node ls (node lls nil llx nil) lx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ node 3 (node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx nil).node' lx nil).node' x nil
    else ((node lls nil llx nil).node' lx nil).rotateR x nil
have node : ∀ (hl : ((node 1 nil llx nil).node' lx nil).Balanced) (sl : (node ls (node 1 nil llx nil) lx nil).Sized),
  node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then ((node 1 nil llx nil).node' lx nil).node' x nil
    else ((node 1 nil llx nil).node' lx nil).rotateR x nil
Tactic: obtain rfl : lls = 1 := sl.2.1.1
Cleared hypotheses: lls, 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
llx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then ((node 1 nil llx nil).node' lx nil).node' x nil
    else ((node 1 nil llx nil).node' lx nil).rotateR x nil
have node : node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = (node 1 nil llx nil).node3R lx nil x nil
Tactic: rw [if_neg, rotateR_node, if_pos]
-- 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
llx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : ((Ordnode.node 1 nil llx nil).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node 1 nil llx nil) lx nil).Sized
node :
  Ordnode.node 3 (Ordnode.node 1 nil llx nil) lx (Ordnode.singleton x) =
    (Ordnode.node 1 nil llx nil).node3R lx nil x nil
⊢ Ordnode.node 3 (Ordnode.node 1 nil llx nil) lx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then ((Ordnode.node 1 nil llx nil).node' lx nil).node' x nil
    else ((Ordnode.node 1 nil llx nil).node' lx nil).rotateR x nil
have node₁ : size.{u_1} (α := α) nil < ratio * (Ordnode.node 1 nil llx nil).size
Tactic: rw [if_neg, rotateR_node, if_pos]
-- 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
llx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : ((Ordnode.node 1 nil llx nil).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node 1 nil llx nil) lx nil).Sized
node :
  Ordnode.node 3 (Ordnode.node 1 nil llx nil) lx (Ordnode.singleton x) =
    (Ordnode.node 1 nil llx nil).node3R lx nil x nil
node₁ : size.{u_1} (α := α) nil < ratio * (Ordnode.node 1 nil llx nil).size
⊢ Ordnode.node 3 (Ordnode.node 1 nil llx nil) lx (Ordnode.singleton x) =
    if HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then ((Ordnode.node 1 nil llx nil).node' lx nil).node' x nil
    else ((Ordnode.node 1 nil llx nil).node' lx nil).rotateR x nil
have node₂ : ¬HAdd.hAdd (α := ℕ) 1 1 ≤ 1
Tactic: rw [if_neg, rotateR_node, if_pos]
-- 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
⊢ (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
have node : (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) =
  if lrs < ratio * lls then
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
  else
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
Tactic: 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
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
⊢ (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) =
    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)
have node : (if (node lrs lrl lrx lrr).size < ratio * (node lls lll llx llr).size then
    (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
  else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
  if lrs < ratio * lls then
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
  else
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
Tactic: rw [if_neg, rotateR]
-- 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 : ((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
node :
  (if (Ordnode.node lrs lrl lrx lrr).size < ratio * (Ordnode.node lls lll llx llr).size then
      (Ordnode.node lls lll llx llr).node3R lx (Ordnode.node lrs lrl lrx lrr) x nil
    else (Ordnode.node lls lll llx llr).node4R lx (Ordnode.node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)
⊢ (if lls + lrs + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)
have node₁ : ¬lls + lrs + 1 ≤ 1
Tactic: rw [if_neg, rotateR]
-- 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
⊢ (if (node lrs lrl lrx lrr).size < ratio * (node lls lll llx llr).size then
      (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)
have node : (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
  else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
  if lrs < ratio * lls then
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
  else
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
Tactic: dsimp only [size_node]
-- 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
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)
have pos : lrs < ratio * lls →
  (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
Tactic: split_ifs
-- 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
pos :
  lrs < ratio * lls →
    (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)
have neg : ¬lrs < ratio * lls →
  (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
Tactic: split_ifs
-- 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
h : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
have pos : lls + (lrs + 1) = lls + lrs + 1
Tactic: simp [node3R, node']
-- 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
h : ¬lrs < ratio * lls
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x nil =
    node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
      (node (lrr.size + 1) lrr x nil)
have neg : lls + lrl.size + 1 + (lrr.size + 1) = lls + (lrl.size + lrr.size + 1) + 1
Tactic: simp [node4R, node', sl.2.2.1]