-- 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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
left✝¹ : Ordered cmp nil
hp : Path.Ordered cmp path
left✝ : All (Path.RootOrdered cmp path) nil
right✝ : Path.Zoomed cut path
⊢ Ordered cmp
    (match f none with
    | none => t
    | some y => path.insertNew y)

Tactic:
split

Result:
case h_1
α : 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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
left✝¹ : Ordered cmp nil
hp : Path.Ordered cmp path
left✝ : All (Path.RootOrdered cmp path) nil
right✝ : Path.Zoomed cut path
x✝ : Option α
heq✝ : f none = none
⊢ Ordered cmp t

case h_2
α : 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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
left✝¹ : Ordered cmp nil
hp : Path.Ordered cmp path
left✝ : All (Path.RootOrdered cmp path) nil
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
heq✝ : f none = some y✝
⊢ Ordered cmp (path.insertNew y✝)

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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
left✝¹ : Ordered cmp nil
hp : Path.Ordered cmp path
left✝ : All (Path.RootOrdered cmp path) nil
right✝ : Path.Zoomed cut path
x✝ : Option α
y✝ : α
hf : f none = some y✝
⊢ Ordered cmp (path.insertNew y✝)

Tactic:
exact hp.insertNew (H eq hf).1

Result:
no goals

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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
⊢ Ordered cmp
    (match f none with
    | none => t
    | some y => path.insertNew y)

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

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 α
path : Path α
eq : RBNode.zoom cut t = (nil, path)
left✝¹ : Ordered cmp nil
hp : Path.Ordered cmp path
left✝ : All (Path.RootOrdered cmp path) nil
right✝ : Path.Zoomed cut path
⊢ Ordered cmp
    (match f none with
    | none => t
    | some y => path.insertNew y)

Proof state:
case h_1
α : 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 α
heq✝ : f (some x✝¹) = none
⊢ Ordered cmp (path.del (a✝.append b✝) c✝)

Tactic:
exact hp.del (ha.append ax xb hb) (ap.append bp)

Result:
no goals

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)
⊢ Ordered cmp
    (match f (some x✝) with
    | none => path.del (a✝.append b✝) c✝
    | some y => path.fill (node c✝ a✝ y b✝))

Tactic:
have ⟨⟨ax, xb, ha, hb⟩, hp, ⟨_, ap, bp⟩, _⟩ := h.zoom eq

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
⊢ Ordered cmp
    (match f (some x✝) with
    | none => path.del (a✝.append b✝) c✝
    | some y => 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
⊢ Ordered cmp (alter cut f t)

Tactic:
simp [alter]

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
⊢ Ordered cmp
    (match RBNode.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))