case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ↑(monotoneUncurry α β γ) (ωSup c) { fst := x, snd := y } =
    ωSup (Chain.map c (monotoneUncurry α β γ)) { fst := x, snd := y }
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ ↑(monotoneUncurry α β γ) (ωSup c) = ωSup (Chain.map c (monotoneUncurry α β γ))
ext ⟨x, y⟩
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map (Chain.map c (evalOrderHom x)) (evalOrderHom y)) =
    ωSup (Chain.map (Chain.map c (monotoneUncurry α β γ)) (evalOrderHom { fst := x, snd := y }))
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ↑(monotoneUncurry α β γ) (ωSup c) { fst := x, snd := y } =
    ωSup (Chain.map c (monotoneUncurry α β γ)) { fst := x, snd := y }
dsimp [uncurry, ωSup]
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map c (OrderHom.comp (evalOrderHom y) (evalOrderHom x))) =
    ωSup (Chain.map c (OrderHom.comp (evalOrderHom { fst := x, snd := y }) (monotoneUncurry α β γ)))
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map (Chain.map c (evalOrderHom x)) (evalOrderHom y)) =
    ωSup (Chain.map (Chain.map c (monotoneUncurry α β γ)) (evalOrderHom { fst := x, snd := y }))
rw [map_comp, map_comp]
no goals
case h.mk
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (Chain.map c (OrderHom.comp (evalOrderHom y) (evalOrderHom x))) =
    ωSup (Chain.map c (OrderHom.comp (evalOrderHom { fst := x, snd := y }) (monotoneUncurry α β γ)))
rfl