awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ Bounded nil o₁ (↑(rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1 : WithTop α)

Tactic:
@findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil

Premises used: WithTop.some, And.right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil, Ordnode.All.imp, Ordnode.findMin'_all
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
refine_1 : ∀ (a : α), lx < a → Bounded nil o₁ (↑a : WithBot α)
⊢ Bounded nil o₁ (↑(rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1 : WithTop α)

Tactic:
refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil

Premises used: And.right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil, Ordnode.All.imp, Ordnode.findMin'_all
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ∀ (a : α), lx < a → Bounded nil o₁ (↑a : WithBot α)

Tactic:
fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)

Premises used: WithBot.some, le_of_lt, Ordnode.Bounded.mono_right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ ∀ (a : α), lx < a → Bounded nil o₁ (↑a : WithBot α)

Tactic:
exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)

Premises used: le_of_lt, Ordnode.Bounded.mono_right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ All (fun (x : α) ↦ x < (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1)
    (Ordnode.node ls ll lx lr)

Tactic:
@findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)

Premises used: Iff.mpr, Iff.mp, Ordnode.All.imp, Ordnode.findMin'_all, Ordnode.all_iff_forall
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ All (fun (x : α) ↦ x < (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1)
    (Ordnode.node ls ll lx lr)

Tactic:
exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)

Premises used: Iff.mpr, Iff.mp, Ordnode.All.imp, Ordnode.findMin'_all, Ordnode.all_iff_forall
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
refine_3 : (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).size = ls + (rl.size + rr.size + 1)
⊢ ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
    ls + rs

Tactic:
rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]

Premises used: Ordnode.Valid'.bal, add_assoc, Ordnode.size_balanceL, Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
H :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ (Ordnode.node ls ll lx lr).size + (rl.node' rx rr).size = ls + (rl.size + rr.size + 1)

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
neg :
  (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'
⊢ Valid' o₁
      ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
        (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2)
      o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1
          (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2).size =
      ls + rs

Tactic:
suffices H : _ by
        refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩
        · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α))
            _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil
          exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h)
        · exact
            @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx
              (all_iff_forall.2 fun x hx => sep.imp fun y hy => all_iff_forall.1 hy.1 _ hx)
              (sep.imp fun y hy => hy.2.1)
        · rw [size_balanceL hl.3 v.3 hl.2 v.2 H, add_assoc, ← e, hr.2.1]; rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
⊢ (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'

Tactic:
Or.inr ⟨_, Or.inr e, ?_⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
neg : BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
⊢ (∃ (l' : ℕ),
      Raised l' (Ordnode.node ls ll lx lr).size ∧
        BalancedSz l' (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size) ∨
    ∃ (r' : ℕ),
      Raised (rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).2.size r' ∧
        BalancedSz (Ordnode.node ls ll lx lr).size r'

Tactic:
refine Or.inr ⟨_, Or.inr e, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h : ¬ls > rs
v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1
neg neg₁ neg₂ neg₃ :
  ∀ (bal : BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size),
    ¬ls > rs →
      ∀ (v : Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂)
        (e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1),
        BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size
⊢ BalancedSz (Ordnode.node ls ll lx lr).size (rl.node' rx rr).size

Tactic:
rwa [hr.2.eq_node'] at bal

Premises used: Ordnode.Valid'.sz, Ordnode.Sized.eq_node'
-- 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₂
⊢ BalancedSz l.size r.size → Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

Tactic:
Valid'.glue_aux (hl.trans_right hr.1) (hr.trans_left hl.1) (hl.1.to_sep hr.1)

Premises used: Ordnode.Bounded.to_sep, Ordnode.Valid'.glue_aux, Ordnode.Valid'.trans_left, Ordnode.Valid'.ord, Ordnode.Valid'.trans_right
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
a b c : ℕ
h₁ : 3 * a < b + c + 1
h₂ : b ≤ 3 * c
⊢ 2 * (a + b) ≤ 9 * c + 5

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ls + rl.size
⊢ t.size = ll.size + lr.size + 1 + rl.size

Tactic:
rw [hl.2.1] at e

Premises used: Ordnode.Valid'.sz, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1

Tactic:
rw [hl.2.1, hr.2.1, delta] at h

Premises used: Ordnode.Valid'.sz, Ordnode.delta, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
h₁ : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
⊢ Valid' o₁ t (↑rx : WithTop α)

Tactic:
rw [hl.2.1, hr.2.1, delta] at h

Premises used: Ordnode.Valid'.sz, Ordnode.delta, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
h₁ : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v₁ : Valid' o₁ t (↑rx : WithTop α)
⊢ t.size = ll.size + lr.size + 1 + rl.size

Tactic:
rw [hl.2.1, hr.2.1, delta] at h

Premises used: Ordnode.Valid'.sz, Ordnode.delta, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
inl : ∀ (H : rl.size + rr.size ≤ 1), Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
inr :
  ∀ (hr₁ : rl.size ≤ delta * rr.size) (hr₂ : rr.size ≤ delta * rl.size),
    Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩)

Premises used: Ordnode.Valid'.bal, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
H : rl.size + rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩

Premises used: Ordnode.Valid'.right, Ordnode.Valid'.balanceL_aux, And.intro
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
refine_1 : 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3
refine_2 : (t.balanceL rx rr).size = ls + rs
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
refine_1 : 2 * (ll.size + lr.size + 1 + rl.size) ≤ 9 * rr.size + 5 ∨ ll.size + lr.size + 1 + rl.size ≤ 3
⊢ 2 * t.size ≤ 9 * rr.size + 5 ∨ t.size ≤ 3

Tactic:
rw [e]
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * (ll.size + lr.size + 1 + rl.size) ≤ 9 * rr.size + 5 ∨ ll.size + lr.size + 1 + rl.size ≤ 3

Tactic:
Or.inl (Valid'.merge_lemma h hr₁)

Premises used: Ordnode.Valid'.merge_lemma, Or.inl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t (↑rx : WithTop α)
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ 2 * (ll.size + lr.size + 1 + rl.size) ≤ 9 * rr.size + 5 ∨ ll.size + lr.size + 1 + rl.size ≤ 3

Tactic:
exact Or.inl (Valid'.merge_lemma h hr₁)

Premises used: Ordnode.Valid'.merge_lemma, Or.inl