-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.fill : ∀ {path : Path α} {t},
    (path.fill t).Ordered cmp ↔ path.Ordered cmp ∧ t.Ordered cmp ∧ t.All (path.RootOrdered cmp)
  | .root, _ => ⟨fun H => ⟨⟨⟩, H, .trivial ⟨⟩⟩, (·.2.1)⟩
  | .left .., _ => by
    simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]
    exact ⟨
      fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩,
      fun ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩
  | .right .., _ => by
    simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]
    exact ⟨
      fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩,
      fun ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ RBNode.Ordered cmp ((right c✝ l✝ v✝ parent✝).fill x✝) ↔
    Ordered cmp (right c✝ l✝ v✝ parent✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (right c✝ l✝ v✝ parent✝)) x✝

Tactic:
simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) l✝ ∧
          All (fun x => cmpLT cmp v✝ x) x✝ ∧ RBNode.Ordered cmp l✝ ∧ RBNode.Ordered cmp x✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ All (RootOrdered cmp parent✝) x✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp x v✝) l✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (cmpLT cmp v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
parent✝ : Path α
x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) l✝ ∧
          All (fun x => cmpLT cmp v✝ x) x✝ ∧ RBNode.Ordered cmp l✝ ∧ RBNode.Ordered cmp x✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ All (RootOrdered cmp parent✝) x✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp x v✝) l✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (cmpLT cmp v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝

Tactic:
exact ⟨
  fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩,
  fun ⟨⟨hp, ax, xp, ap, ha⟩, hb, ⟨xb, bp⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) x✝ ∧
          All (fun x => cmpLT cmp v✝ x) r✝ ∧ RBNode.Ordered cmp x✝ ∧ RBNode.Ordered cmp r✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) x✝ ∧ All (RootOrdered cmp parent✝) r✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp v✝ x) r✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) r✝ ∧ RBNode.Ordered cmp r✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp x v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝

Tactic:
exact ⟨
  fun ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩ => ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩,
  fun ⟨⟨hp, xb, xp, bp, hb⟩, ha, ⟨ax, ap⟩⟩ => ⟨hp, ⟨ax, xb, ha, hb⟩, ⟨xp, ap, bp⟩⟩⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ RBNode.Ordered cmp ((left c✝ parent✝ v✝ r✝).fill x✝) ↔
    Ordered cmp (left c✝ parent✝ v✝ r✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (left c✝ parent✝ v✝ r✝)) x✝

Tactic:
simp [Ordered.fill, RBNode.Ordered, Ordered, RootOrdered, All_and]

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent✝ : Path α
v✝ : α
r✝ x✝ : RBNode α
⊢ Ordered cmp parent✝ ∧
      (All (fun x => cmpLT cmp x v✝) x✝ ∧
          All (fun x => cmpLT cmp v✝ x) r✝ ∧ RBNode.Ordered cmp x✝ ∧ RBNode.Ordered cmp r✝) ∧
        RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) x✝ ∧ All (RootOrdered cmp parent✝) r✝ ↔
    (Ordered cmp parent✝ ∧
        All (fun x => cmpLT cmp v✝ x) r✝ ∧
          RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) r✝ ∧ RBNode.Ordered cmp r✝) ∧
      RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp x v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝