α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ ModifyWF t cut f
refine ⟨.modify ?_ t.2⟩
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
H : ∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x
⊢ OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
revert H
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, root? (zoom cut t.val Path.root).fst = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, RBNode.find? cut t.val = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
rw [find?_eq_zoom]
no goals
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
f : α → α
t : RBSet α cmp
⊢ (∀ {x : α}, root? (zoom cut t.val Path.root).fst = some x → cmpEq cmp (f x) x) →
    OnRoot (fun x => cmpEq cmp (f x) x) (zoom cut t.val Path.root).fst
cases (t.1.zoom cut).1 <;> intro H <;> [trivial; exact H rfl]