-- 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:
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 α
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✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ Ordered cmp (path.fill (node c✝ a✝ y✝ b✝))

Tactic:
next hf =>
have ⟨yp, xy⟩ := H eq hf
apply Path.Ordered.fill.2
exact ⟨hp, ⟨ax.imp xy.lt_congr_right.2, xb.imp xy.lt_congr_left.2, ha, hb⟩, yp, ap, 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
⊢ 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))

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

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 α
c✝ : RBColor
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
path✝ : Path α
heq✝ : 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✝))

Proof state:
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✝)

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

Result:
no goals

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 α
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

Tactic:
exact h

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)
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✝)

Tactic:
exact ⟨hp, ⟨ax.imp xy.lt_congr_right.2, xb.imp xy.lt_congr_left.2, ha, hb⟩, yp, ap, 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)
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✝))

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 α
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✝)

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 α
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✝ : α
heq✝ : f (some x✝¹) = some y✝
⊢ Ordered cmp (path.fill (node c✝ a✝ y✝ b✝))