Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case lt
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

pp: case eq
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.eq.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

pp: case gt
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.gt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.lt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.lt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

case eq
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.eq with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.eq.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

case gt
α : Type u_1
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match Ordering.gt with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match Ordering.gt.swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)