α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ dual (Ordnode.insert x (node size✝ l y r)) = Ordnode.insert x (dual (node size✝ l y r))
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ dual (Ordnode.insert x (node size✝ l y r)) = Ordnode.insert x (dual (node size✝ l y r))
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ dual
      (match cmpLE x y with
      | Ordering.lt => balanceL (Ordnode.insert x l) y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => balanceR l y (Ordnode.insert x r)) =
    match Ordering.swap (cmpLE x y) with
    | Ordering.lt => balanceL (Ordnode.insert x (dual r)) y (dual l)
    | Ordering.eq => node size✝ (dual r) x (dual l)
    | Ordering.gt => balanceR (dual r) y (Ordnode.insert x (dual l))
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ dual (Ordnode.insert x (node size✝ l y r)) = Ordnode.insert x (dual (node size✝ l y r))
rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]
no goals
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ dual
      (match cmpLE x y with
      | Ordering.lt => balanceL (Ordnode.insert x l) y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => balanceR l y (Ordnode.insert x r)) =
    match Ordering.swap (cmpLE x y) with
    | Ordering.lt => balanceL (Ordnode.insert x (dual r)) y (dual l)
    | Ordering.eq => node size✝ (dual r) x (dual l)
    | Ordering.gt => balanceR (dual r) y (Ordnode.insert x (dual l))
cases cmpLE x y <;>
  simp [Ordering.swap, Ordnode.insert, dual_balanceL, dual_balanceR, dual_insert]