awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
hl.node4L hr.left hr.right rl0 ?_

Premises used: Ordnode.Valid'.right, Ordnode.Valid'.node4L, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
neg :
  l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
refine hl.node4L hr.left hr.right rl0 ?_

Premises used: Ordnode.Valid'.right, Ordnode.Valid'.node4L, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
neg :
  ∀ (l0 : l.size = 0),
    l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
      0 < l.size ∧
        ratio * rr.size ≤ rl.size ∧
          delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
neg₁ :
  ∀ (l0 : l.size > 0),
    l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
      0 < l.size ∧
        ratio * rr.size ≤ rl.size ∧
          delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
rcases Nat.eq_zero_or_pos (size l) with l0 | l0

Premises used: Ordnode.size, Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
⊢ rl.size + rr.size ≤ 2

Tactic:
replace H3 := H3_0 l0
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
neg :
  ∀ (rr0 : rr.size = 0),
    l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
      0 < l.size ∧
        ratio * rr.size ≤ rl.size ∧
          delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
neg₁ :
  ∀ (rr0 : rr.size > 0),
    l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
      0 < l.size ∧
        ratio * rr.size ≤ rl.size ∧
          delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0

Premises used: Ordnode.size, Nat.eq_zero_or_pos
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size = 0
⊢ BalancedSz rl.size rr.size

Tactic:
have := hr.3.1
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size = 0
this : BalancedSz rl.size rr.size
⊢ BalancedSz rl.size 0

Tactic:
rw [rr0] at this
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size = 0
this : BalancedSz rl.size 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩

Premises used: Ordnode.balancedSz_zero, Eq.rec, zero_le_one, le_antisymm, And.intro, Iff.mp, Or.inl, Eq.symm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size = 0
this : BalancedSz rl.size 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
exact Or.inl ⟨l0, le_antisymm (balancedSz_zero.1 this) rl0, rr0.symm ▸ zero_le_one⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size > 0
rwa rwa₁ rwa₂ rwa₃ : rl.size + rr.size ≤ 2
⊢ rr.size + rl.size ≤ 2

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size > 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
exact Or.inl ⟨l0, le_antisymm (ablem rr0 <| by rwa [add_comm]) rl0, ablem rl0 H3⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size > 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

Premises used: Ordnode.Valid'.bal, Or.resolve_left, not_lt, And.left, And.intro, Iff.mp, Or.inr, Ordnode.Valid'.rotateL_lemma₄
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x : WithBot α) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ¬rl.size < ratio * rr.size
rl0 : rl.size > 0
l0 : l.size > 0
⊢ l.size = 0 ∧ rl.size = 1 ∧ rr.size ≤ 1 ∨
    0 < l.size ∧
      ratio * rr.size ≤ rl.size ∧
        delta * l.size ≤ rl.size + rr.size ∧ 3 * (rl.size + rr.size) ≤ 16 * l.size + 9 ∧ rl.size ≤ delta * rr.size

Tactic:
exact
      Or.inr ⟨l0, not_lt.1 h, H2, Valid'.rotateL_lemma₄ (H3p l0), (hr.3.1.resolve_left (hlp l0)).1⟩

Premises used: Or.inr
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
Valid'.dual_iff.2 ?_

Premises used: Iff.mpr, Ordnode.Valid'.dual_iff
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
refine : Valid' o₂ (l.rotateR x r).dual o₁
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
refine Valid'.dual_iff.2 ?_

Premises used: Iff.mpr, Ordnode.Valid'.dual_iff
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
rw : Valid' o₂ (r.dual.rotateL x l.dual) o₁
⊢ Valid' o₂ (l.rotateR x r).dual o₁

Tactic:
rw [dual_rotateR]

Premises used: Ordnode.dual_rotateR
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₂ (r.dual.rotateL x l.dual) o₁

Tactic:
hr.dual.rotateL hl.dual ?_ ?_ ?_

Premises used: Ordnode.Valid'.rotateL, Ordnode.Valid'.dual
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
refine_1 : ¬r.dual.size + l.dual.size ≤ 1
refine_2 : delta * r.dual.size < l.dual.size
refine_3 : 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
⊢ Valid' o₂ (r.dual.rotateL x l.dual) o₁

Tactic:
refine hr.dual.rotateL hl.dual ?_ ?_ ?_

Premises used: Ordnode.Valid'.rotateL, Ordnode.Valid'.dual
-- 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₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
refine_1 : ¬r.size + l.dual.size ≤ 1
refine_1₁ : ¬r.size + l.size ≤ 1
refine_1₂ refine_1₃ refine_1₄ refine_1₅ : ¬l.size + r.size ≤ 1
⊢ ¬r.dual.size + l.dual.size ≤ 1

Tactic:
rwa [size_dual, 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 α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
refine_2 : delta * r.size < l.dual.size
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : delta * r.size < l.size
⊢ delta * r.dual.size < l.dual.size

Tactic:
rwa [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 α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
refine_3 : 2 * l.size ≤ 9 * r.dual.size + 5 ∨ l.size ≤ 3
refine_3₁ refine_3₂ refine_3₃ refine_3₄ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3

Tactic:
rwa [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 α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
pos : ∀ (h : l.size + r.size ≤ 1), Valid' o₁ (l.node' x r) o₂
pos₁ : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : r.size > delta * l.size), Valid' o₁ (l.rotateL x r) o₂
pos₂ :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬r.size > delta * l.size) (h_2 : l.size > delta * r.size),
    Valid' o₁ (l.rotateR x r) o₂
neg :
  ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : ¬r.size > delta * l.size) (h_2 : ¬l.size > delta * r.size),
    Valid' o₁ (l.node' x r) o₂
⊢ Valid' o₁
    (if l.size + r.size ≤ 1 then l.node' x r
    else
      if r.size > delta * l.size then l.rotateL x r else if l.size > delta * r.size then l.rotateR x r else l.node' x r)
    o₂

Tactic:
split_ifs with h h_1 h_2
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : l.size + r.size ≤ 1
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
hl.node' hr (Or.inl h)

Premises used: Ordnode.Valid'.node', Or.inl
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : l.size + r.size ≤ 1
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
exact hl.node' hr (Or.inl h)

Premises used: Ordnode.Valid'.node', Or.inl
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ Valid' o₁ (l.rotateL x r) o₂

Tactic:
hl.rotateL hr h h_1 H₁

Premises used: Ordnode.Valid'.rotateL
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : r.size > delta * l.size
⊢ Valid' o₁ (l.rotateL x r) o₂

Tactic:
exact hl.rotateL hr h h_1 H₁

Premises used: Ordnode.Valid'.rotateL
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
hl.rotateR hr h h_2 H₂

Premises used: Ordnode.Valid'.rotateR
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : l.size > delta * r.size
⊢ Valid' o₁ (l.rotateR x r) o₂

Tactic:
exact hl.rotateR hr h h_2 H₂

Premises used: Ordnode.Valid'.rotateR
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
hl.node' hr (Or.inr ⟨not_lt.1 h_2, not_lt.1 h_1⟩)

Premises used: not_lt, And.intro, Iff.mp, Ordnode.Valid'.node', Or.inr
-- 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₁ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
H₂ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
h : ¬l.size + r.size ≤ 1
h_1 : ¬r.size > delta * l.size
h_2 : ¬l.size > delta * r.size
⊢ Valid' o₁ (l.node' x r) o₂

Tactic:
exact hl.node' hr (Or.inr ⟨not_lt.1 h_2, not_lt.1 h_1⟩)

Premises used: not_lt, And.intro, Iff.mp, Ordnode.Valid'.node', Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
this : r.size ≤ 3 * (l.size + 1)
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
suffices : r.size ≤ 3 * (l.size + 1)
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
suffices @size α r ≤ 3 * (size l + 1) by lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
inl : ∀ (hl : l.size.dist l' ≤ 1) (H1 : BalancedSz l' r.size), r.size ≤ 3 * (l.size + 1)
inr : ∀ (hr : r.size.dist r' ≤ 1) (H1 : BalancedSz l.size r'), r.size ≤ 3 * (l.size + 1)
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
H1 : BalancedSz l' r.size
inl : ∀ (h : l' + r.size ≤ 1), r.size ≤ 3 * (l.size + 1)
inl₁ : l' ≤ delta * r.size → ∀ (h₂ : r.size ≤ delta * l'), r.size ≤ 3 * (l.size + 1)
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rcases H1 with (h | ⟨_, h₂⟩)
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
H1 : BalancedSz l.size r'
inr : ∀ (h : l.size + r' ≤ 1), r.size ≤ 3 * (l.size + 1)
inr₁ : l.size ≤ delta * r' → ∀ (h₂ : r' ≤ delta * l.size), r.size ≤ 3 * (l.size + 1)
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rcases H1 with (h | ⟨_, h₂⟩)
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))

Premises used: Nat.le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))

Premises used: Nat.le_add_left, le_trans