awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
rw : ((node sz l' y r').eraseMin.balanceR x r).dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₁ : r.dual.balanceL x (node sz l' y r').eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax
rw₂ : r.dual.balanceL x (node sz l' y r').dual.eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₃ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size (node sz l' y r') x r).dual.eraseMax
rw₄ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz l' y r').dual).eraseMax
rw₅ : r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = (node size r.dual x (node sz r'.dual y l'.dual)).eraseMax
rw₆ rw₇ :
  r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax = r.dual.balanceL x (node sz r'.dual y l'.dual).eraseMax
⊢ (node size (node sz l' y r') x r).eraseMin.dual = (node size (node sz l' y r') x r).dual.eraseMax

Tactic:
rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]

Premises used: Ordnode.eraseMin, Ordnode.dual_balanceR, Ordnode.node, Ordnode.eraseMax, Ordnode.dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
rw : t.eraseMax.dual = t.dual.eraseMin.dual.dual
rw₁ : t.eraseMax.dual = t.dual.dual.eraseMax.dual
rw₂ rw₃ : t.eraseMax.dual = t.eraseMax.dual
⊢ t.eraseMax.dual = t.dual.eraseMin

Tactic:
rw [← dual_dual (eraseMin _), dual_eraseMin, dual_dual]

Premises used: Ordnode.eraseMin, Ordnode.dual_eraseMin, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x_1 ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
rw :
  (match (motive := α × Ordnode α → α × Ordnode α) ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₁ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₂ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    (ll.findMin' lx, (node x_1 (node ls ll lx lr) x r).eraseMin)
rw₃ rw₄ :
  (match (motive := α × Ordnode α → α × Ordnode α) (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    (ll.findMin' lx, (node ls ll lx lr).eraseMin.balanceR x r)
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x_1 (node ls ll lx lr) x r).eraseMin)

Tactic:
rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]

Premises used: Ordnode.eraseMin, Ordnode.splitMin', Ordnode.findMin'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x_1 : ℕ
l : Ordnode α
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rw :
  (match (motive := Ordnode α × α → Ordnode α × α) ll.splitMax' lx lr with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
rw₁ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))
rw₂ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' lx lr)
rw₃ rw₄ :
  (match (motive := Ordnode α × α → Ordnode α × α) ((node ls ll lx lr).eraseMax, findMax' lx lr) with
    | (r', xm) => (l.balanceL x r', xm)) =
    (l.balanceL x (node ls ll lx lr).eraseMax, findMax' lx lr)
⊢ l.splitMax' x (node ls ll lx lr) = ((node x_1 l x (node ls ll lx lr)).eraseMax, findMax' x (node ls ll lx lr))

Tactic:
rw [splitMax', splitMax_eq ls ll lx lr, findMax', eraseMax]

Premises used: Ordnode.eraseMax, Ordnode.splitMax', Ordnode.findMax'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
nil : Eq.{u_1 + 1} (α := Ordnode α) (merge Ordnode.nil Ordnode.nil) Ordnode.nil
node :
  ∀ (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
    (Ordnode.node size l x r).merge Ordnode.nil = Ordnode.node size l x r
⊢ t.merge Ordnode.nil = t

Tactic:
cases t
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Ordnode α) (merge nil nil) nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node size l x r).merge nil = node size l x r

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
t : Ordnode α
⊢ merge nil t = t

Tactic:
rfl

Premises used: Ordnode.merge, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ (node ls ll lx lr).merge (node rs rl rx rr) =
    if delta * ls < rs then ((node ls ll lx lr).merge rl).balanceL rx rr
    else
      if delta * rs < ls then ll.balanceR lx (lr.merge (node rs rl rx rr))
      else (node ls ll lx lr).glue (node rs rl rx rr)

Tactic:
rfl

Premises used: Ordnode.merge, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ cmpLE x y = cmpLE y x

Tactic:
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
rw :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
⊢ (Ordnode.insert x (node size l y r)).dual = Ordnode.insert x (node size l y r).dual

Tactic:
rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]

Premises used: Ordnode.insert, Ordnode.dual, cmpLE_swap
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
lt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
eq :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.eq.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
gt :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.gt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))

Tactic:
cases cmpLE x y

Premises used: cmpLE
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))

Tactic:
simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]

Premises used: Ordnode.dual_balanceL, Ordering.swap, Ordnode.dual_balanceR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.eq.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))

Tactic:
simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]

Premises used: Ordnode.dual_balanceL, Ordering.swap, Ordnode.dual_balanceR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x : α
size : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (match (motive := Ordering → Ordnode α) Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)))
    (match (motive := Ordering → Ordnode αᵒᵈ) Ordering.gt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual))

Tactic:
simp [Ordering.swap, dual_balanceL, dual_balanceR, dual_insert]

Premises used: Ordnode.dual_balanceL, Ordering.swap, Ordnode.dual_balanceR
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
nil :
  ∀ (hl : Balanced.{u_1} (α := α) Ordnode.nil) (sl : Sized.{u_1} (α := α) Ordnode.nil),
    balance Ordnode.nil x r = balance' Ordnode.nil x r
node :
  ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α) (hl : (Ordnode.node ls ll lx lr).Balanced)
    (sl : (Ordnode.node ls ll lx lr).Sized),
    (Ordnode.node ls ll lx lr).balance x r = (Ordnode.node ls ll lx lr).balance' x r
⊢ l.balance x r = l.balance' x r

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
nil :
  ∀ (hr : Balanced.{u_1} (α := α) Ordnode.nil) (sr : Sized.{u_1} (α := α) Ordnode.nil),
    balance Ordnode.nil x Ordnode.nil = balance' Ordnode.nil x Ordnode.nil
nil₁ :
  ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (hr : (node rs rl rx rr).Balanced)
    (sr : (node rs rl rx rr).Sized),
    balance Ordnode.nil x (node rs rl rx rr) = balance' Ordnode.nil x (node rs rl rx rr)
⊢ balance Ordnode.nil x r = balance' Ordnode.nil x r

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
⊢ balance nil x nil = balance' nil x nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
nil :
  ∀ (hr : (rl.node' rx rr).Balanced) (sr : (node rs rl rx rr).Sized),
    balance Ordnode.nil x (rl.node' rx rr) = balance' Ordnode.nil x (rl.node' rx rr)
⊢ balance Ordnode.nil x (node rs rl rx rr) = balance' Ordnode.nil x (node rs rl rx rr)

Tactic:
rw [sr.eq_node'] at hr ⊢

Premises used: Ordnode.Sized.eq_node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (rl.node' rx rr).Balanced
sr : (node rs rl rx rr).Sized
nil :
  ∀ (hr : (node' Ordnode.nil rx rr).Balanced) (sr : (node rs Ordnode.nil rx rr).Sized),
    balance Ordnode.nil x (node' Ordnode.nil rx rr) = balance' Ordnode.nil x (node' Ordnode.nil rx rr)
nil₁ :
  ∀ (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) (hr : ((node rls rll rlx rlr).node' rx rr).Balanced)
    (sr : (node rs (node rls rll rlx rlr) rx rr).Sized),
    balance Ordnode.nil x ((node rls rll rlx rlr).node' rx rr) =
      balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx rr)
⊢ balance Ordnode.nil x (rl.node' rx rr) = balance' Ordnode.nil x (rl.node' rx rr)

Tactic:
obtain - | ⟨rls, rll, rlx, rlr⟩ := rl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rr : Ordnode α
hr : (node' Ordnode.nil rx rr).Balanced
sr : (node rs Ordnode.nil rx rr).Sized
nil :
  ∀ (hr : (node' Ordnode.nil rx Ordnode.nil).Balanced) (sr : (node rs Ordnode.nil rx Ordnode.nil).Sized),
    balance Ordnode.nil x (node' Ordnode.nil rx Ordnode.nil) = balance' Ordnode.nil x (node' Ordnode.nil rx Ordnode.nil)
nil₁ :
  ∀ (rrs : ℕ) (rrl : Ordnode α) (rrx : α) (rrr : Ordnode α)
    (hr : (node' Ordnode.nil rx (node rrs rrl rrx rrr)).Balanced)
    (sr : (node rs Ordnode.nil rx (node rrs rrl rrx rrr)).Sized),
    balance Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr)) =
      balance' Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))
⊢ balance Ordnode.nil x (node' Ordnode.nil rx rr) = balance' Ordnode.nil x (node' Ordnode.nil rx rr)

Tactic:
obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
nil :
  ∀ (hr : ((node rls rll rlx rlr).node' rx Ordnode.nil).Balanced)
    (sr : (node rs (node rls rll rlx rlr) rx Ordnode.nil).Sized),
    balance Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil) =
      balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil)
nil₁ :
  ∀ (rrs : ℕ) (rrl : Ordnode α) (rrx : α) (rrr : Ordnode α)
    (hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced)
    (sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized),
    balance Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
      balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
⊢ balance Ordnode.nil x ((node rls rll rlx rlr).node' rx rr) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx rr)

Tactic:
obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' Ordnode.nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs Ordnode.nil rx (node rrs rrl rrx rrr)).Sized
nil :
  node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))
⊢ balance Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr)) =
    balance' Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))

Tactic:
dsimp +instances [balance, balance']

Premises used: Ordnode.balance', Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx Ordnode.nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx Ordnode.nil).Sized
nil :
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil)
⊢ balance Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx Ordnode.nil)

Tactic:
dsimp +instances [balance, balance']

Premises used: Ordnode.balance', Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
nil :
  (if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) Ordnode.nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))) =
    if 0 + (rls + rrs + 1) ≤ 1 then node' Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
    else rotateL Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))
⊢ balance Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)) =
    balance' Ordnode.nil x ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr))

Tactic:
dsimp +instances [balance, balance']

Premises used: Ordnode.balance', Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
hr : (node' nil rx nil).Balanced
sr : (node rs nil rx nil).Sized
⊢ node 2 nil x (node' nil rx nil) = node' nil x (node' nil rx nil)

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ (node rrs rrl rrx rrr).size ≤ 1

Tactic:
have := balancedSz_zero.1 hr.1.symm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : (node rrs rrl rrx rrr).size ≤ 1
rwa : ∀ (this : rrs ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₁ : ∀ (this : rrl.size + rrr.size + 1 ≤ 1), rrl.size = 0 ∧ rrr.size = 0
rwa₂ : ∀ (this : rrl.size + rrr.size ≤ 0), rrl.size = 0 ∧ rrr.size = 0
rwa₃ : ∀ (this : rrl.size + rrr.size = 0), rrl.size = 0 ∧ rrr.size = 0
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (this : rrl.size = 0 ∧ rrr.size = 0), rrl.size = 0 ∧ rrr.size = 0
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Premises used: Nat.le_zero, Ordnode.size, And.right, And.left, Nat.succ_le_succ_iff, add_eq_zero
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
have : size rrl = 0 ∧ size rrr = 0 := by
          have := balancedSz_zero.1 hr.1.symm
          rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node' Ordnode.nil rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs Ordnode.nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size = 0 ∧ rrr.size = 0
nil :
  ∀ (hr : (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr)).Balanced)
    (sr : (node rs Ordnode.nil rx (node rrs Ordnode.nil rrx rrr)).Sized)
    (this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ rrr.size = 0),
    node 3 (Ordnode.singleton x) rx (node rrs Ordnode.nil rrx rrr) =
      if 0 + (0 + rrs + 1) ≤ 1 then node' Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr))
      else rotateL Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr))
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node rrs rrl rrx rrr))

Tactic:
cases sr.2.2.2.1.size_eq_zero.1 this.1

Premises used: Ordnode.Sized.size_eq_zero, And.right, And.left, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr)).Balanced
sr : (node rs Ordnode.nil rx (node rrs Ordnode.nil rrx rrr)).Sized
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ rrr.size = 0
nil :
  ∀ (hr : (node' Ordnode.nil rx (node rrs Ordnode.nil rrx Ordnode.nil)).Balanced)
    (sr : (node rs Ordnode.nil rx (node rrs Ordnode.nil rrx Ordnode.nil)).Sized)
    (this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0),
    node 3 (Ordnode.singleton x) rx (node rrs Ordnode.nil rrx Ordnode.nil) =
      if 0 + (0 + rrs + 1) ≤ 1 then node' Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx Ordnode.nil))
      else rotateL Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx Ordnode.nil))
⊢ node 3 (Ordnode.singleton x) rx (node rrs Ordnode.nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then node' Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node rrs Ordnode.nil rrx rrr))

Tactic:
cases sr.2.2.2.2.size_eq_zero.1 this.2

Premises used: Ordnode.Sized.size_eq_zero, And.right, Iff.mp
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rrs : ℕ
rrx : α
hr : (node' nil rx (node rrs nil rrx nil)).Balanced
sr : (node rs nil rx (node rrs nil rrx nil)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ rrs = 1

Tactic:
sr.2.2.1

Premises used: And.right, And.left