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_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
rr0 : rr.size > 0
l0 : l.size > 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
left : rl.size ≤ delta * rr.size
hb₂ : rr.size ≤ delta * rl.size
⊢ rr.size ≤ delta * (l.size + rl.size + 1)

Tactic:
exact
        le_trans hb₂
          (Nat.mul_le_mul_left _ <| le_trans (Nat.le_add_left _ _) (Nat.le_add_right _ _))

Premises used: Nat.le_add_right, Nat.le_add_left, Nat.mul_le_mul_left, le_trans
-- 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
neg : ∀ (rl0 : rl.size = 0), Valid' o₁ (l.node4L x rl rx rr) o₂
neg₁ : ∀ (rl0 : rl.size > 0), Valid' o₁ (l.node4L x rl rx rr) o₂
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0

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
⊢ ratio = 0 ∨ rr.size = 0

Tactic:
rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h

Premises used: Nat.le_zero, not_lt, Nat.mul_eq_zero
-- 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
h₁ : ratio = 0 ∨ rr.size = 0
⊢ rl.size = 0

Tactic:
rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h

Premises used: Nat.le_zero, not_lt, Nat.mul_eq_zero
-- 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 : ratio = 0 ∨ rr.size = 0
rl0 : rl.size = 0
⊢ ¬ratio = 0

Tactic:
decide
-- 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 : ratio = 0 ∨ rr.size = 0
rl0 : rl.size = 0
⊢ rr.size = 0

Tactic:
replace h := h.resolve_left (by decide)
-- 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
rl0 : rl.size = 0
h : rr.size = 0
⊢ delta = 0 ∨ l.size = 0

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
⊢ 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
H3₁ : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
⊢ ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ l.size > 0 → ¬rl.size + rr.size ≤ 1

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ rl.size = 0

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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
rl0 : rl.size = 0
h : rr.size = 0
H2₁ : delta = 0 ∨ l.size = 0
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
rl0₁ : rl.size = 0
⊢ rr.size = 0

Tactic:
rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2

Premises used: Nat.le_zero, Nat.mul_eq_zero
-- 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 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2 : delta = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
⊢ ¬delta = 0

Tactic:
decide
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
⊢ ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
⊢ delta = 0 ∨ l.size = 0

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
⊢ 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
H3₁ : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
⊢ ∀ (l0 : l.size = 0), rl.size + rr.size ≤ 2

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ l.size > 0 → ¬rl.size + rr.size ≤ 1

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
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
⊢ rl.size = 0

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2₁ : delta = 0 ∨ l.size = 0
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
rl0₁ : rl.size = 0
⊢ rr.size = 0

Tactic:
rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1

Premises used: Ordnode.Valid'.sz, Or.resolve_left, Ordnode.Sized.size_eq
-- 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 : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2 : delta = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
⊢ 0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1

Tactic:
decide
-- 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 : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
H2 : delta = 0 ∨ l.size = 0
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
rl0 : rl.size = 0
h : rr.size = 0
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
cases H1 (by decide)