awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
have hb₂ : rr.size ≤ delta * rl.size
Tactic: rcases hr.3.1.resolve_left (hlp l0) with ⟨_, hb₂⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
have pos : l.size ≤ delta * rl.size
Tactic: refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
pos : l.size ≤ delta * rl.size
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
have pos₁ : rl.size ≤ delta * l.size
Tactic: refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
pos : l.size ≤ delta * rl.size
pos₁ : rl.size ≤ delta * l.size
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
have pos₂ : l.size + rl.size + 1 ≤ delta * rr.size
Tactic: refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
pos : l.size ≤ delta * rl.size
pos₁ : rl.size ≤ delta * l.size
pos₂ : l.size + rl.size + 1 ≤ delta * rr.size
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
have pos₃ : rr.size ≤ delta * (l.size + rl.size + 1)
Tactic: refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
have neg : ∀ (rl0 : rl.size = 0), Valid' o₁ (l.node4L x rl rx rr) o₂
Tactic: rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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₂
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
have neg₁ : ∀ (rl0 : rl.size > 0), Valid' o₁ (l.node4L x rl rx rr) o₂
Tactic: rcases Nat.eq_zero_or_pos (size rl) with rl0 | rl0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₂
have h₁ : ratio = 0 ∨ rr.size = 0
Tactic: rw [rl0, not_lt, Nat.le_zero, Nat.mul_eq_zero] at h
Cleared hypotheses: h, rl0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
have h₁ : rr.size = 0
Tactic: replace h := h.resolve_left (by decide)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
have H2₁ : delta = 0 ∨ l.size = 0
Tactic: rw [rl0, h, Nat.le_zero, Nat.mul_eq_zero] at H2
Cleared hypotheses: H2, H3, H3_0, H3p, ablem, hlp, rl0, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
have H1₁ : ¬0 + (HAdd.hAdd (α := ℕ) 0 0 + 1) ≤ 1
Tactic: rw [hr.2.size_eq, rl0, h, H2.resolve_left (by decide)] at H1
Cleared hypotheses: H1, H2, H3, H3_0, H3p, ablem, hlp, rl0, h
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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₂
have 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
Tactic: refine hl.node4L hr.left hr.right rl0 ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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
Tactic: rcases Nat.eq_zero_or_pos (size l) with l0 | l0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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
Tactic: rcases Nat.eq_zero_or_pos (size l) with l0 | l0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
have H3₁ : rl.size + rr.size ≤ 2
Tactic: replace H3 := H3_0 l0
Cleared hypotheses: H3
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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
Tactic: rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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
have 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
Tactic: rcases Nat.eq_zero_or_pos (size rr) with rr0 | rr0
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
have this : BalancedSz rl.size rr.size
Tactic: have := hr.3.1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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
⊢ 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
have this₁ : BalancedSz rl.size 0
Tactic: rw [rr0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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₂
have refine : Valid' o₂ (l.rotateR x r).dual o₁
Tactic: refine Valid'.dual_iff.2 ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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).dual o₁
have rw : Valid' o₂ (r.dual.rotateL x l.dual) o₁
Tactic: rw [dual_rotateR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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₁
have refine_1 : ¬r.dual.size + l.dual.size ≤ 1
Tactic: refine hr.dual.rotateL hl.dual ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ Valid' o₂ (r.dual.rotateL x l.dual) o₁
have refine_2 : delta * r.dual.size < l.dual.size
Tactic: refine hr.dual.rotateL hl.dual ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ Valid' o₂ (r.dual.rotateL x l.dual) o₁
have refine_3 : 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
Tactic: refine hr.dual.rotateL hl.dual ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ ¬r.dual.size + l.dual.size ≤ 1
have refine_1 : ¬r.size + l.dual.size ≤ 1
Tactic: rwa [size_dual, size_dual, add_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ ¬r.dual.size + l.dual.size ≤ 1
have refine_1₁ : ¬r.size + l.size ≤ 1
Tactic: rwa [size_dual, size_dual, add_comm]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ delta * r.dual.size < l.dual.size
have refine_2 : delta * r.size < l.dual.size
Tactic: rwa [size_dual, size_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 2 * l.dual.size ≤ 9 * r.dual.size + 5 ∨ l.dual.size ≤ 3
have refine_3 : 2 * l.size ≤ 9 * r.dual.size + 5 ∨ l.size ≤ 3
Tactic: rwa [size_dual, size_dual]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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
⊢ 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₂
have pos : ∀ (h : l.size + r.size ≤ 1), Valid' o₁ (l.node' x r) o₂
Tactic: split_ifs with h h_1 h_2