no goals
α : Type u
α' : Type ?u.73638
β : Type v
β' : Type ?u.73643
γ : Type ?u.73646
φ : Type ?u.73649
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
⊢ ↑(ωSup c₀).toOrderHom (ωSup c₁) = ↑Prod.apply.toOrderHom (ωSup (Chain.zip c₀ c₁))
simp [Prod.apply_apply, Prod.ωSup_zip]