Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: 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
⊢ 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

pp: 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

pp: case neg
α : 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₁ ((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:
· 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)
    exact Valid'.merge_aux₁ hl hr h v e

Goal state after:
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

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