awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
le_trans h₂
        (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))

Premises used: Nat.mul_le_mul_left, Nat.dist_tri_right, Nat.add_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
left : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
      le_trans h₂
        (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))

Premises used: Nat.mul_le_mul_left, Nat.dist_tri_right, Nat.add_le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ HAdd.hAdd (α := ℕ) 1 1 ≤ 3 * (l.size + 1)

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
      le_trans (Nat.dist_tri_left' _ _)
        (le_trans (add_le_add hr (le_trans (Nat.le_add_left _ _) h)) (by lia))

Premises used: Nat.dist_tri_left', add_le_add, Nat.le_add_left, le_trans
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ LE.le (α := ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * l.size + 3

Tactic:
exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))

Premises used: add_le_add, Nat.dist_tri_right', le_trans
-- 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 : ∃ (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₂

Tactic:
let ⟨_, _, H1, H2⟩ := H
  Valid'.balance'_aux hl hr (Valid'.balance'_lemma H1 H2) (Valid'.balance'_lemma H1.symm H2.symm)

Premises used: Ordnode.BalancedSz.symm, _private.0.Ordnode.Valid'.balance'.match_1, Ordnode.Valid', Or.symm, Ordnode.balance', Ordnode.Valid'.balance'_aux, Ordnode.Valid'.balance'_lemma
-- 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 : ∃ (l' : ℕ), ∃ (r' : ℕ), BalancedSz l' r' ∧ (l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l')
rw : Valid' o₁ (l.balance' x r) o₂
⊢ Valid' o₁ (l.balance x r) o₂

Tactic:
rw [balance_eq_balance' hl.3 hr.3 hl.2 hr.2]

Premises used: Ordnode.Valid'.bal, Ordnode.balance_eq_balance', Ordnode.Valid'.sz
-- 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 : ∃ (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₂

Tactic:
hl.balance' hr H

Premises used: Ordnode.Valid'.balance'
-- 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 : ∃ (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₂

Tactic:
exact hl.balance' hr H

Premises used: Ordnode.Valid'.balance'
-- 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₁ : 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
rw : Valid' o₁ (l.balance' x r) o₂
⊢ Valid' o₁ (l.balanceL 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]

Premises used: Ordnode.Valid'.bal, Ordnode.balance_eq_balance', Ordnode.Valid'.sz, Ordnode.balanceL_eq_balance
-- 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₁ : 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₂

Tactic:
hl.balance'_aux hr (Or.inl ?_) H₃

Premises used: Ordnode.Valid'.balance'_aux, 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₁ : 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
refine : 2 * r.size ≤ 9 * l.size + 5
⊢ Valid' o₁ (l.balance' x r) o₂

Tactic:
refine hl.balance'_aux hr (Or.inl ?_) H₃

Premises used: Ordnode.Valid'.balance'_aux, 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₁ : 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
inr : ∀ (r0 : r.size > 0), 2 * r.size ≤ 9 * l.size + 5
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
rcases Nat.eq_zero_or_pos (size r) with r0 | r0

Premises used: Ordnode.size, Nat.eq_zero_or_pos
-- 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₁ : 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
inl : HMul.hMul (α := ℕ) 2 0 ≤ 9 * l.size + 5
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
rw [r0]
-- 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₁ : 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
⊢ HMul.hMul (α := ℕ) 2 0 ≤ 9 * l.size + 5

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- 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₁ : 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
⊢ HMul.hMul (α := ℕ) 2 0 ≤ 9 * l.size + 5

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- 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₁ : 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
inr₁ : ∀ (l0 : l.size > 0), 2 * r.size ≤ 9 * l.size + 5
⊢ 2 * r.size ≤ 9 * l.size + 5

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 : α
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
inr : 2 * r.size ≤ HMul.hMul (α := ℕ) 9 0 + 5
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
rw [l0]
-- 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₁ : 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
⊢ HMul.hMul (α := ℕ) 2 1 ≤ HMul.hMul (α := ℕ) 9 0 + 5

Tactic:
decide
-- 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₁ : 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 ≤ HMul.hMul (α := ℕ) 9 0 + 5

Tactic:
exact le_trans (Nat.mul_le_mul_left _ (H₁ l0)) (by decide)

Premises used: Nat.mul_le_mul_left, le_trans
-- 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₁ : 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
⊢ r.size ≤ 3 * l.size

Tactic:
replace H₂ : _ ≤ 3 * _ := H₂ l0 r0
-- 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₁ : l.size = 0 → r.size ≤ 1
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size > 0
H₂ : r.size ≤ 3 * l.size
⊢ 2 * r.size ≤ 9 * l.size + 5

Tactic:
lia
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
rw : Valid' o₁ (l.balance' x r) o₂
⊢ Valid' o₁ (l.balanceL x r) o₂

Tactic:
rw [balanceL_eq_balance' hl.3 hr.3 hl.2 hr.2 H]

Premises used: Ordnode.Valid'.bal, Ordnode.balanceL_eq_balance', Ordnode.Valid'.sz
-- 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 : (∃ (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₂

Tactic:
hl.balance' hr ?_

Premises used: Ordnode.Valid'.balance'
-- 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 : (∃ (l' : ℕ), Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r.size r' ∧ BalancedSz l.size r'
refine :
  ∃ (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₂

Tactic:
refine hl.balance' hr ?_

Premises used: Ordnode.Valid'.balance'
-- 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 : (∃ (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')
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')
⊢ ∃ (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⟩)
-- 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₂
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:
⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩

Premises used: Ordnode.Raised.dist_le', And.intro, Exists.intro, Or.inl, rfl
-- 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₂
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:
exact ⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩
-- 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₂
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:
⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩

Premises used: Ordnode.Raised.dist_le, And.intro, Exists.intro, Or.inr, rfl
-- 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₂
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:
exact ⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩
-- 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₁ : 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
rw : Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]

Premises used: Ordnode.dual_balanceR, 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₂
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
⊢ ∀ (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
-- 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₁ : 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₁
⊢ ∀ (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

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₁ : 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.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₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
this H₁ H₂ H₃
-- 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₁ : 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.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₁
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
exact this H₁ H₂ H₃
-- 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 : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
rw : Valid' o₂ (r.dual.balanceL x l.dual) o₁
⊢ Valid' o₁ (l.balanceR x r) o₂

Tactic:
rw [Valid'.dual_iff, dual_balanceR]

Premises used: Ordnode.dual_balanceR, 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₂
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
hr.dual.balanceL hl.dual (balance_sz_dual H)

Premises used: Ordnode.balance_sz_dual, Ordnode.Valid'.balanceL, 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₂
H : (∃ (l' : ℕ), Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ (r' : ℕ), Raised r' r.size ∧ BalancedSz l.size r'
⊢ Valid' o₂ (r.dual.balanceL x l.dual) o₁

Tactic:
exact hr.dual.balanceL hl.dual (balance_sz_dual H)

Premises used: Ordnode.balance_sz_dual, Ordnode.Valid'.balanceL, Ordnode.Valid'.dual
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
⊢ Ordnode.node s l x r = l.node' x r

Tactic:
have := H.2.eq_node'
-- Module: Mathlib.Data.Ordmap.Ordset
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) o₂

Tactic:
rw [this] at H
-- Module: Mathlib.Data.Ordmap.Ordset
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
H₁ : Valid' o₁ (l.node' x r) o₂
⊢ Ordnode.node s l x r = l.node' x r

Tactic:
rw [this] at H
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x nil) o₂
⊢ Valid' o₁ (l.node' x nil).eraseMax (↑(findMax' x nil) : WithTop α) ∧
    (l.node' x nil).size = (l.node' x nil).eraseMax.size + 1

Tactic:
⟨H.left, rfl⟩

Premises used: And.intro, rfl, Ordnode.Valid'.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
o₂ : WithTop α
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x nil) o₂
⊢ Valid' o₁ (l.node' x nil).eraseMax (↑(findMax' x nil) : WithTop α) ∧
    (l.node' x nil).size = (l.node' x nil).eraseMax.size + 1

Tactic:
exact ⟨H.left, rfl⟩
-- Module: Mathlib.Data.Ordmap.Ordset
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₂
⊢ Ordnode.node rs rl rx rr = rl.node' rx rr

Tactic:
have := H.2.2.2.eq_node'
-- Module: Mathlib.Data.Ordmap.Ordset
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
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
⊢ 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

Tactic:
rw [this] at H ⊢
-- Module: Mathlib.Data.Ordmap.Ordset
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' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)

Tactic:
rcases IHrr H.right with ⟨h, e⟩

Premises used: Ordnode.Valid'.right