awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
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
node :
  ∀ (hl : ((Ordnode.node lls lll llx llr).node' lx nil).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx nil).Sized),
    ((Ordnode.node lls lll llx llr).node' lx nil).balance x nil =
      ((Ordnode.node lls lll llx llr).node' lx nil).balance' x nil
node₁ :
  ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α)
    (hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized),
    ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
      ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil
⊢ ((Ordnode.node lls lll llx llr).node' lx lr).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx lr).balance' x nil

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
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 :
  Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else (node' nil lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil
⊢ (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
    (node' nil lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil

Tactic:
dsimp [balance, balance']

Premises used: Ordnode.balance', Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx nil).Sized
node :
  Ordnode.node 3 (Ordnode.node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx nil).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx nil).rotateR x nil
⊢ ((Ordnode.node lls lll llx llr).node' lx nil).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx nil).balance' x nil

Tactic:
dsimp [balance, balance']

Premises used: Ordnode.balance', Ordnode.balance
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized
node :
  (if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)) =
    if lls + lrs + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil
⊢ ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance x nil =
    ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).balance' x nil

Tactic:
dsimp [balance, balance']

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

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ (node lrs lrl lrx lrr).size ≤ 1

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

Tactic:
rwa [size, sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node' nil lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
have : size lrl = 0 ∧ size lrr = 0 := by
          have := balancedSz_zero.1 hl.1.symm
          rwa [size, sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
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
this : lrl.size = 0 ∧ lrr.size = 0
node :
  ∀ (hl : (node' nil lx (Ordnode.node lrs nil lrx lrr)).Balanced)
    (sl : (Ordnode.node ls nil lx (Ordnode.node lrs nil lrx lrr)).Sized)
    (this : size.{u_1} (α := α) nil = 0 ∧ lrr.size = 0),
    Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
      if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs nil lrx lrr)).node' x nil
      else (node' nil lx (Ordnode.node lrs nil lrx lrr)).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else (node' nil lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil

Tactic:
cases sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrx : α
lrr : Ordnode α
hl : (node' nil lx (Ordnode.node lrs nil lrx lrr)).Balanced
sl : (Ordnode.node ls nil lx (Ordnode.node lrs nil lrx lrr)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ lrr.size = 0
node :
  ∀ (hl : (node' nil lx (Ordnode.node lrs nil lrx nil)).Balanced)
    (sl : (Ordnode.node ls nil lx (Ordnode.node lrs nil lrx nil)).Sized)
    (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
    Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
      if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs nil lrx nil)).node' x nil
      else (node' nil lx (Ordnode.node lrs nil lrx nil)).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs nil lrx lrr)).node' x nil
    else (node' nil lx (Ordnode.node lrs nil lrx lrr)).rotateR x nil

Tactic:
cases sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrx : α
hl : (node' nil lx (node lrs nil lrx nil)).Balanced
sl : (node ls nil lx (node lrs nil lrx nil)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ lrs = 1

Tactic:
sl.2.2.1

Premises used: And.right, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrs : ℕ
lrx : α
hl : (node' nil lx (Ordnode.node lrs nil lrx nil)).Balanced
sl : (Ordnode.node ls nil lx (Ordnode.node lrs nil lrx nil)).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
node :
  ∀ (hl : (node' nil lx (Ordnode.node 1 nil lrx nil)).Balanced)
    (sl : (Ordnode.node ls nil lx (Ordnode.node 1 nil lrx nil)).Sized),
    Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
      if HAdd.hAdd (α := ℕ) 0 1 + 1 ≤ 1 then (node' nil lx (Ordnode.node 1 nil lrx nil)).node' x nil
      else (node' nil lx (Ordnode.node 1 nil lrx nil)).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (node' nil lx (Ordnode.node lrs nil lrx nil)).node' x nil
    else (node' nil lx (Ordnode.node lrs nil lrx nil)).rotateR x nil

Tactic:
obtain rfl : lrs = 1 := sl.2.2.1

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

Tactic:
rw [if_neg, rotateR_node, if_neg]

Premises used: Ordnode.rotateR_node, if_neg
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : (node' nil lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) = node4R nil lx (node 1 nil lrx nil) x nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lrx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : (node' nil lx (node 1 nil lrx nil)).Balanced
sl : (node ls nil lx (node 1 nil lrx nil)).Sized
⊢ ¬1 < ratio * 0

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

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ (node lls lll llx llr).size ≤ 1

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

Tactic:
rwa [size, sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ lll.size = 0 ∧ llr.size = 0

Tactic:
have : size lll = 0 ∧ size llr = 0 := by
          have := balancedSz_zero.1 hl.1
          rwa [size, sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx nil).Sized
this : lll.size = 0 ∧ llr.size = 0
node :
  ∀ (hl : ((Ordnode.node lls nil llx llr).node' lx nil).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls nil llx llr) lx nil).Sized)
    (this : size.{u_1} (α := α) nil = 0 ∧ llr.size = 0),
    Ordnode.node 3 (Ordnode.node lls nil llx llr) lx (Ordnode.singleton x) =
      if lls + 1 ≤ 1 then ((Ordnode.node lls nil llx llr).node' lx nil).node' x nil
      else ((Ordnode.node lls nil llx llr).node' lx nil).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx nil).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx nil).rotateR x nil

Tactic:
cases sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
llx : α
llr : Ordnode α
hl : ((Ordnode.node lls nil llx llr).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node lls nil llx llr) lx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ llr.size = 0
node :
  ∀ (hl : ((Ordnode.node lls nil llx nil).node' lx nil).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node lls nil llx nil) lx nil).Sized)
    (this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0),
    Ordnode.node 3 (Ordnode.node lls nil llx nil) lx (Ordnode.singleton x) =
      if lls + 1 ≤ 1 then ((Ordnode.node lls nil llx nil).node' lx nil).node' x nil
      else ((Ordnode.node lls nil llx nil).node' lx nil).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((Ordnode.node lls nil llx llr).node' lx nil).node' x nil
    else ((Ordnode.node lls nil llx llr).node' lx nil).rotateR x nil

Tactic:
cases sl.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 : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
llx : α
hl : ((node lls nil llx nil).node' lx nil).Balanced
sl : (node ls (node lls nil llx nil) lx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
⊢ lls = 1

Tactic:
sl.2.1.1

Premises used: And.right, And.left
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
llx : α
hl : ((Ordnode.node lls nil llx nil).node' lx nil).Balanced
sl : (Ordnode.node ls (Ordnode.node lls nil llx nil) lx nil).Sized
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
node :
  ∀ (hl : ((Ordnode.node 1 nil llx nil).node' lx nil).Balanced)
    (sl : (Ordnode.node ls (Ordnode.node 1 nil llx nil) lx nil).Sized),
    Ordnode.node 3 (Ordnode.node 1 nil llx nil) lx (Ordnode.singleton x) =
      if HAdd.hAdd (α := ℕ) 1 1 ≤ 1 then ((Ordnode.node 1 nil llx nil).node' lx nil).node' x nil
      else ((Ordnode.node 1 nil llx nil).node' lx nil).rotateR x nil
⊢ Ordnode.node 3 (Ordnode.node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((Ordnode.node lls nil llx nil).node' lx nil).node' x nil
    else ((Ordnode.node lls nil llx nil).node' lx nil).rotateR x nil

Tactic:
obtain rfl : lls = 1 := sl.2.1.1

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

Tactic:
rw [if_neg, rotateR_node, if_pos]

Premises used: if_pos, Ordnode.rotateR_node, if_neg
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
llx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = (node 1 nil llx nil).node3R lx nil x nil

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
llx : α
this : size.{u_1} (α := α) nil = 0 ∧ size.{u_1} (α := α) nil = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ 0 < ratio * 1

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

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized
node :
  (if lls + lrs + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)
⊢ (if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)) =
    if lls + lrs + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil

Tactic:
symm
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized
node :
  (if (Ordnode.node lrs lrl lrx lrr).size < ratio * (Ordnode.node lls lll llx llr).size then
      (Ordnode.node lls lll llx llr).node3R lx (Ordnode.node lrs lrl lrx lrr) x nil
    else (Ordnode.node lls lll llx llr).node4R lx (Ordnode.node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)
node₁ : ¬lls + lrs + 1 ≤ 1
⊢ (if lls + lrs + 1 ≤ 1 then ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).node' x nil
    else ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).rotateR x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)

Tactic:
rw [if_neg, rotateR]

Premises used: Ordnode.rotateR, if_neg
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : Balanced.{u_1} (α := α) nil
sr : Sized.{u_1} (α := α) nil
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((Ordnode.node lls lll llx llr).node' lx (Ordnode.node lrs lrl lrx lrr)).Balanced
sl : (Ordnode.node ls (Ordnode.node lls lll llx llr) lx (Ordnode.node lrs lrl lrx lrr)).Sized
node :
  (if lrs < ratio * lls then (Ordnode.node lls lll llx llr).node3R lx (Ordnode.node lrs lrl lrx lrr) x nil
    else (Ordnode.node lls lll llx llr).node4R lx (Ordnode.node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)
⊢ (if (Ordnode.node lrs lrl lrx lrr).size < ratio * (Ordnode.node lls lll llx llr).size then
      (Ordnode.node lls lll llx llr).node3R lx (Ordnode.node lrs lrl lrx lrr) x nil
    else (Ordnode.node lls lll llx llr).node4R lx (Ordnode.node lrs lrl lrx lrr) x nil) =
    if lrs < ratio * lls then
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node lls lll llx llr) lx
        (Ordnode.node (lrs + 1) (Ordnode.node lrs lrl lrx lrr) x nil)
    else
      Ordnode.node (lls + lrs + 1 + 1) (Ordnode.node (lls + lrl.size + 1) (Ordnode.node lls lll llx llr) lx lrl) lrx
        (Ordnode.node (lrr.size + 1) lrr x nil)

Tactic:
dsimp only [size_node]

Premises used: Ordnode.size_node