α : Type u
α' : Type ?u.58987
β✝ : Type v
β' : Type ?u.58992
γ✝ : Type ?u.58995
φ : Type ?u.58998
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hf' : Continuous { toFun := f, monotone' := hf }
hg : Monotone g
hg' : Continuous { toFun := g, monotone' := hg }
c : Chain α
⊢ ↑(OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }) (ωSup c) =
    ωSup (Chain.map c (OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }))
α : Type u
α' : Type ?u.58987
β✝ : Type v
β' : Type ?u.58992
γ✝ : Type ?u.58995
φ : Type ?u.58998
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hf' : Continuous { toFun := f, monotone' := hf }
hg : Monotone g
hg' : Continuous { toFun := g, monotone' := hg }
⊢ Continuous (OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg })
intro c
α : Type u
α' : Type ?u.58987
β✝ : Type v
β' : Type ?u.58992
γ✝ : Type ?u.58995
φ : Type ?u.58998
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hf' : Continuous { toFun := f, monotone' := hf }
hg : Monotone g
hg' : Continuous { toFun := g, monotone' := hg }
c : Chain α
⊢ ↑(OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }) (ωSup c) =
    ↑{ toFun := f, monotone' := hf } (ωSup c) >>= ↑{ toFun := g, monotone' := hg } (ωSup c)
α : Type u
α' : Type ?u.58987
β✝ : Type v
β' : Type ?u.58992
γ✝ : Type ?u.58995
φ : Type ?u.58998
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hf' : Continuous { toFun := f, monotone' := hf }
hg : Monotone g
hg' : Continuous { toFun := g, monotone' := hg }
c : Chain α
⊢ ↑(OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }) (ωSup c) =
    ωSup (Chain.map c (OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }))
rw [ωSup_bind, ← hf', ← hg']
no goals
α : Type u
α' : Type ?u.58987
β✝ : Type v
β' : Type ?u.58992
γ✝ : Type ?u.58995
φ : Type ?u.58998
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hf' : Continuous { toFun := f, monotone' := hf }
hg : Monotone g
hg' : Continuous { toFun := g, monotone' := hg }
c : Chain α
⊢ ↑(OrderHom.bind { toFun := f, monotone' := hf } { toFun := g, monotone' := hg }) (ωSup c) =
    ↑{ toFun := f, monotone' := hf } (ωSup c) >>= ↑{ toFun := g, monotone' := hg } (ωSup c)
rfl