c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h :
  match c with
  | black => ∃ n', n = n' + 1 ∧ RedRed True t n'
  | red => ∃ c, Balanced t c n
⊢ ∃ n', RedRed (c = black) t n'
c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h : DelProp c t n
⊢ ∃ n', RedRed (c = black) t n'
unfold DelProp at h
no goals
c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h :
  match c with
  | black => ∃ n', n = n' + 1 ∧ RedRed True t n'
  | red => ∃ c, Balanced t c n
⊢ ∃ n', RedRed (c = black) t n'
exact match c, h with
| red, ⟨_, h⟩ => ⟨_, .balanced h⟩
| black, ⟨_, _, h⟩ => ⟨_, h.imp fun _ => rfl⟩