case node
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
h₁ : p x
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : All p l✝ → All p (ins cmp x l✝)
r_ih✝ : All p r✝ → All p (ins cmp x r✝)
h₂ : All p (node c✝ l✝ v✝ r✝)
⊢ All p
    (match node c✝ l✝ v✝ r✝ with
    | nil => node red nil x nil
    | node red a y b =>
      match cmp x y with
      | Ordering.lt => node red (ins cmp x a) y b
      | Ordering.gt => node red a y (ins cmp x b)
      | Ordering.eq => node red a x b
    | node black a y b =>
      match cmp x y with
      | Ordering.lt => balance1 (ins cmp x a) y b
      | Ordering.gt => balance2 a y (ins cmp x b)
      | Ordering.eq => node black a x b)
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
t : RBNode α
h₁ : p x
h₂ : All p t
⊢ All p (ins cmp x t)
induction t <;> unfold ins <;> simp [*]
no goals
case node
α : Type u_1
p : α → Prop
cmp : α → α → Ordering
x : α
h₁ : p x
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : All p l✝ → All p (ins cmp x l✝)
r_ih✝ : All p r✝ → All p (ins cmp x r✝)
h₂ : All p (node c✝ l✝ v✝ r✝)
⊢ All p
    (match node c✝ l✝ v✝ r✝ with
    | nil => node red nil x nil
    | node red a y b =>
      match cmp x y with
      | Ordering.lt => node red (ins cmp x a) y b
      | Ordering.gt => node red a y (ins cmp x b)
      | Ordering.eq => node red a x b
    | node black a y b =>
      match cmp x y with
      | Ordering.lt => balance1 (ins cmp x a) y b
      | Ordering.gt => balance2 a y (ins cmp x b)
      | Ordering.eq => node black a x b)
split <;> cases ‹_=_› <;> split <;> simp at h₂ <;> simp [*]