-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Balanced.ins {path : Path α}
    (hp : path.Balanced c₀ n₀ c n) (ht : t.RedRed (c = red) n) :
    ∃ n, (path.ins t).Balanced black n

Proof state:
α : 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 : l✝.Balanced black x✝
hb : r✝.Balanced black x✝
hr : y✝.Balanced black x✝
hp : Path.Balanced c₀ n₀ parent✝ red x✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t x✝ → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((left red parent✝ v✝¹ y✝).ins (node red l✝ v✝ r✝)).Balanced black n

Tactic:
exact ih (.redred rfl (.red ha hb) hr)

Result:
no goals

Proof state:
α : 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 : l✝.Balanced c₁✝ n✝
hb : r✝.Balanced c₂✝ n✝
hr : y✝.Balanced black (n✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (red = red) t (n✝ + 1) → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((left red parent✝ v✝¹ y✝).ins (node black l✝ v✝ r✝)).Balanced black n

Tactic:
exact ih (.balanced (.red (.black ha hb) hr))

Result:
no goals

Proof state:
α : 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, (path.ins t).Balanced black n

Tactic:
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)

Result:
no goals

Proof state:
α : 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 : l✝.Balanced black x✝
hb : r✝.Balanced black x✝
hl : x✝¹.Balanced black x✝
hp : Path.Balanced c₀ n₀ parent✝ red x✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t x✝ → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((right red x✝¹ v✝¹ parent✝).ins (node red l✝ v✝ r✝)).Balanced black n

Tactic:
exact ih (.redred rfl hl (.red ha hb))

Result:
no goals

Proof state:
α : 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 : y✝.Balanced black 0
hp : Path.Balanced c₀ n₀ parent✝ red 0
ih : ∀ {t : RBNode α}, RedRed (red = red) t 0 → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((left red parent✝ v✝ y✝).ins nil).Balanced black n

Tactic:
exact ih (.balanced (.red .nil hr))

Result:
no goals

Proof state:
α : 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 : l✝.Balanced c₁✝ n✝
hb : r✝.Balanced c₂✝ n✝
hl : x✝.Balanced black (n✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (red = red) t (n✝ + 1) → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((right red x✝ v✝¹ parent✝).ins (node black l✝ v✝ r✝)).Balanced black n

Tactic:
exact ih (.balanced (.red hl (.black ha hb)))

Result:
no goals

Proof state:
α : 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 : x✝.Balanced black 0
hp : Path.Balanced c₀ n₀ parent✝ red 0
ih : ∀ {t : RBNode α}, RedRed (red = red) t 0 → ∃ n, (parent✝.ins t).Balanced black n
⊢ ∃ n, ((right red x✝ v✝ parent✝).ins nil).Balanced black n

Tactic:
exact ih (.balanced (.red hl .nil))

Result:
no goals

Proof state:
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 : x✝.Balanced c₁✝ n✝
_hp : Path.Balanced c₀ n₀ parent✝ black (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (black = red) t (n✝ + 1) → ∃ n, (parent✝.ins t).Balanced black n
t : RBNode α
ht : RedRed (c₂✝ = red) t n✝
⊢ ∃ n, ((right black x✝ v✝ parent✝).ins t).Balanced black n

Tactic:
exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)

Result:
no goals

Proof state:
case redL
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
y✝ : RBNode α
n✝ : Nat
parent✝ : Path α
v✝ : α
hr : y✝.Balanced black n✝
hp : Path.Balanced c₀ n₀ parent✝ red n✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t n✝ → ∃ n, (parent✝.ins t).Balanced black n
t : RBNode α
ht : RedRed (black = red) t n✝
⊢ ∃ n, ((left red parent✝ v✝ y✝).ins t).Balanced black n

Tactic:
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))

Result:
no goals

Proof state:
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 : y✝.Balanced c₂✝ n✝
_hp : Path.Balanced c₀ n₀ parent✝ black (n✝ + 1)
ih : ∀ {t : RBNode α}, RedRed (black = red) t (n✝ + 1) → ∃ n, (parent✝.ins t).Balanced black n
t : RBNode α
ht : RedRed (c₁✝ = red) t n✝
⊢ ∃ n, ((left black parent✝ v✝ y✝).ins t).Balanced black n

Tactic:
exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)

Result:
no goals

Proof state:
case redR
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
x✝ : RBNode α
n✝ : Nat
v✝ : α
parent✝ : Path α
hl : x✝.Balanced black n✝
hp : Path.Balanced c₀ n₀ parent✝ red n✝
ih : ∀ {t : RBNode α}, RedRed (red = red) t n✝ → ∃ n, (parent✝.ins t).Balanced black n
t : RBNode α
ht : RedRed (black = red) t n✝
⊢ ∃ n, ((right red x✝ v✝ parent✝).ins t).Balanced black n

Tactic:
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)))

Result:
no goals

Proof state:
case root
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
t : RBNode α
ht : RedRed (c₀ = red) t n₀
⊢ ∃ n, (root.ins t).Balanced black n

Tactic:
exact ht.setBlack

Result:
no goals