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

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
x✝ : RBNode α
n : Nat
v✝ : α
parent✝ : Path α
c' : RBColor
t : RBNode α
ht : DelProp c' t n
w✝ : Nat
hb : RedRed True t w✝
ha : x✝.Balanced black (w✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (w✝ + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (w✝ + 1) → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : black = black → black ≠ red
⊢ ∃ n, ((right red x✝ v✝ parent✝).del t black).Balanced black n

Tactic:
exact ih ((ha.balRight hb).of_false nofun) nofun

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
y✝ : RBNode α
c₂✝ : RBColor
n : Nat
parent✝ : Path α
v✝ : α
c₁✝ c' : RBColor
t : RBNode α
ht : DelProp c' t n
x✝ : Nat
w✝ : RBColor
ha : t.Balanced w✝ x✝
hb : y✝.Balanced c₂✝ x✝
hp : Path.Balanced c₀ n₀ parent✝ black (x✝ + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (x✝ + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : c₁✝ = black → red ≠ red
⊢ ∃ n, ((left black parent✝ v✝ y✝).del t red).Balanced black n

Tactic:
exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
c' : RBColor
t : RBNode α
ht : DelProp c' t n₀
w✝ : Nat
left✝ : n₀ = w✝ + 1
h : RedRed True t w✝
hc : c₀ = black → black ≠ red
⊢ ∃ n, (root.del t black).Balanced black n

Tactic:
exact h.setBlack

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
x✝¹ : RBNode α
c₁✝ : RBColor
n : Nat
v✝ : α
parent✝ : Path α
c₂✝ c' : RBColor
t : RBNode α
ht : DelProp c' t n
x✝ : Nat
w✝ : RBColor
hb : t.Balanced w✝ x✝
ha : x✝¹.Balanced c₁✝ x✝
hp : Path.Balanced c₀ n₀ parent✝ black (x✝ + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (x✝ + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : c₂✝ = black → red ≠ red
⊢ ∃ n, ((right black x✝¹ v✝ parent✝).del t red).Balanced black n

Tactic:
exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun

Result:
no goals

Proof state:
case root
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n : Nat
path : Path α
c' : RBColor
t : RBNode α
ht : DelProp c' t n₀
hc : c₀ = black → c' ≠ red
⊢ ∃ n, (root.del t c').Balanced black n

Tactic:
match c', ht with
| red, ⟨_, h⟩ | black, ⟨_, _, h⟩ => exact h.setBlack

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
ha : x✝.Balanced c₁✝ n
hp : Path.Balanced c₀ n₀ parent✝ black (n + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (n + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
c' : RBColor
t : RBNode α
ht : DelProp c' t n
hc : c₂✝ = black → c' ≠ red
⊢ ∃ n, ((right black x✝ v✝ parent✝).del t c').Balanced black n

Tactic:
match c', n, ht with
| red, _, ⟨_, hb⟩ => exact ih ⟨_, rfl, .redred ⟨⟩ ha hb⟩ nofun
| black, _, ⟨_, rfl, hb⟩ => exact ih ⟨_, rfl, (ha.balRight hb).imp fun _ => ⟨⟩⟩ nofun

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
x✝ : RBNode α
c₁✝ : RBColor
n : Nat
v✝ : α
parent✝ : Path α
c₂✝ c' : RBColor
t : RBNode α
ht : DelProp c' t n
w✝ : Nat
hb : RedRed True t w✝
ha : x✝.Balanced c₁✝ (w✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ black (w✝ + 1 + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (w✝ + 1 + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : c₂✝ = black → black ≠ red
⊢ ∃ n, ((right black x✝ v✝ parent✝).del t black).Balanced black n

Tactic:
exact ih ⟨_, rfl, (ha.balRight hb).imp fun _ => ⟨⟩⟩ nofun

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✝ : α
c' : RBColor
t : RBNode α
ht : DelProp c' t n
x✝¹ : Nat
x✝ : DelProp red t x✝¹
hb : y✝.Balanced black x✝¹
hp : Path.Balanced c₀ n₀ parent✝ red x✝¹
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t x✝¹ → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : black = black → red ≠ red
⊢ ∃ n, ((left red parent✝ v✝ y✝).del t red).Balanced black n

Tactic:
cases hc rfl rfl

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✝ : α
c' : RBColor
t : RBNode α
ht : DelProp c' t n
w✝ : Nat
ha : RedRed True t w✝
hb : y✝.Balanced black (w✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ red (w✝ + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (w✝ + 1) → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : black = black → black ≠ red
⊢ ∃ n, ((left red parent✝ v✝ y✝).del t black).Balanced black n

Tactic:
exact ih ((hb.balLeft ha).of_false nofun) nofun

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
y✝ : RBNode α
c₂✝ : RBColor
n : Nat
parent✝ : Path α
v✝ : α
c₁✝ c' : RBColor
t : RBNode α
ht : DelProp c' t n
w✝ : Nat
ha : RedRed True t w✝
hb : y✝.Balanced c₂✝ (w✝ + 1)
hp : Path.Balanced c₀ n₀ parent✝ black (w✝ + 1 + 1)
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t (w✝ + 1 + 1) → (black = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : c₁✝ = black → black ≠ red
⊢ ∃ n, ((left black parent✝ v✝ y✝).del t black).Balanced black n

Tactic:
exact ih ⟨_, rfl, (hb.balLeft ha).imp fun _ => ⟨⟩⟩ nofun

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 α
ha : x✝.Balanced black n
hp : Path.Balanced c₀ n₀ parent✝ red n
ih :
  ∀ {c' : RBColor} {t : RBNode α}, DelProp c' t n → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
c' : RBColor
t : RBNode α
ht : DelProp c' t n
hc : black = black → c' ≠ red
⊢ ∃ n, ((right red x✝ v✝ parent✝).del t c').Balanced black n

Tactic:
match c', n, ht with
| red, _, _ => cases hc rfl rfl
| black, _, ⟨_, rfl, hb⟩ => exact ih ((ha.balRight hb).of_false nofun) nofun

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 α
c' : RBColor
t : RBNode α
ht : DelProp c' t n
x✝¹ : Nat
x✝ : DelProp red t x✝¹
ha : x✝².Balanced black x✝¹
hp : Path.Balanced c₀ n₀ parent✝ red x✝¹
ih :
  ∀ {c' : RBColor} {t : RBNode α},
    DelProp c' t x✝¹ → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
hc : black = black → red ≠ red
⊢ ∃ n, ((right red x✝² v✝ parent✝).del t red).Balanced black n

Tactic:
cases hc rfl rfl

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✝ : α
hb : y✝.Balanced black n
hp : Path.Balanced c₀ n₀ parent✝ red n
ih :
  ∀ {c' : RBColor} {t : RBNode α}, DelProp c' t n → (red = black → c' ≠ red) → ∃ n, (parent✝.del t c').Balanced black n
c' : RBColor
t : RBNode α
ht : DelProp c' t n
hc : black = black → c' ≠ red
⊢ ∃ n, ((left red parent✝ v✝ y✝).del t c').Balanced black n

Tactic:
match c', n, ht with
| red, _, _ => cases hc rfl rfl
| black, _, ⟨_, rfl, ha⟩ => exact ih ((hb.balLeft ha).of_false nofun) nofun

Result:
no goals