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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
refine_1 : Bounded nil (↑((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 : WithBot α) o₂
refine_2 :
  All (fun (x : α) ↦ x > ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2)
    (Ordnode.node rs rl rx rr)
refine_3 :
  (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
    ls + rs
⊢ Valid' o₁
      (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2
          (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
-- 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ Bounded nil (↑((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 : WithBot α) o₂

Tactic:
findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)

Premises used: WithBot.some, Ordnode.findMax'_all, And.right, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil, Ordnode.All.imp
-- 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
refine_1 : ∀ (a : α), All (fun (y : α) ↦ a < y) (Ordnode.node rs rl rx rr) → Bounded nil (↑a : WithTop α) o₂
⊢ Bounded nil (↑((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 : WithBot α) o₂

Tactic:
refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)

Premises used: Ordnode.findMax'_all, And.right, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil, Ordnode.All.imp
-- 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ ∀ (a : α), All (fun (y : α) ↦ a < y) (Ordnode.node rs rl rx rr) → Bounded nil (↑a : WithTop α) o₂

Tactic:
fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)

Premises used: le_of_lt, WithTop.some, And.right, And.left, Ordnode.Bounded.mono_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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ ∀ (a : α), All (fun (y : α) ↦ a < y) (Ordnode.node rs rl rx rr) → Bounded nil (↑a : WithTop α) o₂

Tactic:
exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)

Premises used: le_of_lt, And.right, Ordnode.Bounded.mono_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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ All (fun (x : α) ↦ x > ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2)
    (Ordnode.node rs rl rx rr)

Tactic:
@findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2

Premises used: Ordnode.findMax'_all, And.right, 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ All (fun (x : α) ↦ x > ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2)
    (Ordnode.node rs rl rx rr)

Tactic:
exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2

Premises used: Ordnode.findMax'_all, And.right, 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
refine_3 : (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ll.size + lr.size + 1 + rs
⊢ (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
    ls + rs

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

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, add_right_comm, Ordnode.size_balanceR, 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ (ll.node' lx lr).size + (Ordnode.node rs rl rx rr).size = ll.size + lr.size + 1 + rs

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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
pos :
  (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ Valid' o₁
      (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2
          (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
suffices H : _ by
        refine ⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩
        · refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)
          exact fun x h => hr.1.2.to_nil.mono_left (le_of_lt h.2.1)
        · exact @findMax'_all _ (fun a => All (· > a) (.node rs rl rx rr)) lx lr sep.2.1 sep.2.2
        · rw [size_balanceR v.3 hr.3 v.2 hr.2 H, add_right_comm, ← e, hl.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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
⊢ (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'

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

Premises used: And.intro, Exists.intro, Or.inl, 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
pos : BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size
⊢ (∃ (l' : ℕ),
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ (r' : ℕ),
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'

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

Premises used: Or.inl
-- 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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
pos pos₁ pos₂ pos₃ :
  ∀ (bal : BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size),
    ls > rs →
      ∀ (v : Valid' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α))
        (e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1),
        BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size
⊢ BalancedSz (ll.node' lx lr).size (Ordnode.node rs rl rx rr).size

Tactic:
rwa [hl.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 α
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
neg :
  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
neg₁ : ℕ
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2) o₂ ∧
    ((Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size = ls + rs

Tactic:
rw [splitMin_eq]

Premises used: Ordnode.splitMin_eq
-- 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
⊢ Valid' (↑(rl.findMin' rx) : WithBot α) (rl.node' rx rr).eraseMin o₂

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr

Premises used: Ordnode.Valid'.eraseMin_aux
-- 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₂
⊢ (rl.node' rx rr).size = (rl.node' rx rr).eraseMin.size + 1

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMin_aux hr

Premises used: Ordnode.Valid'.eraseMin_aux
-- 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'
⊢ 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:
⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩

Premises used: Ordnode.Valid'.balanceL, And.intro, Ordnode.Valid'.of_lt
-- 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 : Bounded nil o₁ (↑(rl.findMin' rx, (Ordnode.node (rl.size + rr.size + 1) rl rx rr).eraseMin).1 : WithTop α)
refine_2 :
  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)
refine_3 :
  ((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
⊢ 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:
refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩