α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : Balanced t c n
⊢ ∃ c' n',
    Balanced
      (match isRed t with
      | red => setBlack (ins cmp v t)
      | black => ins cmp v t)
      c' n'
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : Balanced t c n
⊢ ∃ c' n', Balanced (RBNode.insert cmp t v) c' n'
unfold insert
no goals
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : Balanced t c n
⊢ ∃ c' n',
    Balanced
      (match isRed t with
      | red => setBlack (ins cmp v t)
      | black => ins cmp v t)
      c' n'
match ins cmp v t, h.ins cmp v with
| _, .balanced h => split <;> [exact ⟨_, h.setBlack⟩; exact ⟨_, _, h⟩]
| _, .redred _ ha hb => have .node red .. := t; exact ⟨_, _, .black ha hb⟩
no goals
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h✝ : Balanced t c n
x✝ : RBNode α
c✝ : RBColor
h : Balanced x✝ c✝ n
⊢ ∃ c' n',
    Balanced
      (match isRed t with
      | red => setBlack x✝
      | black => x✝)
      c' n'
split <;> [exact ⟨_, h.setBlack⟩; exact ⟨_, _, h⟩]
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
ha : Balanced a✝¹ c₁✝ n
hb : Balanced b✝ c₂✝ n
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
h : Balanced (node red l✝ v✝ r✝) c n
a✝ : isRed (node red l✝ v✝ r✝) = red
⊢ ∃ c' n',
    Balanced
      (match isRed (node red l✝ v✝ r✝) with
      | red => setBlack (node red a✝¹ x✝ b✝)
      | black => node red a✝¹ x✝ b✝)
      c' n'
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t : RBNode α
h : Balanced t c n
a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
a✝ : isRed t = red
ha : Balanced a✝¹ c₁✝ n
hb : Balanced b✝ c₂✝ n
⊢ ∃ c' n',
    Balanced
      (match isRed t with
      | red => setBlack (node red a✝¹ x✝ b✝)
      | black => node red a✝¹ x✝ b✝)
      c' n'
have .node red .. := t
no goals
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
t a✝¹ : RBNode α
c₁✝ : RBColor
b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
ha : Balanced a✝¹ c₁✝ n
hb : Balanced b✝ c₂✝ n
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
h : Balanced (node red l✝ v✝ r✝) c n
a✝ : isRed (node red l✝ v✝ r✝) = red
⊢ ∃ c' n',
    Balanced
      (match isRed (node red l✝ v✝ r✝) with
      | red => setBlack (node red a✝¹ x✝ b✝)
      | black => node red a✝¹ x✝ b✝)
      c' n'
exact ⟨_, _, .black ha hb⟩