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 α
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_2 : ll.size + lr.size + 1 + rl.size + rr.size + 1 = ll.size + lr.size + 1 + (rl.size + rr.size + 1)
⊢ (t.balanceL rx rr).size = ls + rs

Tactic:
rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]

Premises used: Ordnode.Valid'.bal, Ordnode.balance_eq_balance', Ordnode.Valid'.sz, Ordnode.balanceL_eq_balance, Ordnode.size_balance', 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 α
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
⊢ ll.size + lr.size + 1 + rl.size + rr.size + 1 = ll.size + lr.size + 1 + (rl.size + rr.size + 1)

Tactic:
abel
-- 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
suffices : t.size = 0 → rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
-- 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
rw : ll.size + lr.size + rl.size + 1 = 0 → rr.size ≤ 1
⊢ t.size = 0 → rr.size ≤ 1

Tactic:
rw [e, add_right_comm]

Premises used: add_right_comm
-- 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
inr : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
suffices H₂ : _ by
    suffices H₁ : _ by
      refine ⟨Valid'.balanceL_aux v hr.right H₁ H₂ ?_, ?_⟩
      · rw [e]; exact Or.inl (Valid'.merge_lemma h hr₁)
      · rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
          size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
        abel
    · rw [e, add_right_comm]; rintro ⟨⟩
-- 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 : 1 ≤ t.size
inr : 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ 1 ≤ rr.size → rr.size ≤ delta * t.size

Tactic:
_
-- 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 : 1 ≤ t.size
h_2 : 1 ≤ rr.size
inr : rr.size ≤ delta * (ll.size + lr.size + 1 + rl.size)
⊢ rr.size ≤ delta * t.size

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 ≤ 3 * rl.size
h_1 : 1 ≤ t.size
h_2 : 1 ≤ rr.size
⊢ rr.size ≤ 3 * (ll.size + lr.size + 1 + rl.size)

Tactic:
lia
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ nil o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) nil
⊢ Valid' o₁ (merge nil r) o₂ ∧ (merge 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 α
hl : Valid' o₁ nil o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) nil
⊢ Valid' o₁ (merge nil r) o₂ ∧ (merge 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 α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size

Tactic:
?_
-- 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
node :
  ∀ (ls : ℕ) (ll : Ordnode α) (lx : α) (lr : Ordnode α),
    (∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
        (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
        Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size) →
      ∀
        (IHlr :
          ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
            (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
            Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size)
        {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
        (hr : Valid' o₁ r o₂) (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)),
        Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
          ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size
⊢ Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size

Tactic:
induction l generalizing o₁ o₂ r with
  | nil => exact ⟨hr, (zero_add _).symm⟩
  | node ls ll lx lr _ IHlr => ?_

Premises used: Ordnode.nil, Ordnode.Valid'.node
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
o₁ : WithBot α
o₂ : WithTop α
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)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge 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 α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
o₁ : WithBot α
o₂ : WithTop α
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)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge 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 α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
?_
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) (Ordnode.node ls ll lx lr)
node :
  ∀ (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α)
    (IHrl :
      ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
        (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
        Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
          ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size),
    (∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
        (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
        Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
          ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size) →
      ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂)
        (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)),
        Valid' o₁ ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)) o₂ ∧
          ((Ordnode.node ls ll lx lr).merge (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).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size

Tactic:
induction r generalizing o₁ o₂ with
  | nil => exact ⟨hl, rfl⟩
  | node rs rl rx rr IHrl _ => ?_

Premises used: Ordnode.nil, Ordnode.Valid'.node
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
node :
  Valid' o₁
      (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
      else
        if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
        else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr))
      o₂ ∧
    (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
        else
          if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
          else (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).merge (Ordnode.node rs rl rx rr)) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge (Ordnode.node rs rl rx rr)).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
rw [merge_node]

Premises used: Ordnode.merge_node
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
pos :
  ∀ (h : delta * ls < rs),
    Valid' o₁ (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr) o₂ ∧
      (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr).size =
        (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
pos₁ :
  ∀ (h : ¬delta * ls < rs) (h_1 : delta * rs < ls),
    Valid' o₁ (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))) o₂ ∧
      (ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))).size =
        (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size
neg :
  ∀ (h : ¬delta * ls < rs) (h_1 : ¬delta * rs < ls),
    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₁
      (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
      else
        if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
        else (Ordnode.node ls ll lx lr).glue (Ordnode.node rs rl rx rr))
      o₂ ∧
    (if delta * ls < rs then ((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr
        else
          if delta * rs < ls then ll.balanceR lx (lr.merge (Ordnode.node rs rl rx rr))
          else (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:
split_ifs with h h_1
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ ll o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) ll),
    Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ lr o₂) (hr : Valid' o₁ r o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) lr),
    Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rl o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rl) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α} (hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Valid' o₁ rr o₂)
    (sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) rr) (Ordnode.node ls ll lx lr)),
    Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
      ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
h : delta * ls < rs
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)

Tactic:
obtain ⟨v, e⟩ := IHrl (hl.of_lt hr.1.1.to_nil <| sep.imp fun x h => h.2.1) hr.left
      (sep.imp fun x h => h.1)

Premises used: And.left, Ordnode.Valid'.ord, Ordnode.Valid'.of_lt, Ordnode.Bounded.to_nil, Ordnode.All.imp, Ordnode.Valid'.left