awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
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) 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:
try rfl
-- Module: Mathlib.Data.Ordmap.Invariants
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)
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))
⊢ (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))

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h_1 : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
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:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h_1 : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
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:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₃ rw₄ : (l.balanceR x r).dual = (l.balanceR x r).dual
⊢ (l.balanceR x r).dual = r.dual.balanceL x l.dual

Tactic:
rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]

Premises used: Ordnode.dual_balanceL, Ordnode.balanceL, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node3L x m y r).Sized

Tactic:
(hl.node' hm).node' hr

Premises used: Ordnode.node3L, Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node3R x m y r).Sized

Tactic:
hl.node' (hm.node' hr)

Premises used: Ordnode.node3R, Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (Ordnode.node size l_1 x_1 r_1).Sized),
    (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).Sized
⊢ (l.node4L x m y r).Sized

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
hm : Sized.{u_1} (α := α) nil
⊢ (l.node4L x nil y r).Sized

Tactic:
(hl.node' hm).node' hr

Premises used: Ordnode.node3L, Ordnode.Sized.node', Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
hm : Sized.{u_1} (α := α) nil
⊢ (l.node4L x nil y r).Sized

Tactic:
exact (hl.node' hm).node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
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:
(hl.node' hm.2.1).node' (hm.2.2.node' hr)

Premises used: Ordnode.Sized.node', And.right, And.left, Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
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:
exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)

Premises used: Ordnode.Sized.node', And.right, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (Ordnode.node size l_1 x_1 r_1).Sized),
    (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).Sized
nil₁ : ∀ (hm : Sized.{u_1} (α := α) Ordnode.nil), (l.node4L x Ordnode.nil y r).Sized
node₁ :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (Ordnode.node size l_1 x_1 r_1).Sized),
    (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).Sized
⊢ (l.node4L x m y r).Sized

Tactic:
cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
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
⊢ (l.node3L x m y r).size = l.size + m.size + r.size + 2

Tactic:
dsimp [node3L, node', size]

Premises used: Ordnode.node', Ordnode.node3L, Ordnode.size
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
rw 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
⊢ 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:
rw [add_right_comm _ 1]

Premises used: add_right_comm, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
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
⊢ (l.node3R x m y r).size = l.size + m.size + r.size + 2

Tactic:
dsimp [node3R, node', size]

Premises used: Ordnode.node', Ordnode.node3R, Ordnode.size
-- Module: Mathlib.Data.Ordmap.Invariants
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
rw₁ 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
⊢ 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]

Premises used: add_assoc
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α) (hm : (Ordnode.node size l_1 x_1 r_1).Sized),
    (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).size = l.size + (Ordnode.node size l_1 x_1 r_1).size + r.size + 2
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : Sized.{u_1} (α := α) Ordnode.nil
nil : l.size + 1 + r.size = l.size + r.size + 1
⊢ (l.node4L x Ordnode.nil y r).size = l.size + size.{u_1} (α := α) Ordnode.nil + r.size + 2

Tactic:
simp [node4L, node3L, node']

Premises used: Ordnode.node', Ordnode.node3L, Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : Sized.{u_1} (α := α) nil
⊢ l.size + 1 + r.size = l.size + r.size + 1

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
hm : (Ordnode.node size l_1 x_1 r_1).Sized
node :
  HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | Ordnode.node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) l_1 with
            | nil => 0
            | Ordnode.node sz l x r => sz :
            ℕ) +
        1 +
      (HAdd.hAdd (α := ℕ) (β := ℕ)
          (match (motive := Ordnode α → ℕ) r_1 with
            | nil => 0
            | Ordnode.node sz l x r => sz :
            ℕ)
          (match (motive := Ordnode α → ℕ) r with
            | nil => 0
            | Ordnode.node sz l x r => sz :
            ℕ) +
        1) =
    HAdd.hAdd (β := ℕ)
        (HAdd.hAdd (α := ℕ)
          (match (motive := Ordnode α → ℕ) l with
            | nil => 0
            | Ordnode.node sz l x r => sz :
            ℕ)
          (HAdd.hAdd (α := ℕ) (β := ℕ)
              (match (motive := Ordnode α → ℕ) l_1 with
                | nil => 0
                | Ordnode.node sz l x r => sz :
                ℕ)
              (match (motive := Ordnode α → ℕ) r_1 with
                | nil => 0
                | Ordnode.node sz l x r => sz :
                ℕ) +
            1))
        (match (motive := Ordnode α → ℕ) r with
          | nil => 0
          | Ordnode.node sz l x r => sz :
          ℕ) +
      1
⊢ (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).size = l.size + (Ordnode.node size l_1 x_1 r_1).size + r.size + 2

Tactic:
simp [node4L, node', size, hm.1]

Premises used: Ordnode.node', Ordnode.size, And.left, Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
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
⊢ 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:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
sl : l.Sized
sr : r.Sized
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Premises used: Ordnode.size_dual, add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
rw : t.dual.dual.Sized
⊢ t.Sized

Tactic:
rw [← dual_dual t]

Premises used: Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Tactic:
h.dual

Premises used: Ordnode.Sized.dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
h : t.dual.Sized
⊢ t.dual.dual.Sized

Tactic:
exact h.dual

Premises used: Ordnode.Sized.dual
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α) (hr : (Ordnode.node size l_1 x_1 r).Sized),
    (l.rotateL x (Ordnode.node size l_1 x_1 r)).Sized
⊢ (l.rotateL x r).Sized

Tactic:
cases r
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : Sized.{u_1} (α := α) nil
⊢ (l.rotateL x nil).Sized

Tactic:
hl.node' hr

Premises used: Ordnode.Sized.node', Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
hr : Sized.{u_1} (α := α) nil
⊢ (l.rotateL x nil).Sized

Tactic:
exact hl.node' hr

Premises used: Ordnode.Sized.node'
-- Module: Mathlib.Data.Ordmap.Invariants
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
neg : ¬l_1.size < ratio * r.size → (l.node4L 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

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : l_1.size < ratio * r.size
⊢ (l.node3L x l_1 x_1 r).Sized

Tactic:
hl.node3L hr.2.1 hr.2.2

Premises used: And.right, And.left, Ordnode.Sized.node3L
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : l_1.size < ratio * r.size
⊢ (l.node3L x l_1 x_1 r).Sized

Tactic:
exact hl.node3L hr.2.1 hr.2.2

Premises used: And.right, And.left, Ordnode.Sized.node3L
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : ¬l_1.size < ratio * r.size
⊢ (l.node4L x l_1 x_1 r).Sized

Tactic:
hl.node4L hr.2.1 hr.2.2

Premises used: And.right, And.left, Ordnode.Sized.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
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
h : ¬l_1.size < ratio * r.size
⊢ (l.node4L x l_1 x_1 r).Sized

Tactic:
exact hl.node4L hr.2.1 hr.2.2

Premises used: And.right, And.left, Ordnode.Sized.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
rw : (r.dual.rotateL x l.dual).Sized
⊢ (l.rotateR x r).dual.Sized

Tactic:
rw [dual_rotateR]

Premises used: Ordnode.dual_rotateR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized

Tactic:
hr.dual.rotateL hl.dual

Premises used: Ordnode.Sized.dual, Ordnode.Sized.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (r.dual.rotateL x l.dual).Sized

Tactic:
exact hr.dual.rotateL hl.dual

Premises used: Ordnode.Sized.dual, Ordnode.Sized.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
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
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α) (hm : (Ordnode.node size l_1 x_1 r).Sized),
    (l.rotateL x (Ordnode.node size l_1 x_1 r)).size = l.size + (Ordnode.node size l_1 x_1 r).size + 1
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
cases r