awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
⊢ Valid' o₁ nil o₂

Tactic:
⟨h, ⟨⟩, ⟨⟩⟩

Premises used: Ordnode.Valid'.mk, True.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
⊢ Valid.{u_1} (α := α) nil

Tactic:
valid'_nil ⟨⟩

Premises used: Ordnode.Valid, Ordnode.valid'_nil, True.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H : BalancedSz l.size r.size
hs : s = l.size + r.size + 1
⊢ Valid' o₁ (Ordnode.node s l x r) o₂

Tactic:
⟨⟨hl.1, hr.1⟩, ⟨hs, hl.2, hr.2⟩, ⟨H, hl.3, hr.3⟩⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, And.intro, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
lo : WithBot α
hi : WithTop α
ol : l.Bounded lo (↑x : WithTop α)
Or : r.Bounded (↑x : WithBot α) hi
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x : WithTop α) lo
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi (↑x : WithBot α)
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ l.size + r.size + 1 = r.dual.size + l.dual.size + 1

Tactic:
simp [size_dual, add_comm]

Premises used: Ordnode.size_dual, add_comm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
lo : WithBot α
hi : WithTop α
ol : l.Bounded lo (↑x : WithTop α)
Or : r.Bounded (↑x : WithBot α) hi
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x : WithTop α) lo
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi (↑x : WithBot α)
sr' : r.dual.Sized
br' : r.dual.Balanced
rw : BalancedSz r.size l.size
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Premises used: Ordnode.size_dual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
lo : WithBot α
hi : WithTop α
ol : l.Bounded lo (↑x : WithTop α)
Or : r.Bounded (↑x : WithBot α) hi
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x : WithTop α) lo
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi (↑x : WithBot α)
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size

Tactic:
b.symm

Premises used: Ordnode.BalancedSz.symm, OrderDual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
lo : WithBot α
hi : WithTop α
ol : l.Bounded lo (↑x : WithTop α)
Or : r.Bounded (↑x : WithBot α) hi
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x : WithTop α) lo
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi (↑x : WithBot α)
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Premises used: Ordnode.BalancedSz.symm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
⊢ Valid' o₁ t.dual.dual o₂

Tactic:
have := Valid'.dual h
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
rwa : ∀ (this : Valid' o₁ t o₂), Valid' o₁ t o₂
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : Valid' o₁ t o₂), Valid' o₁ t o₂
⊢ Valid' o₁ t o₂

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

Premises used: OrderDual.Preorder.dual_dual, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
⊢ t.Valid → t.dual.Valid

Tactic:
Valid'.dual

Premises used: Ordnode.Valid, OrderDual, Ordnode.Valid'.dual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
⊢ t.Valid ↔ t.dual.Valid

Tactic:
Valid'.dual_iff

Premises used: Ordnode.Valid, OrderDual, Ordnode.Valid'.dual_iff
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' o₁ l (↑x : WithTop α)

Tactic:
⟨H.1.1, H.2.2.1, H.3.2.1⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, And.right, And.left, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑x : WithBot α) r o₂

Tactic:
⟨H.1.2, H.2.2.2, H.3.2.2⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, And.right, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
H : (node s l x r).Valid
⊢ l.Valid

Tactic:
H.left.valid

Premises used: Ordnode.Valid'.valid, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
H : (node s l x r).Valid
⊢ r.Valid

Tactic:
H.right.valid

Premises used: Ordnode.Valid'.valid, Ordnode.Valid'.right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
H : (node s l x r).Valid
⊢ (node s l x r).size = l.size + r.size + 1

Tactic:
H.2.1

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H : BalancedSz l.size r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
hl.node hr H rfl

Premises used: rfl, Ordnode.Valid'.node
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
x : α
o₁ : WithBot α
o₂ : WithTop α
h₁ : Bounded nil o₁ (↑x : WithTop α)
h₂ : Bounded nil (↑x : WithBot α) o₂
⊢ Valid' o₁ {x} o₂

Tactic:
(valid'_nil h₁).node (valid'_nil h₂) (Or.inl zero_le_one) rfl

Premises used: zero_le_one, Or.inl, rfl, Ordnode.Valid'.node, Ordnode.valid'_nil
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
x : α
⊢ Valid (α := α) {x}

Tactic:
valid'_singleton ⟨⟩ ⟨⟩

Premises used: Ordnode.Valid, Ordnode.valid'_singleton, True.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hm : Valid' (↑x : WithBot α) m (↑y : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
H1 : BalancedSz l.size m.size
H2 : BalancedSz (l.size + m.size + 1) r.size
⊢ Valid' o₁ (l.node3L x m y r) o₂

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

Premises used: Ordnode.node3L, Ordnode.Valid'.node'
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hm : Valid' (↑x : WithBot α) m (↑y : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
H1 : BalancedSz l.size (m.size + r.size + 1)
H2 : BalancedSz m.size r.size
⊢ Valid' o₁ (l.node3R x m y r) o₂

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

Premises used: Ordnode.node3R, Ordnode.Valid'.node'
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ b < 3 * a + 1

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
b c d : ℕ
mr₂ : b + c + 1 ≤ 3 * d
⊢ c ≤ 3 * d

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
b c d : ℕ
mr₁ : 2 * d ≤ b + c + 1
mm₁ : b ≤ 3 * c
⊢ d ≤ 3 * c

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
a b c d : ℕ
lr₁ : 3 * a ≤ b + c + 1 + d
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ a + b + 1 ≤ 3 * (c + d + 1)

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₁ : 2 * d ≤ b + c + 1
mm₂ : c ≤ 3 * b
⊢ c + d + 1 ≤ 3 * (a + b + 1)

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hm : Valid' (↑x : WithBot α) m (↑y : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
Hm : 0 < m.size
H :
  l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ m.size ∧
        delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size
nil :
  ∀ (hm : Valid' (↑x : WithBot α) Ordnode.nil (↑y : WithTop α)) (Hm : 0 < size.{u_1} (α := α) Ordnode.nil)
    (H :
      l.size = 0 ∧ size.{u_1} (α := α) Ordnode.nil = 1 ∧ r.size ≤ 1 ∨
        0 < l.size ∧
          ratio * r.size ≤ size.{u_1} (α := α) Ordnode.nil ∧
            delta * l.size ≤ size.{u_1} (α := α) Ordnode.nil + r.size ∧
              3 * (size.{u_1} (α := α) Ordnode.nil + r.size) ≤ 16 * l.size + 9 ∧
                size.{u_1} (α := α) Ordnode.nil ≤ delta * r.size),
    Valid' o₁ (l.node4L x Ordnode.nil y r) o₂
node :
  ∀ (s : ℕ) (ml : Ordnode α) (z : α) (mr : Ordnode α)
    (hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)) (Hm : 0 < (Ordnode.node s ml z mr).size)
    (H :
      l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
        0 < l.size ∧
          ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
            delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
              3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
                (Ordnode.node s ml z mr).size ≤ delta * r.size),
    Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
⊢ Valid' o₁ (l.node4L x m y r) o₂

Tactic:
obtain - | ⟨s, ml, z, mr⟩ := m
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
hm : Valid' (↑x : WithBot α) nil (↑y : WithTop α)
Hm : 0 < size.{u_1} (α := α) nil
H :
  l.size = 0 ∧ size.{u_1} (α := α) nil = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ size.{u_1} (α := α) nil ∧
        delta * l.size ≤ size.{u_1} (α := α) nil + r.size ∧
          3 * (size.{u_1} (α := α) nil + r.size) ≤ 16 * l.size + 9 ∧ size.{u_1} (α := α) nil ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x nil y r) o₂

Tactic:
cases Hm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
node : BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂

Tactic:
suffices
    BalancedSz (size l) (size ml) ∧
      BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1) from
    Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
node :
  ∀ (l0 : l.size = 0) (m1 : (Ordnode.node s ml z mr).size = 1) (r0 : r.size ≤ 1),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
node₁ :
  ∀ (l0 : 0 < l.size) (mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size)
    (lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size)
    (lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9)
    (mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
⊢ ml.size = 0 ∧ mr.size = 0

Tactic:
rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1

Premises used: Nat.succ_inj, Ordnode.Valid'.sz, add_eq_zero, Ordnode.Sized.size_eq
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : (Ordnode.node s ml z mr).size = 1
r0 : r.size ≤ 1
m1₁ : ml.size = 0 ∧ mr.size = 0
⊢ r.size ≤ 1

Tactic:
rw [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1

Premises used: Nat.succ_inj, Ordnode.Valid'.sz, add_eq_zero, Ordnode.Sized.size_eq
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
node : BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [l0, m1.1, m1.2]

Premises used: And.right, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
r0 : r.size ≤ 1
node :
  ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)
⊢ BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)

Tactic:
revert r0
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
node₁ :
  ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
node₂ :
  ∀ (n : ℕ) (r0 : n + 1 + 1 ≤ 1),
    BalancedSz 0 0 ∧ BalancedSz 0 (n + 1 + 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + (n + 1 + 1) + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)

Tactic:
rcases size r with (_ | _ | _)

Premises used: Ordnode.size
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
n : ℕ
r0 : n + 1 + 1 ≤ 1
⊢ (HAdd.hAdd (α := ℕ) 0 0 ≤ 1 ∨ 0 ≤ HMul.hMul (α := ℕ) 3 0 ∧ 0 ≤ HMul.hMul (α := ℕ) 3 0) ∧
    (0 + (n + 1 + 1) ≤ 1 ∨ 0 ≤ 3 * (n + 1 + 1) ∧ n + 1 + 1 ≤ HMul.hMul (α := ℕ) 3 0) ∧
      (HAdd.hAdd (α := ℕ) 0 0 + 1 + (0 + (n + 1 + 1) + 1) ≤ 1 ∨
        HAdd.hAdd (α := ℕ) 0 0 + 1 ≤ 3 * (0 + (n + 1 + 1) + 1) ∧ 0 + (n + 1 + 1) + 1 ≤ 3 * (HAdd.hAdd (α := ℕ) 0 0 + 1))

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
node :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
node₁ :
  ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
node₂ :
  ∀ (n : ℕ) (r0 : n + 1 + 1 ≤ 1),
    BalancedSz 0 0 ∧ BalancedSz 0 (n + 1 + 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + (n + 1 + 1) + 1)
node₃ :
  ∀ (r0 : LE.le (α := ℕ) 0 1),
    BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (HAdd.hAdd (α := ℕ) 0 0 + 1)
node₄ :
  ∀ (r0 : HAdd.hAdd (α := ℕ) 0 1 ≤ 1),
    BalancedSz 0 0 ∧
      BalancedSz 0 (HAdd.hAdd (α := ℕ) 0 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + HAdd.hAdd (α := ℕ) 0 1 + 1)
node₅ :
  ∀ (n : ℕ) (r0 : n + 1 + 1 ≤ 1),
    BalancedSz 0 0 ∧ BalancedSz 0 (n + 1 + 1) ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + (n + 1 + 1) + 1)
⊢ ∀ (r0 : r.size ≤ 1), BalancedSz 0 0 ∧ BalancedSz 0 r.size ∧ BalancedSz (HAdd.hAdd (α := ℕ) 0 0 + 1) (0 + r.size + 1)

Tactic:
rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]

Premises used: Ordnode.size, Ordnode.delta, Ordnode.BalancedSz
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
node :
  ∀ (r0 : r.size = 0),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
node₁ :
  ∀ (r0 : r.size > 0),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rcases Nat.eq_zero_or_pos (size r) with r0 | r0

Premises used: Ordnode.size, Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size = 0
⊢ (Ordnode.node s ml z mr).size ≤ delta * 0

Tactic:
rw [r0] at mr₂
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size = 0
mr₃ : (Ordnode.node s ml z mr).size ≤ delta * 0
⊢ r.size = 0

Tactic:
rw [r0] at mr₂
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑y : WithBot α) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x : WithBot α) (Ordnode.node s ml z mr) (↑y : WithTop α)
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * 0
r0 : r.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
cases not_le_of_gt Hm mr₂

Premises used: not_le_of_gt