-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.alter {t : RBNode α}
    (H : ∀ {x t' p}, t.zoom cut = (t', p) → f t'.root? = some x →
      p.RootOrdered cmp x ∧ t'.OnRoot (cmpEq cmp x))
    (h : t.Ordered cmp) : (alter cut f t).Ordered cmp

Proof state:
α : Type u_1
cut : α → Ordering
f : Option α → Option α
cmp : α → α → Ordering
t : RBNode α
H :
  ∀ {x : α} {t' : RBNode α} {p : Path α},
    RBNode.zoom cut t = (t', p) → f t'.root? = some x → Path.RootOrdered cmp p x ∧ OnRoot (cmpEq cmp x) t'
h : Ordered cmp t
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : RBNode.zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
ax : All (fun x => cmpLT cmp x x✝¹) a✝
xb : All (fun x => cmpLT cmp x✝¹ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hp : Path.Ordered cmp path
left✝ : Path.RootOrdered cmp path x✝¹
ap : All (Path.RootOrdered cmp path) a✝
bp : All (Path.RootOrdered cmp path) b✝
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
hf : f (some x✝¹) = some y✝
⊢ Ordered cmp (path.fill (node c✝ a✝ y✝ b✝))

Tactic:
have ⟨yp, xy⟩ := H eq hf

Result:
α : Type u_1
cut : α → Ordering
f : Option α → Option α
cmp : α → α → Ordering
t : RBNode α
H :
  ∀ {x : α} {t' : RBNode α} {p : Path α},
    RBNode.zoom cut t = (t', p) → f t'.root? = some x → Path.RootOrdered cmp p x ∧ OnRoot (cmpEq cmp x) t'
h : Ordered cmp t
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : RBNode.zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
ax : All (fun x => cmpLT cmp x x✝¹) a✝
xb : All (fun x => cmpLT cmp x✝¹ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hp : Path.Ordered cmp path
left✝ : Path.RootOrdered cmp path x✝¹
ap : All (Path.RootOrdered cmp path) a✝
bp : All (Path.RootOrdered cmp path) b✝
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
hf : f (some x✝¹) = some y✝
yp : Path.RootOrdered cmp path y✝
xy : OnRoot (cmpEq cmp y✝) (node c✝ a✝ x✝¹ b✝)
⊢ Ordered cmp (path.fill (node c✝ a✝ y✝ b✝))

Proof state:
α : Type u_1
cut : α → Ordering
f : Option α → Option α
cmp : α → α → Ordering
t : RBNode α
H :
  ∀ {x : α} {t' : RBNode α} {p : Path α},
    RBNode.zoom cut t = (t', p) → f t'.root? = some x → Path.RootOrdered cmp p x ∧ OnRoot (cmpEq cmp x) t'
h : Ordered cmp t
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : RBNode.zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
ax : All (fun x => cmpLT cmp x x✝¹) a✝
xb : All (fun x => cmpLT cmp x✝¹ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hp : Path.Ordered cmp path
left✝ : Path.RootOrdered cmp path x✝¹
ap : All (Path.RootOrdered cmp path) a✝
bp : All (Path.RootOrdered cmp path) b✝
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
hf : f (some x✝¹) = some y✝
yp : Path.RootOrdered cmp path y✝
xy : OnRoot (cmpEq cmp y✝) (node c✝ a✝ x✝¹ b✝)
⊢ Ordered cmp (path.fill (node c✝ a✝ y✝ b✝))

Tactic:
apply Path.Ordered.fill.2

Result:
α : Type u_1
cut : α → Ordering
f : Option α → Option α
cmp : α → α → Ordering
t : RBNode α
H :
  ∀ {x : α} {t' : RBNode α} {p : Path α},
    RBNode.zoom cut t = (t', p) → f t'.root? = some x → Path.RootOrdered cmp p x ∧ OnRoot (cmpEq cmp x) t'
h : Ordered cmp t
x✝² : RBNode α × Path α
c✝ : RBColor
a✝ : RBNode α
x✝¹ : α
b✝ : RBNode α
path : Path α
eq : RBNode.zoom cut t = (node c✝ a✝ x✝¹ b✝, path)
ax : All (fun x => cmpLT cmp x x✝¹) a✝
xb : All (fun x => cmpLT cmp x✝¹ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hp : Path.Ordered cmp path
left✝ : Path.RootOrdered cmp path x✝¹
ap : All (Path.RootOrdered cmp path) a✝
bp : All (Path.RootOrdered cmp path) b✝
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
hf : f (some x✝¹) = some y✝
yp : Path.RootOrdered cmp path y✝
xy : OnRoot (cmpEq cmp y✝) (node c✝ a✝ x✝¹ b✝)
⊢ Path.Ordered cmp path ∧ Ordered cmp (node c✝ a✝ y✝ b✝) ∧ All (Path.RootOrdered cmp path) (node c✝ a✝ y✝ b✝)