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