no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
t : RBNode α
path : Path α
hp : Path.Balanced c₀ n₀ path c n
ht : RedRed (c = red) t n
⊢ ∃ n, Balanced (ins path t) black n
induction hp generalizing t with
| root => exact ht.setBlack
| redL hr hp ih => match ht with
  | .balanced .nil => exact ih (.balanced (.red .nil hr))
  | .balanced (.red ha hb) => exact ih (.redred rfl (.red ha hb) hr)
  | .balanced (.black ha hb) => exact ih (.balanced (.red (.black ha hb) hr))
| redR hl hp ih => match ht with
  | .balanced .nil => exact ih (.balanced (.red hl .nil))
  | .balanced (.red ha hb) => exact ih (.redred rfl hl (.red ha hb))
  | .balanced (.black ha hb) => exact ih (.balanced (.red hl (.black ha hb)))
| blackL hr hp ih => exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
| blackR hl hp ih => exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)
no goals
case root
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
t : RBNode α
ht : RedRed (c₀ = red) t n₀
⊢ ∃ n, Balanced (ins root t) black n
exact ht.setBlack
no goals
case redL
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
n✝ : Nat
parent✝ : Path α
v✝ : α
hr : Balanced y✝ black n✝
hp : Path.Balanced c₀ n₀ parent✝ red n✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t n✝ → ∃ n, Balanced (ins parent✝ t) black n
t : RBNode α
ht : RedRed (black = red) t n✝
⊢ ∃ n, Balanced (ins (left red parent✝ v✝ y✝) t) black n
match ht with
| .balanced .nil => exact ih (.balanced (.red .nil hr))
| .balanced (.red ha hb) => exact ih (.redred rfl (.red ha hb) hr)
| .balanced (.black ha hb) => exact ih (.balanced (.red (.black ha hb) hr))
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
n✝ : Nat
parent✝ : Path α
v✝ : α
t : RBNode α
ht : RedRed (black = red) t n✝
hr : Balanced y✝ black 0
hp : Path.Balanced c₀ n₀ parent✝ red 0
ih : ∀ {t : RBNode α}, RedRed (red = red) t 0 → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (left red parent✝ v✝ y✝) nil) black n
exact ih (.balanced (.red .nil hr))
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
n✝ : Nat
parent✝ : Path α
v✝¹ : α
t : RBNode α
ht : RedRed (black = red) t n✝
x✝ : Nat
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ha : Balanced l✝ black x✝
hb : Balanced r✝ black x✝
hr : Balanced y✝ black x✝
hp : Path.Balanced c₀ n₀ parent✝ red x✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t x✝ → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (left red parent✝ v✝¹ y✝) (node red l✝ v✝ r✝)) black n
exact ih (.redred rfl (.red ha hb) hr)
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
n✝¹ : Nat
parent✝ : Path α
v✝¹ : α
t : RBNode α
ht : RedRed (black = red) t n✝¹
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
n✝ : Nat
c₁✝ c₂✝ : RBColor
ha : Balanced l✝ c₁✝ n✝
hb : Balanced r✝ c₂✝ n✝
hr : Balanced y✝ black (n✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (red = red) t (n✝ + 1) → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (left red parent✝ v✝¹ y✝) (node black l✝ v✝ r✝)) black n
exact ih (.balanced (.red (.black ha hb) hr))
no goals
case redR
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝ : RBNode α
n✝ : Nat
v✝ : α
parent✝ : Path α
hl : Balanced x✝ black n✝
hp : Path.Balanced c₀ n₀ parent✝ red n✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t n✝ → ∃ n, Balanced (ins parent✝ t) black n
t : RBNode α
ht : RedRed (black = red) t n✝
⊢ ∃ n, Balanced (ins (right red x✝ v✝ parent✝) t) black n
match ht with
| .balanced .nil => exact ih (.balanced (.red hl .nil))
| .balanced (.red ha hb) => exact ih (.redred rfl hl (.red ha hb))
| .balanced (.black ha hb) => exact ih (.balanced (.red hl (.black ha hb)))
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝ : RBNode α
n✝ : Nat
v✝ : α
parent✝ : Path α
t : RBNode α
ht : RedRed (black = red) t n✝
hl : Balanced x✝ black 0
hp : Path.Balanced c₀ n₀ parent✝ red 0
ih : ∀ {t : RBNode α}, RedRed (red = red) t 0 → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (right red x✝ v✝ parent✝) nil) black n
exact ih (.balanced (.red hl .nil))
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝¹ : RBNode α
n✝ : Nat
v✝¹ : α
parent✝ : Path α
t : RBNode α
ht : RedRed (black = red) t n✝
x✝ : Nat
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
ha : Balanced l✝ black x✝
hb : Balanced r✝ black x✝
hl : Balanced x✝¹ black x✝
hp : Path.Balanced c₀ n₀ parent✝ red x✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t x✝ → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (right red x✝¹ v✝¹ parent✝) (node red l✝ v✝ r✝)) black n
exact ih (.redred rfl hl (.red ha hb))
no goals
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝ : RBNode α
n✝¹ : Nat
v✝¹ : α
parent✝ : Path α
t : RBNode α
ht : RedRed (black = red) t n✝¹
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
n✝ : Nat
c₁✝ c₂✝ : RBColor
ha : Balanced l✝ c₁✝ n✝
hb : Balanced r✝ c₂✝ n✝
hl : Balanced x✝ black (n✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (red = red) t (n✝ + 1) → ∃ n, Balanced (ins parent✝ t) black n
⊢ ∃ n, Balanced (ins (right red x✝ v✝¹ parent✝) (node black l✝ v✝ r✝)) black n
exact ih (.balanced (.red hl (.black ha hb)))
no goals
case blackL
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
c₂✝ : RBColor
n✝ : Nat
parent✝ : Path α
v✝ : α
c₁✝ : RBColor
hr : Balanced y✝ c₂✝ n✝
hp : Path.Balanced c₀ n₀ parent✝ black (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (black = red) t (n✝ + 1) → ∃ n, Balanced (ins parent✝ t) black n
t : RBNode α
ht : RedRed (c₁✝ = red) t n✝
⊢ ∃ n, Balanced (ins (left black parent✝ v✝ y✝) t) black n
exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
no goals
case blackR
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
v✝ : α
parent✝ : Path α
c₂✝ : RBColor
hl : Balanced x✝ c₁✝ n✝
hp : Path.Balanced c₀ n₀ parent✝ black (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (black = red) t (n✝ + 1) → ∃ n, Balanced (ins parent✝ t) black n
t : RBNode α
ht : RedRed (c₂✝ = red) t n✝
⊢ ∃ n, Balanced (ins (right black x✝ v✝ parent✝) t) black n
exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)