α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (eraseMax (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l))) ↑(findMax' x (Ordnode.dual l)) ∧
    size (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l)) =
      size (eraseMax (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l))) + 1
⊢ Valid' (↑(findMin' l x)) (eraseMin (Ordnode.node' l x r)) o₂ ∧
    size (Ordnode.node' l x r) = size (eraseMin (Ordnode.node' l x r)) + 1
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑(findMin' l x)) (eraseMin (Ordnode.node' l x r)) o₂ ∧
    size (Ordnode.node' l x r) = size (eraseMin (Ordnode.node' l x r)) + 1
have := H.dual.eraseMax_aux
no goals
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (eraseMax (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l))) ↑(findMax' x (Ordnode.dual l)) ∧
    size (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l)) =
      size (eraseMax (Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l))) + 1
⊢ Valid' (↑(findMin' l x)) (eraseMin (Ordnode.node' l x r)) o₂ ∧
    size (Ordnode.node' l x r) = size (eraseMin (Ordnode.node' l x r)) + 1
rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
  at this