awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
lr : Ordnode α
h : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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 (rs + size_1 + 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)))
    (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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx
                (node lls lll llx llr).dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx (node lls lll llx llr).dual))
          lr.dual)
      (node lls lll llx llr).dual)
have pos : Eq.{u_1 + 1} (α := Ordnode α)
  (dual
    (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 (rs + size_1 + 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)))
  (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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x (dual nil)) lx
              (node lls lll llx llr).dual
          else
            node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
              (node (r.size + size + 1) r lx (node lls lll llx llr).dual))
        (dual nil))
    (node lls lll llx llr).dual)
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then
        node (ls + rs + 1) (node lls lll llx llr) lx (node (rs + lrs + 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))).dual =
    if lrs < ratio * lls then
      node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
        (node lls llr.dual llx lll.dual)
    else
      node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
have pos : ∀ (h : lrs < ratio * lls),
  (node (ls + rs + 1) (node lls lll llx llr) lx
        (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))).dual =
    node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
      (node lls llr.dual llx lll.dual)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
pos :
  ∀ (h : lrs < ratio * lls),
    (node (ls + rs + 1) (node lls lll llx llr) lx
          (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))).dual =
      node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
        (node lls llr.dual llx lll.dual)
⊢ (if lrs < ratio * lls then
        node (ls + rs + 1) (node lls lll llx llr) lx (node (rs + lrs + 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))).dual =
    if lrs < ratio * lls then
      node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
        (node lls llr.dual llx lll.dual)
    else
      node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
have neg : ∀ (h : ¬lrs < ratio * lls),
  (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))).dual =
    node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual
have rw : (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual
Tactic: rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual
have rw₁ : (l.balanceR x r).dual = (l.dual.dual.balanceR x r.dual.dual).dual
Tactic: rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual
rw₁ : (l.balanceR x r).dual = (l.dual.dual.balanceR x r.dual.dual).dual
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual
have rw₂ : (l.balanceR x r).dual = (l.balanceR x r.dual.dual).dual
Tactic: rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.balanceR x r).dual = (r.dual.balanceL x l.dual).dual.dual
rw₁ : (l.balanceR x r).dual = (l.dual.dual.balanceR x r.dual.dual).dual
rw₂ : (l.balanceR x r).dual = (l.balanceR x r.dual.dual).dual
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual
have rw₃ : (l.balanceR x r).dual = (l.balanceR x r).dual
Tactic: rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node4L x m y r).Sized
have nil : ∀ (hm : Sized.{u_1} (α := α) nil), (l.node4L x nil y r).Sized
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
nil : ∀ (hm : Sized.{u_1} (α := α) Ordnode.nil), (l.node4L x Ordnode.nil y r).Sized
⊢ (l.node4L x m y r).Sized
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (node size l_1 x_1 r_1).Sized),
  (l.node4L x (node size l_1 x_1 r_1) y r).Sized
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node4L x m y r).Sized
have nil : ∀ (hm : Sized.{u_1} (α := α) nil), (l.node4L x nil y r).Sized
Tactic: cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
nil : ∀ (hm : Sized.{u_1} (α := α) Ordnode.nil), (l.node4L x Ordnode.nil y r).Sized
⊢ (l.node4L x m y r).Sized
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (node size l_1 x_1 r_1).Sized),
  (l.node4L x (node size l_1 x_1 r_1) y r).Sized
Tactic: cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).size = l.size + m.size + r.size + 2
have dsimp : HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ) +
        1)
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    1 =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) m with
          | nil => 0
          | node sz l x r => sz :
          ℕ))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    2
Tactic: dsimp [node3L, node', size]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
            (match (motive := Ordnode α → ℕ) l with
              | nil => 0
              | node sz l x r => sz :
              ℕ)
            (match (motive := Ordnode α → ℕ) m with
              | nil => 0
              | node sz l x r => sz :
              ℕ) +
          1)
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      1 =
    HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      2
have rw : HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      1 +
    1 =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) m with
          | nil => 0
          | node sz l x r => sz :
          ℕ))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    2
Tactic: rw [add_right_comm _ 1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).size = l.size + m.size + r.size + 2
have dsimp : HAdd.hAdd (α := ℕ)
      (match (motive := Ordnode α → ℕ) l with
        | nil => 0
        | node sz l x r => sz :
        ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) r with
            | nil => 0
            | node sz l x r => sz :
            ℕ) +
        1) +
    1 =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) m with
          | nil => 0
          | node sz l x r => sz :
          ℕ))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    2
Tactic: dsimp [node3R, node', size]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ HAdd.hAdd (α := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
            (match (motive := Ordnode α → ℕ) m with
              | nil => 0
              | node sz l x r => sz :
              ℕ)
            (match (motive := Ordnode α → ℕ) r with
              | nil => 0
              | node sz l x r => sz :
              ℕ) +
          1) +
      1 =
    HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      2
have rw : HAdd.hAdd (α := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) r with
            | nil => 0
            | node sz l x r => sz :
            ℕ)) +
      1 +
    1 =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) m with
          | nil => 0
          | node sz l x r => sz :
          ℕ))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    2
Tactic: rw [← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
rw :
  HAdd.hAdd (α := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (HAdd.hAdd (α := ℕ) (β := ℕ)
            (match (motive := Ordnode α → ℕ) m with
              | nil => 0
              | node sz l x r => sz :
              ℕ)
            (match (motive := Ordnode α → ℕ) r with
              | nil => 0
              | node sz l x r => sz :
              ℕ)) +
        1 +
      1 =
    HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      2
⊢ HAdd.hAdd (α := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
            (match (motive := Ordnode α → ℕ) m with
              | nil => 0
              | node sz l x r => sz :
              ℕ)
            (match (motive := Ordnode α → ℕ) r with
              | nil => 0
              | node sz l x r => sz :
              ℕ) +
          1) +
      1 =
    HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      2
have rw₁ : HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) m with
            | nil => 0
            | node sz l x r => sz :
            ℕ))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      1 +
    1 =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) m with
          | nil => 0
          | node sz l x r => sz :
          ℕ))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    2
Tactic: rw [← add_assoc, ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2
have nil : ∀ (hm : Sized.{u_1} (α := α) nil), (l.node4L x nil y r).size = l.size + size.{u_1} (α := α) nil + r.size + 2
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
nil :
  ∀ (hm : Sized.{u_1} (α := α) Ordnode.nil),
    (l.node4L x Ordnode.nil y r).size = l.size + size.{u_1} (α := α) Ordnode.nil + r.size + 2
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (node size l_1 x_1 r_1).Sized),
  (l.node4L x (node size l_1 x_1 r_1) y r).size = l.size + (node size l_1 x_1 r_1).size + r.size + 2
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : Sized.{u_1} (α := α) nil
⊢ (l.node4L x nil y r).size = l.size + size.{u_1} (α := α) nil + r.size + 2
have nil : l.size + 1 + r.size = l.size + r.size + 1
Tactic: simp [node4L, node3L, node']
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
hm : (node size l_1 x_1 r_1).Sized
⊢ (l.node4L x (node size l_1 x_1 r_1) y r).size = l.size + (node size l_1 x_1 r_1).size + r.size + 2
have node : HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) l_1 with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      1 +
    (HAdd.hAdd (α := ℕ) (β := ℕ)
        (match (motive := Ordnode α → ℕ) r_1 with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | node sz l x r => sz :
          ℕ) +
      1) =
  HAdd.hAdd (β := ℕ)
      (HAdd.hAdd (α := ℕ)
        (match (motive := Ordnode α → ℕ) l with
          | nil => 0
          | node sz l x r => sz :
          ℕ)
        (HAdd.hAdd (α := ℕ) (β := ℕ)
            (match (motive := Ordnode α → ℕ) l_1 with
              | nil => 0
              | node sz l x r => sz :
              ℕ)
            (match (motive := Ordnode α → ℕ) r_1 with
              | nil => 0
              | node sz l x r => sz :
              ℕ) +
          1))
      (match (motive := Ordnode α → ℕ) r with
        | nil => 0
        | node sz l x r => sz :
        ℕ) +
    1
Tactic: simp [node4L, node', size, hm.1]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.Sized
have rw : t.dual.dual.Sized
Tactic: rw [← dual_dual t]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateL x r).Sized
have nil : ∀ (hr : Sized.{u_1} (α := α) nil), (l.rotateL x nil).Sized
Tactic: cases r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
nil : ∀ (hr : Sized.{u_1} (α := α) Ordnode.nil), (l.rotateL x Ordnode.nil).Sized
⊢ (l.rotateL x r).Sized
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α) (hr : (node size l_1 x_1 r).Sized),
  (l.rotateL x (node size l_1 x_1 r)).Sized
Tactic: cases r
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
hr : (node size l_1 x_1 r).Sized
⊢ (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).Sized
have pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
hr : (node size l_1 x_1 r).Sized
pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).Sized
⊢ (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).Sized
have neg : ¬l_1.size < ratio * r.size → (l.node4L x l_1 x_1 r).Sized
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.rotateR x r).dual.Sized
have rw : (r.dual.rotateL x l.dual).Sized
Tactic: rw [dual_rotateR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : r.Sized
⊢ (l.rotateL x r).size = l.size + r.size + 1
have nil : ∀ (hm : Sized.{u_1} (α := α) nil), (l.rotateL x nil).size = l.size + size.{u_1} (α := α) nil + 1
Tactic: cases r
Cleared hypotheses: r, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : r.Sized
nil :
  ∀ (hm : Sized.{u_1} (α := α) Ordnode.nil),
    (l.rotateL x Ordnode.nil).size = l.size + size.{u_1} (α := α) Ordnode.nil + 1
⊢ (l.rotateL x r).size = l.size + r.size + 1
have node : ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α) (hm : (node size l_1 x_1 r).Sized),
  (l.rotateL x (node size l_1 x_1 r)).size = l.size + (node size l_1 x_1 r).size + 1
Tactic: cases r
Cleared hypotheses: r, hm
-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
hm : (node size l_1 x_1 r).Sized
⊢ (l.rotateL x (node size l_1 x_1 r)).size = l.size + (node size l_1 x_1 r).size + 1
have node : (if l_1.size < ratio * r.size then l.node3L x l_1 x_1 r else l.node4L x l_1 x_1 r).size = l.size + size + 1
Tactic: simp [Ordnode.rotateL]