awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
sz : ℕ
m : Ordnode α
y : α
r : Ordnode α
⊢ l.rotateL x (node sz m y r) = if m.size < ratio * r.size then l.node3L x m y r else l.node4L x m y r

Tactic:
rfl

Premises used: Ordnode.rotateL, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
⊢ l.rotateL x nil = l.node' x nil

Tactic:
rfl

Premises used: Ordnode.rotateL, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
sz : ℕ
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (node sz l x m).rotateR y r = if m.size < ratio * l.size then l.node3R x m y r else l.node4R x m y r

Tactic:
rfl

Premises used: Ordnode.rotateR, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
y : α
r : Ordnode α
⊢ rotateR nil y r = node' nil y r

Tactic:
rfl

Premises used: Ordnode.rotateR, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
simp [node', add_comm]

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

Tactic:
simp [node3L, node3R, add_comm]

Premises used: Ordnode.node3L, Ordnode.node3R, add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual

Tactic:
simp [node3L, node3R, add_comm]

Premises used: Ordnode.node3L, Ordnode.node3R, add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : (l.node4L x Ordnode.nil y r).dual = r.dual.node4R y (dual Ordnode.nil) x l.dual
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
    (l.node4L x (Ordnode.node size l_1 x_1 r_1) y r).dual =
      r.dual.node4R y (Ordnode.node size l_1 x_1 r_1).dual x l.dual
⊢ (l.node4L x m y r).dual = r.dual.node4R y m.dual x l.dual

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4L x nil y r).dual = r.dual.node4R y (dual nil) x l.dual

Tactic:
simp [node4L, node4R, node3R, dual_node3L, add_comm]

Premises used: Ordnode.node3R, Ordnode.dual_node3L, add_comm, Ordnode.node4L, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ (l.node4L x (node size l_1 x_1 r_1) y r).dual = r.dual.node4R y (node size l_1 x_1 r_1).dual x l.dual

Tactic:
simp [node4L, node4R, node3R, dual_node3L, add_comm]

Premises used: Ordnode.node3R, Ordnode.dual_node3L, add_comm, Ordnode.node4L, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
nil : (l.node4R x Ordnode.nil y r).dual = r.dual.node4L y (dual Ordnode.nil) x l.dual
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r_1 : Ordnode α),
    (l.node4R x (Ordnode.node size l_1 x_1 r_1) y r).dual =
      r.dual.node4L y (Ordnode.node size l_1 x_1 r_1).dual x l.dual
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual

Tactic:
cases m
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4R x nil y r).dual = r.dual.node4L y (dual nil) x l.dual

Tactic:
simp [node4L, node4R, node3L, dual_node3R, add_comm]

Premises used: Ordnode.node3L, add_comm, Ordnode.dual_node3R, Ordnode.node4L, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ (l.node4R x (node size l_1 x_1 r_1) y r).dual = r.dual.node4L y (node size l_1 x_1 r_1).dual x l.dual

Tactic:
simp [node4L, node4R, node3L, dual_node3R, add_comm]

Premises used: Ordnode.node3L, add_comm, Ordnode.dual_node3R, Ordnode.node4L, Ordnode.node4R
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
nil : (l.rotateL x Ordnode.nil).dual = rotateR (dual Ordnode.nil) x l.dual
node :
  ∀ (size : ℕ) (l_1 : Ordnode α) (x_1 : α) (r : Ordnode α),
    (l.rotateL x (Ordnode.node size l_1 x_1 r)).dual = (Ordnode.node size l_1 x_1 r).dual.rotateR x l.dual
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
cases r
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
⊢ (l.rotateL x nil).dual = rotateR (dual nil) x l.dual

Tactic:
simp [rotateL, rotateR]

Premises used: Ordnode.rotateR, Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
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).dual =
    if l_1.size < ratio * r.size then r.dual.node3R x_1 l_1.dual x l.dual else r.dual.node4R x_1 l_1.dual x l.dual
⊢ (l.rotateL x (Ordnode.node size l_1 x_1 r)).dual = (Ordnode.node size l_1 x_1 r).dual.rotateR x l.dual

Tactic:
simp [rotateL, rotateR]

Premises used: Ordnode.rotateR, Ordnode.rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
pos : l_1.size < ratio * r.size → (l.node3L x l_1 x_1 r).dual = r.dual.node3R x_1 l_1.dual x l.dual
neg : ¬l_1.size < ratio * r.size → (l.node4L x l_1 x_1 r).dual = r.dual.node4R x_1 l_1.dual x l.dual
⊢ (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).dual =
    if l_1.size < ratio * r.size then r.dual.node3R x_1 l_1.dual x l.dual else r.dual.node4R x_1 l_1.dual x l.dual

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
h : l_1.size < ratio * r.size
⊢ (l.node3L x l_1 x_1 r).dual = r.dual.node3R x_1 l_1.dual x l.dual

Tactic:
simp [dual_node3L, dual_node4L, node3R]

Premises used: Ordnode.node3R, Ordnode.dual_node4L, Ordnode.dual_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
size : ℕ
l_1 : Ordnode α
x_1 : α
r : Ordnode α
h : ¬l_1.size < ratio * r.size
⊢ (l.node4L x l_1 x_1 r).dual = r.dual.node4R x_1 l_1.dual x l.dual

Tactic:
simp [dual_node3L, dual_node4L, node3R]

Premises used: Ordnode.node3R, Ordnode.dual_node4L, Ordnode.dual_node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rw : (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
rw₁ : (l.rotateR x r).dual = (l.dual.dual.rotateR x r.dual.dual).dual
rw₂ : (l.rotateR x r).dual = (l.rotateR x r.dual.dual).dual
rw₃ rw₄ : (l.rotateR x r).dual = (l.rotateR x r).dual
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

Tactic:
rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]

Premises used: Ordnode.dual_rotateL, Ordnode.rotateL, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
simp :
  (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
⊢ (l.balance' x r).dual = r.dual.balance' x l.dual

Tactic:
simp [balance', add_comm]

Premises used: add_comm, Ordnode.balance'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
pos : ∀ (h : l.size + r.size ≤ 1), (l.node' x r).dual = r.dual.node' x l.dual
pos₁ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateL x l.dual
neg :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : delta * l.size < r.size) (h_2 : ¬delta * r.size < l.size),
    (l.rotateL x r).dual = r.dual.rotateR x l.dual
pos₂ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬delta * l.size < r.size),
    delta * r.size < l.size → (l.rotateR x r).dual = r.dual.rotateL x l.dual
neg₁ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬delta * l.size < r.size),
    ¬delta * r.size < l.size → (l.node' x r).dual = r.dual.node' x l.dual
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual

Tactic:
split_ifs with h h_1 h_2
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : l.size + r.size ≤ 1
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
simp [dual_rotateL, dual_rotateR, add_comm]

Premises used: Ordnode.dual_rotateR, add_comm, Ordnode.dual_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
pos : r.dual.rotateR x l.dual = r.dual.rotateL x l.dual
⊢ (l.rotateL x r).dual = r.dual.rotateL x l.dual

Tactic:
simp [dual_rotateL, dual_rotateR, add_comm]

Premises used: Ordnode.dual_rotateR, add_comm, Ordnode.dual_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : ¬delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
simp [dual_rotateL, dual_rotateR, add_comm]

Premises used: Ordnode.dual_rotateR, add_comm, Ordnode.dual_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

Tactic:
simp [dual_rotateL, dual_rotateR, add_comm]

Premises used: Ordnode.dual_rotateR, add_comm, Ordnode.dual_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h_2 : ¬delta * r.size < l.size
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
simp [dual_rotateL, dual_rotateR, add_comm]

Premises used: Ordnode.dual_rotateR, add_comm, Ordnode.dual_rotateL
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ r.dual.rotateR x l.dual = r.dual.rotateL x l.dual

Tactic:
cases delta_lt_false h_1 h_2

Premises used: Ordnode.delta_lt_false
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lrx (Ordnode.singleton lx).dual =
    node 3 (Ordnode.singleton x) lrx (Ordnode.singleton lx)

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lrx (Ordnode.singleton lx).dual =
    node 3 (Ordnode.singleton x) lrx (Ordnode.singleton lx)

Tactic:
try rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lx (node lls llr.dual llx lll.dual) =
    node 3 (Ordnode.singleton x) lx (node lls llr.dual llx lll.dual)

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
⊢ node 3 (Ordnode.singleton x).dual lx (node lls llr.dual llx lll.dual) =
    node 3 (Ordnode.singleton x) lx (node lls llr.dual llx lll.dual)

Tactic:
try rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
pos :
  ∀ (h : lrs < ratio * lls),
    (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
neg :
  ∀ (h : ¬lrs < ratio * lls),
    (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
      node (ls + 1) (node (lrr.dual.size + 1) nil 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 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
      else
        node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + 1) lrr x nil)).dual =
    if lrs < ratio * lls then
      node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)
    else
      node (ls + 1) (node (lrr.dual.size + 1) nil 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 : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil 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 : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : lrs < ratio * lls
⊢ (node (ls + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)).dual =
    node (ls + 1) (node (lrs + 1) nil x (node lrs lrr.dual lrx lrl.dual)) lx (node lls llr.dual llx lll.dual)

Tactic:
repeat simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil 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
x : α
ls : ℕ
lx : α
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
h : ¬lrs < ratio * lls
⊢ (node (ls + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx (node (lrr.size + 1) lrr x nil)).dual =
    node (ls + 1) (node (lrr.dual.size + 1) nil x lrr.dual) lrx
      (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Tactic:
repeat simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.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 : ls > delta * rs
⊢ 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) nil lx (node (rs + size_1 + 1) nil x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            nil)
        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 : 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 (dual nil)
            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 (dual nil)))
          (dual nil))
      (dual nil))

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h : ls > delta * rs
⊢ 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) nil lx (node (rs + size_1 + 1) nil x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            nil)
        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 : 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 (dual nil)
            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 (dual nil)))
          (dual nil))
      (dual nil))

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
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : 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) nil lx (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        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 : 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 (node lrs lrl lrx lrr).dual) lx
                (dual nil)
            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 (dual nil)))
          (node lrs lrl lrx lrr).dual)
      (dual nil))

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h : ls > delta * rs
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : 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) nil lx (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        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 : 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 (node lrs lrl lrx lrr).dual) lx
                (dual nil)
            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 (dual nil)))
          (node lrs lrl lrx lrr).dual)
      (dual nil))

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 α
⊢ 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:
rfl