case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) PUnit.unit = ωSup (Chain.map x✝ (toUnitMono f)) PUnit.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) = ωSup (Chain.map x✝ (toUnitMono f))
ext ⟨⟩ : 1
case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑f (Part.ωSup (Chain.map x✝ (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map (Chain.map x✝ (toUnitMono f)) (Pi.evalOrderHom PUnit.unit))
case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑(toUnitMono f) (ωSup x✝) PUnit.unit = ωSup (Chain.map x✝ (toUnitMono f)) PUnit.unit
dsimp [OmegaCompletePartialOrder.ωSup]
case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit)))
case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ↑f (Part.ωSup (Chain.map x✝ (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map (Chain.map x✝ (toUnitMono f)) (Pi.evalOrderHom PUnit.unit))
erw [hc, Chain.map_comp]
no goals
case h.unit
α : Type u_1
β : α → Type ?u.16900
f : Part α →o Part α
hc : Continuous f
x✝ : Chain (Unit → Part α)
⊢ ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit))) =
    Part.ωSup (Chain.map x✝ (OrderHom.comp f (Pi.evalOrderHom PUnit.unit)))
rfl