awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
pos : ∀ (h : l.size + r.size ≤ 1), 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₂
have pos₁ : ∀ (h : ¬l.size + r.size ≤ 1) (h_1 : r.size > delta * l.size), Valid' o₁ (l.rotateL x r) o₂
Tactic: split_ifs with h h_1 h_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₂
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₂
⊢ 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) (h_1 : ¬r.size > delta * l.size) (h_2 : l.size > delta * r.size),
  Valid' o₁ (l.rotateR x r) o₂
Tactic: split_ifs with h h_1 h_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₂
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₂
⊢ 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 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₂
Tactic: split_ifs with h h_1 h_2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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'
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
have suffices : r.size ≤ 3 * (l.size + 1)
Tactic: suffices @size α r ≤ 3 * (size l + 1) by lia
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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'
⊢ r.size ≤ 3 * (l.size + 1)
have inl : ∀ (hl : l.size.dist l' ≤ 1) (H1 : BalancedSz l' r.size), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩)
Cleared hypotheses: r', H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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)
⊢ r.size ≤ 3 * (l.size + 1)
have inr : ∀ (hr : r.size.dist r' ≤ 1) (H1 : BalancedSz l.size r'), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩)
Cleared hypotheses: l', H1, H2
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
H1 : BalancedSz l' r.size
⊢ r.size ≤ 3 * (l.size + 1)
have inl : ∀ (h : l' + r.size ≤ 1), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H1 with (h | ⟨_, h₂⟩)
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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)
⊢ r.size ≤ 3 * (l.size + 1)
have inl₁ : l' ≤ delta * r.size → ∀ (h₂ : r.size ≤ delta * l'), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H1 with (h | ⟨_, h₂⟩)
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
H1 : BalancedSz l.size r'
⊢ r.size ≤ 3 * (l.size + 1)
have inr : ∀ (h : l.size + r' ≤ 1), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H1 with (h | ⟨_, h₂⟩)
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
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)
⊢ r.size ≤ 3 * (l.size + 1)
have inr₁ : l.size ≤ delta * r' → ∀ (h₂ : r' ≤ delta * l.size), r.size ≤ 3 * (l.size + 1)
Tactic: rcases H1 with (h | ⟨_, h₂⟩)
Cleared hypotheses: H1
-- 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 : ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ Valid' o₁ (l.balance x r) o₂
have rw : Valid' o₁ (l.balance' x r) o₂
Tactic: rw [balance_eq_balance' hl.3 hr.3 hl.2 hr.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₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balanceL x r) o₂
have rw : Valid' o₁ (l.balance' x r) o₂
Tactic: rw [balanceL_eq_balance hl.2 hr.2 H₁ H₂, balance_eq_balance' hl.3 hr.3 hl.2 hr.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₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ Valid' o₁ (l.balance' x r) o₂
have refine : 2 * r.size ≤ 9 * l.size + 5
Tactic: refine hl.balance'_aux hr (Or.inl ?_) H₃
-- 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₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ 2 * r.size ≤ 9 * l.size + 5
have inl : ∀ (r0 : r.size = 0), 2 * r.size ≤ 9 * l.size + 5
Tactic: rcases Nat.eq_zero_or_pos (size r) with r0 | r0
-- 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₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
inl : ∀ (r0 : r.size = 0), 2 * r.size ≤ 9 * l.size + 5
⊢ 2 * r.size ≤ 9 * l.size + 5
have inr : ∀ (r0 : r.size > 0), 2 * r.size ≤ 9 * l.size + 5
Tactic: rcases Nat.eq_zero_or_pos (size r) with r0 | r0
-- 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₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5
have inl : HMul.hMul (α := ℕ) 2 0 ≤ 9 * l.size + 5
Tactic: rw [r0]
-- 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₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5
have inr : ∀ (l0 : l.size = 0), 2 * r.size ≤ 9 * l.size + 5
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 : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
inr : ∀ (l0 : l.size = 0), 2 * r.size ≤ 9 * l.size + 5
⊢ 2 * r.size ≤ 9 * l.size + 5
have inr₁ : ∀ (l0 : l.size > 0), 2 * r.size ≤ 9 * l.size + 5
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 : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l (↑x : WithTop α)
hr : Valid' (↑x : WithBot α) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size = 0
⊢ 2 * r.size ≤ 9 * l.size + 5
have inr : 2 * r.size ≤ HMul.hMul (α := ℕ) 9 0 + 5
Tactic: rw [l0]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
⊢ 2 * r.size ≤ 9 * l.size + 5
have H₄ : r.size ≤ 3 * l.size
Tactic: replace H₂ : _ ≤ 3 * _ := H₂ l0 r0
Cleared hypotheses: H₂
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceL x r) o₂
have rw : Valid' o₁ (l.balance' x r) o₂
Tactic: rw [balanceL_eq_balance' hl.3 hr.3 hl.2 hr.2 H]
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balance' x r) o₂
have refine : ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
Tactic: refine hl.balance' hr ?_
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
⊢ ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
have inl : ∀ (l' : ℕ) (e : Raised l' l.size) (H : BalancedSz l' r.size),
  ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
Tactic: rcases H with (⟨l', e, H⟩ | ⟨r', e, H⟩)
Cleared hypotheses: H
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
inl :
  ∀ (l' : ℕ) (e : Raised l' l.size) (H : BalancedSz l' r.size),
    ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
⊢ ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
have inr : ∀ (r' : ℕ) (e : Raised r.size r') (H : BalancedSz l.size r'),
  ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
Tactic: rcases H with (⟨l', e, H⟩ | ⟨r', e, H⟩)
Cleared hypotheses: H
-- 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₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₁ (l.balanceR x r) o₂
have rw : Valid' o₂ (r.dual.balanceL x l.dual) o₁
Tactic: rw [Valid'.dual_iff, dual_balanceR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
have this : ∀ (H₁ : r.dual.size = 0 → l.dual.size ≤ 1) (H₂ : 1 ≤ r.dual.size → 1 ≤ l.dual.size → l.dual.size ≤ delta * r.dual.size)
  (H₃ : 2 * r.dual.size ≤ 9 * l.dual.size + 5 ∨ r.dual.size ≤ 3), Valid' o₂ (r.dual.balanceL x l.dual) o₁
Tactic: have := hr.dual.balanceL_aux hl.dual
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
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₁ : r.size = 0 → l.size ≤ 1
H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size
H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3
this :
  ∀ (H₁ : r.dual.size = 0 → l.dual.size ≤ 1)
    (H₂ : 1 ≤ r.dual.size → 1 ≤ l.dual.size → l.dual.size ≤ delta * r.dual.size)
    (H₃ : 2 * r.dual.size ≤ 9 * l.dual.size + 5 ∨ r.dual.size ≤ 3), Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁
have this₁ : ∀ (H₁ : r.size = 0 → l.size ≤ 1) (H₂ : 1 ≤ r.size → 1 ≤ l.size → l.size ≤ delta * r.size)
  (H₃ : 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3), Valid' o₂ (r.dual.balanceL x l.dual) o₁
Tactic: rw [size_dual, size_dual] 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₂
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₁ (l.balanceR x r) o₂
have rw : Valid' o₂ (r.dual.balanceL x l.dual) o₁
Tactic: rw [Valid'.dual_iff, dual_balanceR]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' o₁ (l.node' x r).eraseMax (↑(findMax' x r) : WithTop α) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
have this : Ordnode.node s l x r = l.node' x r
Tactic: have := H.2.eq_node'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this : Ordnode.node s l x r = l.node' x r
⊢ Valid' o₁ (l.node' x r).eraseMax (↑(findMax' x r) : WithTop α) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1
have H₁ : Valid' o₁ (l.node' x r) o₂
Tactic: rw [this] at H
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax (↑(findMax' x (Ordnode.node rs rl rx rr)) : WithTop α) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1
have this : Ordnode.node rs rl rx rr = rl.node' rx rr
Tactic: have := H.2.2.2.eq_node'
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
⊢ Valid' o₁ (l.node' x (Ordnode.node rs rl rx rr)).eraseMax (↑(findMax' x (Ordnode.node rs rl rx rr)) : WithTop α) ∧
    (l.node' x (Ordnode.node rs rl rx rr)).size = (l.node' x (Ordnode.node rs rl rx rr)).eraseMax.size + 1
have node : ∀ (H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂) (this : Ordnode.node rs rl rx rr = rl.node' rx rr),
  Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax (↑(findMax' x (rl.node' rx rr)) : WithTop α) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
Tactic: rw [this] at H ⊢
Cleared hypotheses: H, this
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
⊢ Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax (↑(findMax' x (rl.node' rx rr)) : WithTop α) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
have h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
Tactic: rcases IHrr H.right with ⟨h, e⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
⊢ Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax (↑(findMax' x (rl.node' rx rr)) : WithTop α) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
have e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
Tactic: rcases IHrr H.right with ⟨h, e⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax (↑(findMax' x (rl.node' rx rr)) : WithTop α) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
have node : (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
Tactic: refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
have node : (l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
Tactic: rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
-- Lean 4 proof step from Mathlib.Data.Ordmap.Ordset (goal)
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rl) o₂),
    Valid' o₁ (l.node' x rl).eraseMax (↑(findMax' x rl) : WithTop α) ∧
      (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x rr) o₂),
    Valid' o₁ (l.node' x rr).eraseMax (↑(findMax' x rr) : WithTop α) ∧
      (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
have node : l.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
Tactic: rw [size_node, e]