-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.glue_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) (bal : BalancedSz (size l) (size r)) :
    Valid' o₁ (@glue α l r) o₂ ∧ size (glue l r) = size l + size r

Proof state:
case node.node
α : 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
⊢ 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

Result:
case pos
α : 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.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

case neg
α : 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₁ ((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

Proof state:
case refine_1
α : 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)
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'
⊢ nil.Bounded (↑((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2) o₂

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

Result:
case refine_1
α : 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)
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) → nil.Bounded (↑a) o₂

Proof state:
case node
α : 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
⊢ 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

Result:
case node.nil
α : 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 nil.size
⊢ 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 + nil.size

case node.node
α : 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
⊢ 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

Proof state:
α : 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
⊢ Valid' o₁ (l.glue r) o₂ ∧ (l.glue r).size = l.size + r.size

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l

Result:
case nil
α : 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 nil.size r.size
⊢ Valid' o₁ (nil.glue r) o₂ ∧ (nil.glue r).size = nil.size + r.size

case node
α : 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
⊢ 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