α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : Balanced x✝ black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : Balanced t black n
⊢ ins parent✝ (node red x✝ v✝ t) = setBlack (fill (right red x✝ v✝ parent✝) t)
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : Balanced x✝ black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : Balanced t black n
⊢ ins (right red x✝ v✝ parent✝) t = setBlack (fill (right red x✝ v✝ parent✝) t)
unfold ins
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : Balanced x✝ black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : Balanced t black n
⊢ ins parent✝ (node red x✝ v✝ t) = setBlack (fill (right red x✝ v✝ parent✝) t)
exact ins_eq_fill H (.red ha hb)
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c✝ : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
c : RBColor
y✝ : RBNode α
c₂✝ : RBColor
parent✝ : Path α
v✝ : α
hb : Balanced y✝ c₂✝ n
H : Path.Balanced c₀ n₀ parent✝ black (n + 1)
ha : Balanced t c n
⊢ ins (left black parent✝ v✝ y✝) t = setBlack (fill (left black parent✝ v✝ y✝) t)
rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance1_eq ha]
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c✝ : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
c : RBColor
x✝ : RBNode α
c₁✝ : RBColor
v✝ : α
parent✝ : Path α
ha : Balanced x✝ c₁✝ n
H : Path.Balanced c₀ n₀ parent✝ black (n + 1)
hb : Balanced t c n
⊢ ins (right black x✝ v✝ parent✝) t = setBlack (fill (right black x✝ v✝ parent✝) t)
rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance2_eq hb]