awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
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
nil :
  ∀ (hr : (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Balanced)
    (sr : (node rs Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Sized),
    node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
      if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then
        node' Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
      else rotateL Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
⊢ 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))

Tactic:
obtain rfl : rrs = 1 := sr.2.2.1

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Balanced
sr : (node rs Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)).Sized
nil :
  node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    node3L Ordnode.nil x Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil)
nil₁ : size.{u_1} (α := α) Ordnode.nil < ratio * (node 1 Ordnode.nil rrx Ordnode.nil).size
nil₂ : ¬0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1
⊢ node 3 (Ordnode.singleton x) rx (node 1 Ordnode.nil rrx Ordnode.nil) =
    if 0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1 then
      node' Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))
    else rotateL Ordnode.nil x (node' Ordnode.nil rx (node 1 Ordnode.nil rrx Ordnode.nil))

Tactic:
rw [if_neg, rotateL_node, if_pos]

Premises used: if_pos, Ordnode.rotateL_node, if_neg
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : (node' nil rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ node 3 (Ordnode.singleton x) rx (node 1 nil rrx nil) = node3L nil x nil rx (node 1 nil rrx 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 rrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : (node' nil rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ 0 < ratio * 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : (node' nil rx (node 1 nil rrx nil)).Balanced
sr : (node rs nil rx (node 1 nil rrx nil)).Sized
⊢ ¬0 + (HAdd.hAdd (α := ℕ) 0 1 + 1) ≤ 1

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ (node rls rll rlx rlr).size ≤ 1

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

Tactic:
rwa [size, sr.2.1.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 : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
⊢ rll.size = 0 ∧ rlr.size = 0

Tactic:
have : size rll = 0 ∧ size rlr = 0 := by
          have := balancedSz_zero.1 hr.1
          rwa [size, sr.2.1.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 : α
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
this : rll.size = 0 ∧ rlr.size = 0
nil :
  ∀ (hr : ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.nil).Balanced)
    (sr : (node rs (node rls Ordnode.nil rlx rlr) rx Ordnode.nil).Sized)
    (this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ rlr.size = 0),
    node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
      if 0 + (rls + 1) ≤ 1 then node' Ordnode.nil x ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.nil)
      else rotateL Ordnode.nil x ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.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)

Tactic:
cases sr.2.1.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 : α
rls : ℕ
rlx : α
rlr : Ordnode α
hr : ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.nil).Balanced
sr : (node rs (node rls Ordnode.nil rlx rlr) rx Ordnode.nil).Sized
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ rlr.size = 0
nil :
  ∀ (hr : ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced)
    (sr : (node rs (node rls Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized)
    (this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0),
    node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
      if 0 + (rls + 1) ≤ 1 then node' Ordnode.nil x ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
      else rotateL Ordnode.nil x ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' Ordnode.nil x ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node rls Ordnode.nil rlx rlr).node' rx Ordnode.nil)

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

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} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx : α
rls : ℕ
rlx : α
hr : ((node rls nil rlx nil).node' rx nil).Balanced
sr : (node rs (node rls nil rlx nil) rx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ rls = 1

Tactic:
sr.2.1.1

Premises used: And.right, And.left
-- 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 : ℕ
rlx : α
hr : ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced
sr : (node rs (node rls Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
nil :
  ∀ (hr : ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced)
    (sr : (node rs (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized),
    node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
      if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then
        node' Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
      else rotateL Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + (rls + 1) ≤ 1 then node' Ordnode.nil x ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node rls Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)

Tactic:
obtain rfl : rls = 1 := sr.2.1.1

Premises used: And.right, And.left, rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) Ordnode.nil
sl : Sized.{u_1} (α := α) Ordnode.nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) Ordnode.nil = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 0
hr : ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil).Balanced
sr : (node rs (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil).Sized
nil :
  node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    node4L Ordnode.nil x (node 1 Ordnode.nil rlx Ordnode.nil) rx Ordnode.nil
nil₁ : ¬(node 1 Ordnode.nil rlx Ordnode.nil).size < ratio * size.{u_1} (α := α) Ordnode.nil
nil₂ : ¬0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) =
    if 0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then
      node' Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)
    else rotateL Ordnode.nil x ((node 1 Ordnode.nil rlx Ordnode.nil).node' rx Ordnode.nil)

Tactic:
rw [if_neg, rotateL_node, if_neg]

Premises used: Ordnode.rotateL_node, if_neg
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = node4L nil x (node 1 nil rlx 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 rlx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬1 < ratio * 0

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) nil
rs : ℕ
rx rlx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ ¬0 + HAdd.hAdd (α := ℕ) 1 1 ≤ 1

Tactic:
decide
-- 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 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))) =
    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 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))

Tactic:
symm
-- 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 (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      node3L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    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))
nil₁ : ¬rls + rrs + 1 ≤ 1
⊢ (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))) =
    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))

Tactic:
rw [zero_add, if_neg, rotateL]

Premises used: zero_add, Ordnode.rotateL, if_neg
-- 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 node3L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    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 (node rls rll rlx rlr).size < ratio * (node rrs rrl rrx rrr).size then
      node3L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L Ordnode.nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    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))

Tactic:
dsimp only [size_node]

Premises used: Ordnode.size_node
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
pos :
  rls < ratio * rrs →
    node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
neg :
  ¬rls < ratio * rrs →
    node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))
⊢ (if rls < ratio * rrs then node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
split_ifs
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
h : rls < ratio * rrs
pos : rls + 1 + rrs = rls + rrs + 1
⊢ node3L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rls + 1) nil x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

Tactic:
simp [node3L, node']

Premises used: Ordnode.node', Ordnode.node3L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
h : rls < ratio * rrs
⊢ rls + 1 + rrs = rls + rrs + 1

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
h : ¬rls < ratio * rrs
neg : rll.size + 1 + (rlr.size + rrs + 1) = rll.size + rlr.size + 1 + rrs + 1
⊢ node4L nil x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
simp [node4L, node', sr.2.1.1]

Premises used: Ordnode.node', And.right, And.left, Ordnode.node4L
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
h : ¬rls < ratio * rrs
⊢ rll.size + 1 + (rlr.size + rrs + 1) = rll.size + rlr.size + 1 + rrs + 1

Tactic:
abel
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
⊢ ¬rls + rrs + 1 ≤ 1

Tactic:
not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))

Premises used: add_pos, Nat.succ_lt_succ, Ordnode.Sized.pos, And.right, And.left, not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
hl : Balanced.{u_1} (α := α) nil
sl : Sized.{u_1} (α := α) 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
⊢ ¬rls + rrs + 1 ≤ 1

Tactic:
exact not_le_of_gt (Nat.succ_lt_succ (add_pos sr.2.1.pos sr.2.2.pos))

Premises used: add_pos, Nat.succ_lt_succ, Ordnode.Sized.pos, And.right, And.left, not_le_of_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
r : Ordnode α
hr : r.Balanced
sr : r.Sized
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (Ordnode.node ls ll lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
node :
  ∀ (hr : Balanced.{u_1} (α := α) nil) (sr : Sized.{u_1} (α := α) nil),
    (Ordnode.node ls ll lx lr).balance x nil = (Ordnode.node ls ll lx lr).balance' x nil
node₁ :
  ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) (hr : (Ordnode.node rs rl rx rr).Balanced)
    (sr : (Ordnode.node rs rl rx rr).Sized),
    (Ordnode.node ls ll lx lr).balance x (Ordnode.node rs rl rx rr) =
      (Ordnode.node ls ll lx lr).balance' x (Ordnode.node rs rl rx rr)
⊢ (Ordnode.node ls ll lx lr).balance x r = (Ordnode.node ls ll lx lr).balance' x r

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

Tactic:
rw [sl.eq_node'] at hl ⊢

Premises used: Ordnode.Sized.eq_node'
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (ll.node' lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
node :
  ∀ (hl : (node' nil lx lr).Balanced) (sl : (Ordnode.node ls nil lx lr).Sized),
    (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil
node₁ :
  ∀ (lls : ℕ) (lll : Ordnode α) (llx : α) (llr : Ordnode α) (hl : ((Ordnode.node lls lll llx llr).node' lx lr).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx lr).Sized),
    ((Ordnode.node lls lll llx llr).node' lx lr).balance x nil =
      ((Ordnode.node lls lll llx llr).node' lx lr).balance' x nil
⊢ (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
hl : (node' nil lx lr).Balanced
sl : (Ordnode.node ls nil lx lr).Sized
node :
  ∀ (hl : (node' nil lx nil).Balanced) (sl : (Ordnode.node ls nil lx nil).Sized),
    (node' nil lx nil).balance x nil = (node' nil lx nil).balance' x nil
node₁ :
  ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α)
    (hl : (node' nil lx (Ordnode.node lrs lrl lrx lrr)).Balanced)
    (sl : (Ordnode.node ls nil lx (Ordnode.node lrs lrl lrx lrr)).Sized),
    (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
      (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil
⊢ (node' nil lx lr).balance x nil = (node' nil lx lr).balance' x nil

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr