-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Balanced.alter {t : RBNode α}
    (h : t.Balanced c n) : ∃ c n, (t.alter cut f).Balanced c n

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c n,
    (match zoom cut t with
        | (nil, path) =>
          match f none with
          | none => t
          | some y => path.insertNew y
        | (node c a x b, path) =>
          match f (some x) with
          | none => path.del (a.append b) c
          | some y => path.fill (node c a y b)).Balanced
      c n

Tactic:
split

Result:
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝ : RBNode α × Path α
snd✝ : Path α
heq✝ : zoom cut t = (nil, snd✝)
⊢ ∃ c n,
    (match f none with
        | none => t
        | some y => snd✝.insertNew y).Balanced
      c n

case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path✝ : Path α
heq✝ : zoom cut t = (node c✝ a✝ x✝ b✝, path✝)
⊢ ∃ c n,
    (match f (some x✝) with
        | none => path✝.del (a✝.append b✝) c✝
        | some y => path✝.fill (node c✝ a✝ y b✝)).Balanced
      c n

Proof state:
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
heq✝ : f none = none
⊢ ∃ c n, t.Balanced c n

Tactic:
exact ⟨_, _, h⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
⊢ ∃ c n,
    (match f none with
        | none => t
        | some y => path.insertNew y).Balanced
      c n

Tactic:
split

Result:
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
heq✝ : f none = none
⊢ ∃ c n, t.Balanced c n

case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
⊢ ∃ c n, (path.insertNew y✝).Balanced c n

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝¹ b✝).Balanced w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
ha : a✝.Balanced c₁✝ n✝
hb : b✝.Balanced c₂✝ n✝
eq : zoom cut t = (node black a✝ x✝¹ b✝, path)
hp : Path.Balanced c n path black (n✝ + 1)
⊢ ∃ c n, (path.fill (node black a✝ y✝ b✝)).Balanced c n

Tactic:
exact ⟨_, _, hp.fill (.black ha hb)⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝¹ b✝).Balanced w✝¹ w✝
x✝ : Option α
heq✝ : f (some x✝¹) = none
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
ha : a✝.Balanced c₁✝ n✝
hb : b✝.Balanced c₂✝ n✝
eq : zoom cut t = (node black a✝ x✝¹ b✝, path)
hp : Path.Balanced c n path black (n✝ + 1)
⊢ ∃ c n, (path.del (a✝.append b✝) black).Balanced c n

Tactic:
exact ⟨_, hp.del ⟨_, rfl, (ha.append hb).imp fun _ => ⟨⟩⟩ nofun⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝ b✝).Balanced w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
⊢ ∃ c n,
    (match f (some x✝) with
        | none => path.del (a✝.append b✝) c✝
        | some y => path.fill (node c✝ a✝ y b✝)).Balanced
      c n

Tactic:
split

Result:
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝¹ b✝).Balanced w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
heq✝ : f (some x✝¹) = none
⊢ ∃ c n, (path.del (a✝.append b✝) c✝).Balanced c n

case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝¹ b✝).Balanced w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ ∃ c n, (path.fill (node c✝ a✝ y✝ b✝)).Balanced c n

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c n, (alter cut f t).Balanced c n

Tactic:
simp [alter]

Result:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
⊢ ∃ c n,
    (match zoom cut t with
        | (nil, path) =>
          match f none with
          | none => t
          | some y => path.insertNew y
        | (node c a x b, path) =>
          match f (some x) with
          | none => path.del (a.append b) c
          | some y => path.fill (node c a y b)).Balanced
      c n

Proof state:
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝¹ b✝).Balanced w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ ∃ c n, (path.fill (node c✝ a✝ y✝ b✝)).Balanced c n

Tactic:
match h with
| .red ha hb => exact ⟨_, _, hp.fill (.red ha hb)⟩
| .black ha hb => exact ⟨_, _, hp.fill (.black ha hb)⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝³ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝² : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝² b✝).Balanced w✝¹ w✝
x✝¹ : Option α
y✝ : α
heq✝ : f (some x✝²) = some y✝
x✝ : Nat
ha : a✝.Balanced black x✝
hb : b✝.Balanced black x✝
eq : zoom cut t = (node red a✝ x✝² b✝, path)
hp : Path.Balanced c n path red x✝
⊢ ∃ c n, (path.fill (node red a✝ y✝ b✝)).Balanced c n

Tactic:
exact ⟨_, _, hp.fill (.red ha hb)⟩

Result:
no goals

Proof state:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : t.Balanced c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝ b✝, path)
⊢ ∃ c n,
    (match f (some x✝) with
        | none => path.del (a✝.append b✝) c✝
        | some y => path.fill (node c✝ a✝ y b✝)).Balanced
      c n

Tactic:
have ⟨_, _, h, hp⟩ := h.zoom .root eq

Result:
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : t.Balanced c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t = (node c✝ a✝ x✝ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : (node c✝ a✝ x✝ b✝).Balanced w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
⊢ ∃ c n,
    (match f (some x✝) with
        | none => path.del (a✝.append b✝) c✝
        | some y => path.fill (node c✝ a✝ y b✝)).Balanced
      c n