awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Valid' (↑x : WithBot α) (rl.node' rx rr).eraseMax (↑(findMax' rx rr) : WithTop α)
⊢ (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1

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

Premises used: Ordnode.Valid'.right
-- 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
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

Tactic:
⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩

Premises used: Ordnode.Valid'.balanceL, Ordnode.Valid'.bal, And.left, And.intro, Exists.intro, Or.inr, Ordnode.Valid'.left
-- 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
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
node : (l.node' x (rl.node' rx rr)).size = (l.node' x (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

Tactic:
refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
-- 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
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
node : (l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 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⟩)]

Premises used: Ordnode.Valid'.bal, Ordnode.size_balanceL, Ordnode.Valid'.sz, Ordnode.eraseMax, And.right, And.left, And.intro, Exists.intro, Or.inr
-- 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
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
node : l.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1
⊢ (l.node' x (rl.node' rx rr)).size = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1

Tactic:
rw [size_node, e]

Premises used: Ordnode.size_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 (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.size + ((rl.node' rx rr).eraseMax.size + 1) + 1 = l.size + (rl.node' rx rr).eraseMax.size + 1 + 1

Tactic:
rfl
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (l.node' x r) o₂
nil :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α} (H : Valid' o₁ (l.node' x Ordnode.nil) o₂),
    Valid' o₁ (l.node' x Ordnode.nil).eraseMax (↑(findMax' x Ordnode.nil) : WithTop α) ∧
      (l.node' x Ordnode.nil).size = (l.node' x Ordnode.nil).eraseMax.size + 1
node :
  ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α),
    (∀ {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
⊢ Valid' o₁ (l.node' x r).eraseMax (↑(findMax' x r) : WithTop α) ∧ (l.node' x r).size = (l.node' x r).eraseMax.size + 1

Tactic:
induction r generalizing l x o₁ with
  | nil => exact ⟨H.left, rfl⟩
  | node rs rl rx rr _ IHrr =>
    have := H.2.2.2.eq_node'; rw [this] at H ⊢
    rcases IHrr H.right with ⟨h, e⟩
    refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩
    rw [eraseMax, size_balanceL H.3.2.1 h.3 H.2.2.1 h.2 (Or.inr ⟨_, Or.inr e, H.3.1⟩)]
    rw [size_node, e]; rfl

Premises used: Ordnode.size_node, Ordnode.eraseMax, Ordnode.nil, Ordnode.Valid'.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₂
⊢ Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1

Tactic:
have := H.dual.eraseMax_aux
-- 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 :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
rwa :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).dual.size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₁ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).dual.eraseMax (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).dual.eraseMax.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₂ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.dual.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₃ :
  ∀
    (this :
      Valid' o₂ (l.node' x r).eraseMin.dual (↑(findMax' x l.dual) : WithTop αᵒᵈ) ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₄ :
  ∀
    (this :
      Valid' (↑(findMax' x l.dual) : WithTop αᵒᵈ) (l.node' x r).eraseMin o₂ ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀
    (this :
      Valid' (↑(l.findMin' x) : WithTop αᵒᵈ) (l.node' x r).eraseMin o₂ ∧
        (l.node' x r).size = (l.node' x r).eraseMin.size + 1),
    Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧
      (l.node' x r).size = (l.node' x r).eraseMin.size + 1
⊢ Valid' (↑(l.findMin' x) : WithBot α) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
    at this

Premises used: Ordnode.dual_node', Ordnode.size_dual, Ordnode.dual_eraseMin, Ordnode.findMax'_dual, Ordnode.Valid'.dual_iff
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size l x r).Valid
rw : (l.node' x r).eraseMin.Valid
⊢ (node size l x r).eraseMin.Valid

Tactic:
rw [h.2.eq_node']

Premises used: Ordnode.Valid'.sz, Ordnode.Sized.eq_node'
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size l x r).Valid
⊢ (l.node' x r).eraseMin.Valid

Tactic:
h.eraseMin_aux.1.valid

Premises used: Ordnode.Valid'.valid, Ordnode.Valid'.eraseMin_aux, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
size : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node size l x r).Valid
⊢ (l.node' x r).eraseMin.Valid

Tactic:
exact h.eraseMin_aux.1.valid

Premises used: Ordnode.Valid'.valid, Ordnode.Valid'.eraseMin_aux, And.left
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
h : t.Valid
rw : t.dual.eraseMin.Valid
⊢ t.eraseMax.Valid

Tactic:
rw [Valid.dual_iff, dual_eraseMax]

Premises used: Ordnode.Valid.dual_iff, Ordnode.dual_eraseMax
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid

Tactic:
eraseMin.valid h.dual

Premises used: Ordnode.eraseMin.valid, Ordnode.Valid.dual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid

Tactic:
exact eraseMin.valid h.dual

Premises used: Ordnode.eraseMin.valid, Ordnode.Valid.dual
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) l
bal : BalancedSz l.size r.size
nil :
  ∀ (hl : Valid' o₁ Ordnode.nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) Ordnode.nil)
    (bal : BalancedSz (size.{u_1} (α := α) Ordnode.nil) r.size),
    Valid' o₁ (glue Ordnode.nil r) o₂ ∧ (glue Ordnode.nil r).size = size.{u_1} (α := α) Ordnode.nil + r.size
node :
  ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α) (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr))
    (bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size),
    Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
      ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size
⊢ Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
hl : Valid' o₁ nil o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) nil
bal : BalancedSz (size.{u_1} (α := α) nil) r.size
⊢ Valid' o₁ (glue nil r) o₂ ∧ (glue nil r).size = size.{u_1} (α := α) nil + r.size

Tactic:
⟨hr, (zero_add _).symm⟩

Premises used: zero_add, And.intro, Eq.symm
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
hl : Valid' o₁ nil o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) nil
bal : BalancedSz (size.{u_1} (α := α) nil) r.size
⊢ Valid' o₁ (glue nil r) o₂ ∧ (glue nil r).size = size.{u_1} (α := α) nil + r.size

Tactic:
exact ⟨hr, (zero_add _).symm⟩
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hr : Valid' o₁ r o₂
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size r.size
node :
  ∀ (hr : Valid' o₁ nil o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) nil) (Ordnode.node ls ll lx lr))
    (bal : BalancedSz (Ordnode.node ls ll lx lr).size (size.{u_1} (α := α) nil)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
      ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + size.{u_1} (α := α) nil
node₁ :
  ∀ (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),
    Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
      ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
        (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue r) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue r).size = (Ordnode.node ls ll lx lr).size + r.size

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r
-- 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₂
hr : Valid' o₁ nil o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) nil) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (size.{u_1} (α := α) nil)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + size.{u_1} (α := α) nil

Tactic:
⟨hl, rfl⟩

Premises used: And.intro, 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₂
hr : Valid' o₁ nil o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) nil) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (size.{u_1} (α := α) nil)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue nil).size = (Ordnode.node ls ll lx lr).size + size.{u_1} (α := α) nil

Tactic:
exact ⟨hl, 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
node :
  Valid' o₁
      (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2)
      o₂ ∧
    (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size =
      ls + rs
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
dsimp [glue]

Premises used: Ordnode.glue
-- 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
pos :
  ls > rs →
    Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
      ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs
neg :
  ¬ls > rs →
    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
⊢ Valid' o₁
      (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2)
      o₂ ∧
    (if ls > rs then (ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).balanceL (rl.splitMin' rx rr).1 (rl.splitMin' rx rr).2).size =
      ls + rs

Tactic:
split_ifs
-- 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
pos :
  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
pos₁ : ℕ
⊢ Valid' o₁ ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)) o₂ ∧
    ((ll.splitMax' lx lr).1.balanceR (ll.splitMax' lx lr).2 (Ordnode.node rs rl rx rr)).size = ls + rs

Tactic:
rw [splitMax_eq]

Premises used: Ordnode.splitMax_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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl

Premises used: Ordnode.Valid'.eraseMax_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' o₁ (ll.node' lx lr).eraseMax (↑(findMax' lx lr) : WithTop α)
⊢ (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl

Premises used: Ordnode.Valid'.eraseMax_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' 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'
⊢ 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:
⟨Valid'.balanceR v (hr.of_gt ?_ ?_) H, ?_⟩

Premises used: Ordnode.Valid'.of_gt, And.intro, Ordnode.Valid'.balanceR