-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.merge_aux {l r o₁ o₂} (hl : Valid' o₁ l o₂) (hr : Valid' o₁ r o₂)
    (sep : l.All fun x => r.All fun y => x < y) :
    Valid' o₁ (@merge α l r) o₂ ∧ size (merge l r) = size l + size r

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        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 α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        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 α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rl o₂ →
        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 α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rr o₂ →
        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₁ (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:
obtain ⟨v, e⟩ := IHlr hl.right (hr.of_gt hl.1.2.to_nil sep.2.1) sep.2.2

Result:
case pos.intro
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        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 α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        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 α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rl o₂ →
        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 α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rr o₂ →
        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) (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
⊢ 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