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

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

case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : Balanced t c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
⊢ ∃ c n, Balanced (Path.insertNew path y✝) c n
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : Balanced t c n
x✝ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
⊢ ∃ c n,
    Balanced
      (match f none with
      | none => t
      | some y => Path.insertNew path y)
      c n
split
no goals
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : Balanced t c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
x✝ : Option α
heq✝ : f none = none
⊢ ∃ c n, Balanced t c n
exact ⟨_, _, h⟩
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
h : Path.Balanced c n path black 0
⊢ ∃ c n, Balanced (Path.insertNew path y✝) c n
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : Balanced t c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
⊢ ∃ c n, Balanced (Path.insertNew path y✝) c n
have ⟨_, _, .nil, h⟩ := h.zoom .root eq
no goals
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝¹ : RBNode α × Path α
path : Path α
eq : zoom cut t Path.root = (nil, path)
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
h : Path.Balanced c n path black 0
⊢ ∃ c n, Balanced (Path.insertNew path y✝) c n
exact ⟨_, h.insertNew⟩
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝ b✝) w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
⊢ ∃ c n,
    Balanced
      (match f (some x✝) with
      | none => Path.del path (append a✝ b✝) c✝
      | some y => Path.fill path (node c✝ a✝ y b✝))
      c n
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h : Balanced t c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝ b✝, path)
⊢ ∃ c n,
    Balanced
      (match f (some x✝) with
      | none => Path.del path (append a✝ b✝) c✝
      | some y => Path.fill path (node c✝ a✝ y b✝))
      c n
have ⟨_, _, h, hp⟩ := h.zoom .root eq
case h_1
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝¹ b✝) w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
heq✝ : f (some x✝¹) = none
⊢ ∃ c n, Balanced (Path.del path (append a✝ b✝) c✝) c n

case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝¹ b✝) w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ ∃ c n, Balanced (Path.fill path (node c✝ a✝ y✝ b✝)) c n
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝¹ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝ b✝) w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
⊢ ∃ c n,
    Balanced
      (match f (some x✝) with
      | none => Path.del path (append a✝ b✝) c✝
      | some y => Path.fill path (node c✝ a✝ y b✝))
      c n
split
no goals
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝¹ b✝) w✝¹ w✝
x✝ : Option α
heq✝ : f (some x✝¹) = none
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
ha : Balanced a✝ c₁✝ n✝
hb : Balanced b✝ c₂✝ n✝
eq : zoom cut t Path.root = (node black a✝ x✝¹ b✝, path)
hp : Path.Balanced c n path black (n✝ + 1)
⊢ ∃ c n, Balanced (Path.del path (append a✝ b✝) black) c n
exact ⟨_, hp.del ⟨_, rfl, (ha.append hb).imp fun _ => ⟨⟩⟩ (fun.)⟩
no goals
case h_2
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : zoom cut t Path.root = (node c✝ a✝ x✝¹ b✝, path)
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝¹ b✝) w✝¹ w✝
hp : Path.Balanced c n path w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ ∃ c n, Balanced (Path.fill path (node c✝ a✝ y✝ b✝)) c n
match h with
| .red ha hb => exact ⟨_, _, hp.fill (.red ha hb)⟩
| .black ha hb => exact ⟨_, _, hp.fill (.black ha hb)⟩
no goals
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝³ : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝² : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝² b✝) w✝¹ w✝
x✝¹ : Option α
y✝ : α
heq✝ : f (some x✝²) = some y✝
x✝ : Nat
ha : Balanced a✝ black x✝
hb : Balanced b✝ black x✝
eq : zoom cut t Path.root = (node red a✝ x✝² b✝, path)
hp : Path.Balanced c n path red x✝
⊢ ∃ c n, Balanced (Path.fill path (node red a✝ y✝ b✝)) c n
exact ⟨_, _, hp.fill (.red ha hb)⟩
no goals
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
f : Option α → Option α
t : RBNode α
h✝ : Balanced t c n
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
w✝¹ : RBColor
w✝ : Nat
h : Balanced (node c✝ a✝ x✝¹ b✝) w✝¹ w✝
x✝ : Option α
y✝ : α
heq✝ : f (some x✝¹) = some y✝
c₁✝ : RBColor
n✝ : Nat
c₂✝ : RBColor
ha : Balanced a✝ c₁✝ n✝
hb : Balanced b✝ c₂✝ n✝
eq : zoom cut t Path.root = (node black a✝ x✝¹ b✝, path)
hp : Path.Balanced c n path black (n✝ + 1)
⊢ ∃ c n, Balanced (Path.fill path (node black a✝ y✝ b✝)) c n
exact ⟨_, _, hp.fill (.black ha hb)⟩