awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)
⊢ ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size

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
-- 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
v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)
e : ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
⊢ 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

Tactic:
Valid'.merge_aux₁ hl hr h v e

Premises used: Ordnode.Valid'.merge_aux₁
-- 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
v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) (↑rx : WithTop α)
e : ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
⊢ 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

Tactic:
exact Valid'.merge_aux₁ hl hr h v e

Premises used: Ordnode.Valid'.merge_aux₁
-- 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
h_1 : delta * rs < ls
⊢ Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂

Tactic:
obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2

Premises used: Ordnode.Valid'.of_gt, Ordnode.Valid'.right, And.right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil
-- 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
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
⊢ (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size

Tactic:
obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2

Premises used: Ordnode.Valid'.of_gt, Ordnode.Valid'.right, And.right, And.left, Ordnode.Valid'.ord, Ordnode.Bounded.to_nil
-- 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
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
⊢ ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).dual.size = rs + lr.dual.size),
    Valid' o₂ ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual) o₁ ∧
      ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual).size = rs + ls

Tactic:
have := Valid'.merge_aux₁ hr.dual hl.dual h_1 v.dual
-- 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
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
this :
  ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).dual.size = rs + lr.dual.size),
    Valid' o₂ ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual) o₁ ∧
      ((lr.merge (Ordnode.node rs rl rx rr)).dual.balanceL lx ll.dual).size = rs + ls
⊢ ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + rs),
    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 = ls + rs

Tactic:
rw [size_dual, add_comm, size_dual, ← dual_balanceR, ← Valid'.dual_iff, size_dual,
      add_comm rs] at this

Premises used: Ordnode.size_dual, Ordnode.dual_balanceR, add_comm, Ordnode.Valid'.dual_iff
-- 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
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
this :
  ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + rs),
    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 = ls + rs
⊢ 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

Tactic:
this e

Premises used: OrderDual
-- 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
h_1 : delta * rs < ls
v : Valid' (↑lx : WithBot α) (lr.merge (Ordnode.node rs rl rx rr)) o₂
e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + (Ordnode.node rs rl rx rr).size
this :
  ∀ (e : (lr.merge (Ordnode.node rs rl rx rr)).size = lr.size + rs),
    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 = ls + rs
⊢ 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

Tactic:
exact this e
-- 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
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

Tactic:
Valid'.glue_aux hl hr sep (Or.inr ⟨not_lt.1 h_1, not_lt.1 h⟩)

Premises used: Ordnode.Valid'.glue_aux, not_lt, And.intro, Iff.mp, Or.inr
-- 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
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

Tactic:
refine Valid'.glue_aux hl hr sep (Or.inr ⟨not_lt.1 h_1, not_lt.1 h⟩)

Premises used: Ordnode.Valid'.glue_aux, not_lt, And.intro, Iff.mp, Or.inr
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
l r : Ordnode α
hl : l.Valid
hr : r.Valid
sep : All (fun (x : α) ↦ All (fun (y : α) ↦ x < y) r) l
⊢ (l.merge r).Valid

Tactic:
(Valid'.merge_aux hl hr sep).1

Premises used: Ordnode.Valid, And.left, Ordnode.Valid'.merge_aux