α : Type u_1
cut : α → Ordering
f : α → α
t : RBNode α
⊢ (match zoom cut t Path.root with
    | (nil, snd) => t
    | (node c a x b, path) => Path.fill path (node c a (f x) b)) =
    match zoom cut t Path.root with
    | (nil, path) =>
      match Option.map f none with
      | none => t
      | some y => Path.insertNew path y
    | (node c a x b, path) =>
      match Option.map f (some x) with
      | none => Path.del path (append a b) c
      | some y => Path.fill path (node c a y b)
α : Type u_1
cut : α → Ordering
f : α → α
t : RBNode α
⊢ modify cut f t = alter cut (Option.map f) t
simp [modify, alter]
no goals
α : Type u_1
cut : α → Ordering
f : α → α
t : RBNode α
⊢ (match zoom cut t Path.root with
    | (nil, snd) => t
    | (node c a x b, path) => Path.fill path (node c a (f x) b)) =
    match zoom cut t Path.root with
    | (nil, path) =>
      match Option.map f none with
      | none => t
      | some y => Path.insertNew path y
    | (node c a x b, path) =>
      match Option.map f (some x) with
      | none => Path.del path (append a b) c
      | some y => Path.fill path (node c a y b)
split <;> simp [Option.map]