awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n n_1 : ℕ
mm : n + 1 + (n_1 + 1) ≤ 1
⊢ (n + (n_1 + 1)).succ ≤ 1

Tactic:
rw [Nat.succ_add] at mm

Premises used: Nat.succ_add
-- 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + HAdd.hAdd (α := ℕ) 1 1
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
n n_1 : ℕ
mm : (n + (n_1 + 1)).succ ≤ 1
⊢ BalancedSz 1 (n + 1) ∧ BalancedSz (n_1 + 1) 1 ∧ BalancedSz (1 + (n + 1) + 1) (n_1 + 1 + 1 + 1)

Tactic:
rcases mm with (_ | ⟨⟨⟩⟩)
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
⊢ ml.size ≤ delta * mr.size

Tactic:
rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩

Premises used: Ordnode.Valid'.bal, Or.resolve_left, 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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
⊢ mr.size ≤ delta * ml.size

Tactic:
rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩

Premises used: Ordnode.Valid'.bal, Or.resolve_left, 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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
neg :
  ∀ (ml0 : ml.size = 0),
    BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
neg₁ :
  ∀ (ml0 : ml.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 ml) with ml0 | ml0

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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size = 0
⊢ mr.size = 0

Tactic:
rw [ml0, mul_zero, Nat.le_zero] at mm₂

Premises used: Nat.le_zero, MulZeroClass.mul_zero
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size = 0
mm₃ : mr.size = 0
⊢ ml.size = 0

Tactic:
rw [ml0, mul_zero, Nat.le_zero] at mm₂

Premises used: Nat.le_zero, MulZeroClass.mul_zero
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
⊢ ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1

Tactic:
rw [ml0, mm₂] at mm
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
mm₃ : ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1
⊢ ml.size ≤ delta * mr.size

Tactic:
rw [ml0, mm₂] at mm
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
mm₃ : ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1
mm₄ : ml.size ≤ delta * mr.size
⊢ mr.size = 0

Tactic:
rw [ml0, mm₂] at mm
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
mm₃ : ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1
mm₄ : ml.size ≤ delta * mr.size
mm₅ : mr.size = 0
⊢ ml.size = 0

Tactic:
rw [ml0, mm₂] at mm
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
⊢ 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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬HAdd.hAdd (α := ℕ) 0 0 ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.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 mm (by 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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
⊢ ratio * (delta * l.size) ≤ ratio * (ml.size + mr.size + 1 + r.size)

Tactic:
have := Nat.mul_le_mul_left ratio lr₁
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : ratio * (delta * l.size) ≤ ratio * (ml.size + mr.size + 1 + r.size)
⊢ delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size

Tactic:
rw [mul_left_comm, mul_add] at this

Premises used: mul_left_comm, mul_add
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
⊢ delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + (ml.size + mr.size + 1)

Tactic:
have := le_trans this (add_le_add_right 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this_1 : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + (ml.size + mr.size + 1)
⊢ delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)

Tactic:
rw [← Nat.succ_mul] at this

Premises used: Nat.succ_mul
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this_1 : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)
⊢ 0 < delta

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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this_1 : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)
⊢ 2 * l.size ≤ ml.size + mr.size + 1

Tactic:
exact (mul_le_mul_iff_right₀ (by decide)).1 this

Premises used: Iff.mp, mul_le_mul_iff_right₀
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
⊢ 2 * l.size ≤ ml.size + mr.size + 1

Tactic:
have : 2 * size l ≤ size ml + size mr + 1 := by
      have := Nat.mul_le_mul_left ratio lr₁
      rw [mul_left_comm, mul_add] at this
      have := le_trans this (add_le_add_right mr₁ _)
      rw [← Nat.succ_mul] at this
      exact (mul_le_mul_iff_right₀ (by decide)).1 this
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩

Premises used: And.intro, Or.inr
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
neg : l.size ≤ delta * ml.size
neg₁ : ml.size ≤ delta * l.size
neg₂ : mr.size ≤ delta * r.size
neg₃ : r.size ≤ delta * mr.size
neg₄ : l.size + ml.size + 1 ≤ delta * (mr.size + r.size + 1)
neg₅ : mr.size + r.size + 1 ≤ delta * (l.size + ml.size + 1)
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ LT.lt (α := ℕ) 0 2

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 : 0 < l.size
mr₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
neg : ml.size + mr.size + 1 ≤ 2 * (delta * ml.size)
⊢ l.size ≤ delta * ml.size

Tactic:
refine (mul_le_mul_iff_right₀ (by decide)).1 (le_trans this ?_)

Premises used: Iff.mp, mul_le_mul_iff_right₀, le_trans
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
neg : ml.size + mr.size < delta * ml.size + delta * ml.size
⊢ ml.size + mr.size + 1 ≤ 2 * (delta * ml.size)

Tactic:
rw [two_mul, Nat.succ_le_iff]

Premises used: two_mul, Nat.succ_le_iff
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ ml.size + mr.size < delta * ml.size + delta * ml.size

Tactic:
add_lt_add_of_lt_of_le ?_ mm₂

Premises used: add_lt_add_of_lt_of_le
-- 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
neg : ml.size < delta * ml.size
⊢ ml.size + mr.size < delta * ml.size + delta * ml.size

Tactic:
refine add_lt_add_of_lt_of_le ?_ mm₂

Premises used: add_lt_add_of_lt_of_le