[GOAL]
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β✝
inst✝ : Preorder γ✝
β γ : Type ?u.55
f : α →o Part β
g : α →o β → Part γ
⊢ Monotone fun x => ↑f x >>= ↑g x
[PROOFSTEP]
intro x y h a
[GOAL]
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β✝
inst✝ : Preorder γ✝
β γ : Type ?u.55
f : α →o Part β
g : α →o β → Part γ
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x => ↑f x >>= ↑g x) x → a ∈ (fun x => ↑f x >>= ↑g x) y
[PROOFSTEP]
simp only [and_imp, exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, exists_imp]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β✝
inst✝ : Preorder γ✝
β γ : Type ?u.55
f : α →o Part β
g : α →o β → Part γ
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ ↑f x → a ∈ ↑g x x_1 → ∃ a_3, a_3 ∈ ↑f y ∧ a ∈ ↑g y a_3
[PROOFSTEP]
intro b hb ha
[GOAL]
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β✝
inst✝ : Preorder γ✝
β γ : Type ?u.55
f : α →o Part β
g : α →o β → Part γ
x y : α
h : x ≤ y
a : γ
b : β
hb : b ∈ ↑f x
ha : a ∈ ↑g x b
⊢ ∃ a_1, a_1 ∈ ↑f y ∧ a ∈ ↑g y a_1
[PROOFSTEP]
refine' ⟨b, f.monotone h _ hb, g.monotone h _ _ ha⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
b : β
h : ∃ a, a ∈ c ∧ ↑f a = b
⊢ b ∈ map c f
[PROOFSTEP]
rcases h with ⟨w, h, h'⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
b : β
w : α
h : w ∈ c
h' : ↑f w = b
⊢ b ∈ map c f
[PROOFSTEP]
subst b
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g : β →o γ
w : α
h : w ∈ c
⊢ ↑f w ∈ map c f
[PROOFSTEP]
apply mem_map c _ h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑(map c f) i ≤ ↑(map c g) j
[PROOFSTEP]
simp [mem_map_iff]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
[PROOFSTEP]
intros
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
[PROOFSTEP]
exists i
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ↑f (↑c i) ≤ ↑g (↑c i)
[PROOFSTEP]
apply h
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
i : ℕ
⊢ ↑f (↑c i) ≤ ↑f (ωSup₀ c)
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
i : ℕ
⊢ ↑f (↑c i) ≤ ωSup (Chain.map c f)
[PROOFSTEP]
apply le_ωSup (c.map f)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
x : β
hx : ∀ (i : ℕ), ↑c i ≤ x
⊢ ↑f (ωSup₀ c) ≤ ↑f x
[PROOFSTEP]
rw [h']
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
x : β
hx : ∀ (i : ℕ), ↑c i ≤ x
⊢ ωSup (Chain.map c f) ≤ ↑f x
[PROOFSTEP]
apply ωSup_le
[GOAL]
case a
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
x : β
hx : ∀ (i : ℕ), ↑c i ≤ x
⊢ ∀ (i : ℕ), ↑(Chain.map c f) i ≤ ↑f x
[PROOFSTEP]
intro i
[GOAL]
case a
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : PartialOrder β
f : β →o α
ωSup₀ : Chain β → β
h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y
h' : ∀ (c : Chain β), ↑f (ωSup₀ c) = ωSup (Chain.map c f)
c : Chain β
x : β
hx : ∀ (i : ℕ), ↑c i ≤ x
i : ℕ
⊢ ↑(Chain.map c f) i ≤ ↑f x
[PROOFSTEP]
apply f.monotone (hx i)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), ↑c i ≤ x ∨ x ≤ ↑c i
this : ¬∀ (i : ℕ), ↑c i ≤ x
⊢ ∃ i, ¬↑c i ≤ x
[PROOFSTEP]
simp only [not_forall] at this ⊢
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
h : ∀ (i : ℕ), ↑c i ≤ x ∨ x ≤ ↑c i
this : ∃ x_1, ¬↑c x_1 ≤ x
⊢ ∃ i, ¬↑c i ≤ x
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h : c₀ ≤ c₁
i : ℕ
⊢ ↑c₀ i ≤ ωSup c₁
[PROOFSTEP]
obtain ⟨_, h⟩ := h i
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c₀ c₁ : Chain α
h✝ : c₀ ≤ c₁
i w✝ : ℕ
h : ↑c₀ i ≤ ↑c₁ w✝
⊢ ↑c₀ i ≤ ωSup c₁
[PROOFSTEP]
exact le_trans h (le_ωSup _ _)
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), ↑c i ≤ x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x → ∀ (i : ℕ), ↑c i ≤ x
[PROOFSTEP]
intros
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ (∀ (i : ℕ), ↑c i ≤ x) → ωSup c ≤ x
[PROOFSTEP]
intros
[GOAL]
case mp
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ x
[PROOFSTEP]
trans ωSup c
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ ωSup c
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
[PROOFSTEP]
exact le_ωSup _ _
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
[PROOFSTEP]
assumption
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), ↑c i ≤ x
⊢ ωSup c ≤ x
[PROOFSTEP]
exact ωSup_le _ _ ‹_›
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
⊢ Continuous OrderHom.id
[PROOFSTEP]
intro c
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup (map c OrderHom.id)
[PROOFSTEP]
rw [c.map_id]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup c
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
hfc : Continuous f
hgc : Continuous g
⊢ Continuous (OrderHom.comp g f)
[PROOFSTEP]
dsimp [Continuous] at *
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
hfc : ∀ (c : Chain α), ↑f (ωSup c) = ωSup (map c f)
hgc : ∀ (c : Chain β), ↑g (ωSup c) = ωSup (map c g)
⊢ ∀ (c : Chain α), ↑g (↑f (ωSup c)) = ωSup (map c (OrderHom.comp g f))
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
hfc : ∀ (c : Chain α), ↑f (ωSup c) = ωSup (map c f)
hgc : ∀ (c : Chain β), ↑g (ωSup c) = ωSup (map c g)
c✝ : Chain α
⊢ ↑g (↑f (ωSup c✝)) = ωSup (map c✝ (OrderHom.comp g f))
[PROOFSTEP]
rw [hfc, hgc, Chain.map_comp]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
x : β
c : Chain α
z : β
⊢ ↑(↑(OrderHom.const α) x) (ωSup c) ≤ z ↔ ωSup (map c (↑(OrderHom.const α) x)) ≤ z
[PROOFSTEP]
rw [ωSup_le_iff, Chain.map_coe, OrderHom.const_coe_coe]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
x : β
c : Chain α
z : β
⊢ Function.const α x (ωSup c) ≤ z ↔ ∀ (i : ℕ), (Function.const α x ∘ ↑c) i ≤ z
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
ha : some a ∈ c
hb : some b ∈ c
⊢ a = b
[PROOFSTEP]
cases' ha with i ha
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : some a = ↑c i
⊢ a = b
[PROOFSTEP]
replace ha := ha.symm
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
hb : some b ∈ c
i : ℕ
ha : ↑c i = some a
⊢ a = b
[PROOFSTEP]
cases' hb with j hb
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : some b = ↑c j
⊢ a = b
[PROOFSTEP]
replace hb := hb.symm
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : ↑c i = some a
j : ℕ
hb : ↑c j = some b
⊢ a = b
[PROOFSTEP]
rw [eq_some_iff] at ha hb 
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
⊢ a = b
[PROOFSTEP]
cases' le_total i j with hij hji
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
⊢ a = b
[PROOFSTEP]
have := c.monotone hij _ ha
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hij : i ≤ j
this : a ∈ ↑c j
⊢ a = b
[PROOFSTEP]
apply mem_unique this hb
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
⊢ a = b
[PROOFSTEP]
have := c.monotone hji _ hb
[GOAL]
case intro.intro.inr
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ a = b
[PROOFSTEP]
apply Eq.symm
[GOAL]
case intro.intro.inr.h
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ ↑c i
j : ℕ
hb : b ∈ ↑c j
hji : j ≤ i
this : b ∈ ↑c i
⊢ b = a
[PROOFSTEP]
apply mem_unique this ha
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h : a ∈ Part.ωSup c
⊢ some a ∈ c
[PROOFSTEP]
simp only [Part.ωSup] at h 
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h : a ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
⊢ some a ∈ c
[PROOFSTEP]
split_ifs at h  with h_1
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (choose h_1)
⊢ some a ∈ c
[PROOFSTEP]
have h' := Classical.choose_spec h_1
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (choose h_1)
h' : some (choose h_1) ∈ c
⊢ some a ∈ c
[PROOFSTEP]
rw [← eq_some_iff] at h 
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (choose h_1) = some a
h' : some (choose h_1) ∈ c
⊢ some a ∈ c
[PROOFSTEP]
rw [← h]
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (choose h_1) = some a
h' : some (choose h_1) ∈ c
⊢ some (choose h_1) ∈ c
[PROOFSTEP]
exact h'
[GOAL]
case neg
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c
[PROOFSTEP]
rcases h with ⟨⟨⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
i : ℕ
⊢ ↑c i ≤ Part.ωSup c
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
i : ℕ
x : α
hx : x ∈ ↑c i
⊢ x ∈ Part.ωSup c
[PROOFSTEP]
rw [← eq_some_iff] at hx ⊢
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
i : ℕ
x : α
hx : ↑c i = some x
⊢ Part.ωSup c = some x
[PROOFSTEP]
rw [ωSup_eq_some, ← hx]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
i : ℕ
x : α
hx : ↑c i = some x
⊢ some x ∈ c
[PROOFSTEP]
rw [← hx]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
i : ℕ
x : α
hx : ↑c i = some x
⊢ ↑c i ∈ c
[PROOFSTEP]
exact ⟨i, rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type u_1
⊢ ∀ (c : Chain (Part α)) (x : Part α), (∀ (i : ℕ), ↑c i ≤ x) → Part.ωSup c ≤ x
[PROOFSTEP]
rintro c x hx a ha
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), ↑c i ≤ x
a : α
ha : a ∈ Part.ωSup c
⊢ a ∈ x
[PROOFSTEP]
replace ha := mem_chain_of_mem_ωSup ha
[GOAL]
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), ↑c i ≤ x
a : α
ha : some a ∈ c
⊢ a ∈ x
[PROOFSTEP]
cases' ha with i ha
[GOAL]
case intro
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), ↑c i ≤ x
a : α
i : ℕ
ha : some a = ↑c i
⊢ a ∈ x
[PROOFSTEP]
apply hx i
[GOAL]
case intro.a
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), ↑c i ≤ x
a : α
i : ℕ
ha : some a = ↑c i
⊢ a ∈ ↑c i
[PROOFSTEP]
rw [← ha]
[GOAL]
case intro.a
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), ↑c i ≤ x
a : α
i : ℕ
ha : some a = ↑c i
⊢ a ∈ some a
[PROOFSTEP]
apply mem_some
[GOAL]
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
⊢ x ∈ ωSup c ↔ some x ∈ c
[PROOFSTEP]
simp [OmegaCompletePartialOrder.ωSup, Part.ωSup]
[GOAL]
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) ↔ some x ∈ c
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
⊢ (x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none) → some x ∈ c
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
case neg α : Type u β : Type v γ : Type u_1 x : α c : Chain (Part α) h : ¬∃ a, some a ∈ c ⊢ x ∈ none → some x ∈ c
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ¬∃ a, some a ∈ c
⊢ x ∈ none → some x ∈ c
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
⊢ x ∈ some (choose h) → some x ∈ c
[PROOFSTEP]
intro h'
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
⊢ some x ∈ c
[PROOFSTEP]
have hh := Classical.choose_spec h
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
h' : x ∈ some (choose h)
hh : some (choose h) ∈ c
⊢ some x ∈ c
[PROOFSTEP]
simp only [mem_some_iff] at h' 
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
h' : x = choose h
⊢ some x ∈ c
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u
β : Type v
γ : Type u_1
c : Chain (Part α)
h : ∃ a, some a ∈ c
hh : some (choose h) ∈ c
⊢ some (choose h) ∈ c
[PROOFSTEP]
exact hh
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
⊢ some x ∈ c → x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : some x ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
[PROOFSTEP]
have h' : ∃ a : α, some a ∈ c := ⟨_, h⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ if h : ∃ a, some a ∈ c then some (choose h) else none
[PROOFSTEP]
rw [dif_pos h']
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
⊢ x ∈ some (choose h')
[PROOFSTEP]
have hh := Classical.choose_spec h'
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some (choose h')
[PROOFSTEP]
rw [eq_of_chain hh h]
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type u_1
x : α
c : Chain (Part α)
h : some x ∈ c
h' : ∃ a, some a ∈ c
hh : some (choose h') ∈ c
⊢ x ∈ some x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
c : Chain ((a : α) → β a)
f : (a : α) → β a
hf : ∀ (i : ℕ), ↑c i ≤ f
a : α
⊢ ∀ (i : ℕ), ↑(map c (evalOrderHom a)) i ≤ f a
[PROOFSTEP]
rintro i
[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
c : Chain ((a : α) → β a)
f : (a : α) → β a
hf : ∀ (i : ℕ), ↑c i ≤ f
a : α
i : ℕ
⊢ ↑(map c (evalOrderHom a)) i ≤ f a
[PROOFSTEP]
apply hf
[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
⊢ Continuous { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) }
[PROOFSTEP]
intro c
[GOAL]
α : Type u_1
β : α → Type u_2
γ : Type u_3
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c) =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : α → Type u_2
γ : Type u_3
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
a : α
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c)
      a =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
      a
[PROOFSTEP]
apply (hf a).to_bundled _ c
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
⊢ ωSup (Chain.zip c₀ c₁) = (ωSup c₀, ωSup c₁)
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
⊢ ∀ (c : α × β), ωSup (Chain.zip c₀ c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c
[PROOFSTEP]
rintro ⟨z₁, z₂⟩
[GOAL]
case H.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
c₀ : Chain α
c₁ : Chain β
z₁ : α
z₂ : β
⊢ ωSup (Chain.zip c₀ c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)
[PROOFSTEP]
simp [ωSup_le_iff, forall_and]
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
i : ℕ
c : ℕ → α
monotone'✝ : Monotone c
⊢ ↑{ toFun := c, monotone' := monotone'✝ } i ≤ (fun c => ⨆ (i : ℕ), ↑c i) { toFun := c, monotone' := monotone'✝ }
[PROOFSTEP]
simp only [OrderHom.coe_mk]
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
i : ℕ
c : ℕ → α
monotone'✝ : Monotone c
⊢ ↑{ toFun := c, monotone' := monotone'✝ } i ≤ ⨆ (i : ℕ), ↑{ toFun := c, monotone' := monotone'✝ } i
[PROOFSTEP]
apply le_iSup_of_le i
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
i : ℕ
c : ℕ → α
monotone'✝ : Monotone c
⊢ ↑{ toFun := c, monotone' := monotone'✝ } i ≤ ↑{ toFun := c, monotone' := monotone'✝ } i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
s : α
c : ℕ → α
monotone'✝ : Monotone c
hs : ∀ (i : ℕ), ↑{ toFun := c, monotone' := monotone'✝ } i ≤ s
⊢ (fun c => ⨆ (i : ℕ), ↑c i) { toFun := c, monotone' := monotone'✝ } ≤ s
[PROOFSTEP]
simp only [iSup_le_iff, OrderHom.coe_mk] at hs ⊢
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
s : α
c : ℕ → α
monotone'✝ : Monotone c
hs : ∀ (i : ℕ), ↑{ toFun := c, monotone' := monotone'✝ } i ≤ s
⊢ ∀ (i : ℕ), ↑{ toFun := c, monotone' := monotone'✝ } i ≤ s
[PROOFSTEP]
intro i
[GOAL]
α : Type u
inst✝ : CompleteLattice α
x✝ : Chain α
s : α
c : ℕ → α
monotone'✝ : Monotone c
hs : ∀ (i : ℕ), ↑{ toFun := c, monotone' := monotone'✝ } i ≤ s
i : ℕ
⊢ ↑{ toFun := c, monotone' := monotone'✝ } i ≤ s
[PROOFSTEP]
apply hs i
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
⊢ Continuous (sSup s)
[PROOFSTEP]
intro c
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ↑(sSup s) (ωSup c) = ωSup (Chain.map c (sSup s))
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ∀ (c_1 : β), ↑(sSup s) (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c (sSup s)) ≤ c_1
[PROOFSTEP]
intro z
[GOAL]
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ ↑(sSup s) (ωSup c) ≤ z ↔ ωSup (Chain.map c (sSup s)) ≤ z
[PROOFSTEP]
suffices (∀ f ∈ s, ∀ (n), (f : _) (c n) ≤ z) ↔ ∀ (n), ∀ f ∈ s, (f : _) (c n) ≤ z by
  simpa (config := { contextual := true }) [ωSup_le_iff, hs _ _ _] using this
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
this : (∀ (f : α →o β), f ∈ s → ∀ (n : ℕ), ↑f (↑c n) ≤ z) ↔ ∀ (n : ℕ) (f : α →o β), f ∈ s → ↑f (↑c n) ≤ z
⊢ ↑(sSup s) (ωSup c) ≤ z ↔ ωSup (Chain.map c (sSup s)) ≤ z
[PROOFSTEP]
simpa (config := { contextual := true }) [ωSup_le_iff, hs _ _ _] using this
[GOAL]
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ (∀ (f : α →o β), f ∈ s → ∀ (n : ℕ), ↑f (↑c n) ≤ z) ↔ ∀ (n : ℕ) (f : α →o β), f ∈ s → ↑f (↑c n) ≤ z
[PROOFSTEP]
exact ⟨fun H n f hf => H f hf n, fun H f hf n => H n f hf⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hc : ∀ (f : α → β), f ∈ s → Continuous' f
⊢ Continuous' (sSup s)
[PROOFSTEP]
lift s to Set (α →o β) using fun f hf => (hc f hf).to_monotone
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (f : α → β), f ∈ (fun x x_1 => x '' x_1) FunLike.coe s → Continuous' f
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) FunLike.coe s))
[PROOFSTEP]
simp only [Set.ball_image_iff, continuous'_coe] at hc 
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (sSup ((fun x x_1 => x '' x_1) FunLike.coe s))
[PROOFSTEP]
rw [sSup_image]
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous' (⨆ (a : α →o β) (_ : a ∈ s), ↑a)
[PROOFSTEP]
norm_cast
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hc : ∀ (x : α →o β), x ∈ s → Continuous x
⊢ Continuous (⨆ (i : α →o β) (_ : i ∈ s), i)
[PROOFSTEP]
exact iSup_continuous fun f => iSup_continuous fun hf => hc f hf
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (f ⊔ g)
[PROOFSTEP]
rw [← sSup_pair]
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (sSup {f, g})
[PROOFSTEP]
apply sSup_continuous
[GOAL]
case hs
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ ∀ (f_1 : α →o β), f_1 ∈ {f, g} → Continuous f_1
[PROOFSTEP]
rintro f (rfl | rfl | _)
[GOAL]
case hs.inl
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
g : α →o β
hg : Continuous g
f : α →o β
hf : Continuous f
⊢ Continuous f
[PROOFSTEP]
assumption
[GOAL]
case hs.inr.refl
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous g
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ Continuous ⊤
[PROOFSTEP]
intro c
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ↑⊤ (ωSup c) = ωSup (Chain.map c ⊤)
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ∀ (c_1 : β), ↑⊤ (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c ⊤) ≤ c_1
[PROOFSTEP]
intro z
[GOAL]
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
z : β
⊢ ↑⊤ (ωSup c) ≤ z ↔ ωSup (Chain.map c ⊤) ≤ z
[PROOFSTEP]
simp only [OrderHom.instTopOrderHom_top, OrderHom.const_coe_coe, Function.const, top_le_iff, ωSup_le_iff, Chain.map_coe,
  Function.comp, forall_const]
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ Continuous ⊥
[PROOFSTEP]
rw [← sSup_empty]
[GOAL]
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ Continuous (sSup ∅)
[PROOFSTEP]
exact sSup_continuous _ fun f hf => hf.elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (f ⊓ g)
[PROOFSTEP]
refine' fun c => eq_of_forall_ge_iff fun z => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ ↑(f ⊓ g) (ωSup c) ≤ z ↔ ωSup (Chain.map c (f ⊓ g)) ≤ z
[PROOFSTEP]
simp only [inf_le_iff, hf c, hg c, ωSup_le_iff, ← forall_or_left, ← forall_or_right, Chain.map_coe, OrderHom.coe_inf,
  ge_iff_le, Pi.inf_apply, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ (∀ (x x_1 : ℕ), ↑f (↑c x_1) ≤ z ∨ ↑g (↑c x) ≤ z) ↔ ∀ (i : ℕ), ↑f (↑c i) ≤ z ∨ ↑g (↑c i) ≤ z
[PROOFSTEP]
exact
  ⟨λ h _ => h _ _, λ h i j =>
    (h (max j i)).imp (le_trans $ f.mono $ c.mono $ le_max_left _ _) (le_trans $ g.mono $ c.mono $ le_max_right _ _)⟩
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : Continuous toOrderHom✝¹
toOrderHom✝ : α →o β
cont✝ : Continuous toOrderHom✝
h :
  (fun f => f.toFun) { toOrderHom := toOrderHom✝¹, cont := cont✝¹ } =
    (fun f => f.toFun) { toOrderHom := toOrderHom✝, cont := cont✝ }
⊢ { toOrderHom := toOrderHom✝¹, cont := cont✝¹ } = { toOrderHom := toOrderHom✝, cont := cont✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toOrderHom
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toOrderHom✝¹ : α →o β
cont✝¹ : Continuous toOrderHom✝¹
toOrderHom✝ : α →o β
cont✝ : Continuous toOrderHom✝
h :
  (fun f => f.toFun) { toOrderHom := toOrderHom✝¹, cont := cont✝¹ } =
    (fun f => f.toFun) { toOrderHom := toOrderHom✝, cont := cont✝ }
⊢ toOrderHom✝¹ = toOrderHom✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
⊢ Function.Injective fun f => f.toFun
[PROOFSTEP]
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩ h
[GOAL]
case mk.mk.mk.mk
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
cont✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
cont✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }
h :
  (fun f => f.toFun) { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, cont := cont✝¹ } =
    (fun f => f.toFun) { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, cont := cont✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, cont := cont✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, cont := cont✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
p : Prop
hp : Decidable p
f g : α → β
hf : Continuous' f
hg : Continuous' g
⊢ Continuous' fun x => if p then f x else g x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
p : Prop
hp : Decidable p
f g : α → β
hf : Continuous' f
hg : Continuous' g
h✝ : p
⊢ Continuous' fun x => f x
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
p : Prop
hp : Decidable p
f g : α → β
hf : Continuous' f
hg : Continuous' g
h✝ : ¬p
⊢ Continuous' fun x => g x
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ωSup (Chain.map c (OrderHom.bind f g)) = ωSup (Chain.map c f) >>= ωSup (Chain.map c g)
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ∀ (c_1 : Part γ), ωSup (Chain.map c (OrderHom.bind f g)) ≤ c_1 ↔ ωSup (Chain.map c f) >>= ωSup (Chain.map c g) ≤ c_1
[PROOFSTEP]
intro x
[GOAL]
case H
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ ωSup (Chain.map c (OrderHom.bind f g)) ≤ x ↔ ωSup (Chain.map c f) >>= ωSup (Chain.map c g) ≤ x
[PROOFSTEP]
simp only [ωSup_le_iff, Part.bind_le, Chain.mem_map_iff, and_imp, OrderHom.bind_coe, exists_imp]
[GOAL]
case H
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x) ↔
    ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
[PROOFSTEP]
constructor
[GOAL]
case H.mp
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x) →
    ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
[PROOFSTEP]
intro h'''
[GOAL]
case H.mpr
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x) →
    ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
[PROOFSTEP]
intro h'''
[GOAL]
case H.mp
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
⊢ ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
[PROOFSTEP]
intro b hb
[GOAL]
case H.mp
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
hb : b ∈ ωSup (Chain.map c f)
⊢ ωSup (Chain.map c g) b ≤ x
[PROOFSTEP]
apply ωSup_le _ _ _
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
hb : b ∈ ωSup (Chain.map c f)
⊢ ∀ (i : ℕ), ↑(Chain.map (Chain.map c g) (Pi.evalOrderHom b)) i ≤ x
[PROOFSTEP]
rintro i y hy
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
hb : b ∈ ωSup (Chain.map c f)
i : ℕ
y : γ
hy : y ∈ ↑(Chain.map (Chain.map c g) (Pi.evalOrderHom b)) i
⊢ y ∈ x
[PROOFSTEP]
simp only [Part.mem_ωSup] at hb 
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ↑(Chain.map (Chain.map c g) (Pi.evalOrderHom b)) i
hb : Part.some b ∈ Chain.map c f
⊢ y ∈ x
[PROOFSTEP]
rcases hb with ⟨j, hb⟩
[GOAL]
case intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ↑(Chain.map (Chain.map c g) (Pi.evalOrderHom b)) i
j : ℕ
hb : Part.some b = ↑(Chain.map c f) j
⊢ y ∈ x
[PROOFSTEP]
replace hb := hb.symm
[GOAL]
case intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ↑(Chain.map (Chain.map c g) (Pi.evalOrderHom b)) i
j : ℕ
hb : ↑(Chain.map c f) j = Part.some b
⊢ y ∈ x
[PROOFSTEP]
simp only [Part.eq_some_iff, Chain.map_coe, Function.comp_apply, OrderHom.apply_coe] at hy hb 
[GOAL]
case intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ↑(Pi.evalOrderHom b) (↑g (↑c i))
j : ℕ
hb : b ∈ ↑(Chain.map c f) j
⊢ y ∈ x
[PROOFSTEP]
replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
[GOAL]
case intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ↑(Pi.evalOrderHom b) (↑g (↑c i))
j : ℕ
hb : b ∈ ↑f (↑c (max i j))
⊢ y ∈ x
[PROOFSTEP]
replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
[GOAL]
case intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ ↑f (↑c (max i j))
hy : y ∈ ↑g (↑c (max i j)) b
⊢ y ∈ x
[PROOFSTEP]
apply h''' (max i j)
[GOAL]
case intro.a
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ ↑f (↑c (max i j))
hy : y ∈ ↑g (↑c (max i j)) b
⊢ y ∈ ↑(Chain.map c (OrderHom.bind f g)) (max i j)
[PROOFSTEP]
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe, Function.comp_apply, OrderHom.bind_coe]
[GOAL]
case intro.a
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ ↑f (↑c (max i j))
hy : y ∈ ↑g (↑c (max i j)) b
⊢ ∃ a, a ∈ ↑f (↑c (max i j)) ∧ y ∈ ↑g (↑c (max i j)) a
[PROOFSTEP]
exact ⟨_, hb, hy⟩
[GOAL]
case H.mpr
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
⊢ ∀ (i : ℕ), ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
[PROOFSTEP]
intro i
[GOAL]
case H.mpr
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
⊢ ↑(Chain.map c (OrderHom.bind f g)) i ≤ x
[PROOFSTEP]
intro y hy
[GOAL]
case H.mpr
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
y : γ
hy : y ∈ ↑(Chain.map c (OrderHom.bind f g)) i
⊢ y ∈ x
[PROOFSTEP]
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe, Function.comp_apply, OrderHom.bind_coe] at
  hy 
[GOAL]
case H.mpr
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
y : γ
hy : ∃ a, a ∈ ↑f (↑c i) ∧ y ∈ ↑g (↑c i) a
⊢ y ∈ x
[PROOFSTEP]
rcases hy with ⟨b, hb₀, hb₁⟩
[GOAL]
case H.mpr.intro.intro
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ ↑f (↑c i)
hb₁ : y ∈ ↑g (↑c i) b
⊢ y ∈ x
[PROOFSTEP]
apply h''' b _
[GOAL]
case H.mpr.intro.intro.a
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ ↑f (↑c i)
hb₁ : y ∈ ↑g (↑c i) b
⊢ y ∈ ωSup (Chain.map c g) b
[PROOFSTEP]
apply le_ωSup (c.map g) _ _ _ hb₁
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (a : β), a ∈ ωSup (Chain.map c f) → ωSup (Chain.map c g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ ↑f (↑c i)
hb₁ : y ∈ ↑g (↑c i) b
⊢ b ∈ ωSup (Chain.map c f)
[PROOFSTEP]
apply le_ωSup (c.map f) i _ hb₀
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
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 })
[PROOFSTEP]
intro c
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
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 }))
[PROOFSTEP]
rw [ωSup_bind, ← hf', ← hg']
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
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)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => f <$> g x
[PROOFSTEP]
simp only [map_eq_bind_pure_comp]
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => g x >>= pure ∘ f
[PROOFSTEP]
apply bind_continuous' _ _ hg
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α → Part β
hg : Continuous' g
⊢ Continuous' fun x => pure ∘ f
[PROOFSTEP]
apply const_continuous'
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part (β → γ)
g : α → Part β
hf : Continuous' f
hg : Continuous' g
⊢ Continuous' fun x => Seq.seq (f x) fun x_1 => g x
[PROOFSTEP]
simp only [seq_eq_bind_map]
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part (β → γ)
g : α → Part β
hf : Continuous' f
hg : Continuous' g
⊢ Continuous' fun x => do
    let x_1 ← f x
    x_1 <$> g x
[PROOFSTEP]
apply bind_continuous' _ _ hf
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part (β → γ)
g : α → Part β
hf : Continuous' f
hg : Continuous' g
⊢ Continuous' fun x x_1 => x_1 <$> g x
[PROOFSTEP]
apply Pi.OmegaCompletePartialOrder.flip₂_continuous'
[GOAL]
case hf
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part (β → γ)
g : α → Part β
hf : Continuous' f
hg : Continuous' g
⊢ ∀ (x : β → γ), Continuous' fun g_1 => x <$> g g_1
[PROOFSTEP]
intro
[GOAL]
case hf
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α → Part (β → γ)
g : α → Part β
hf : Continuous' f
hg : Continuous' g
x✝ : β → γ
⊢ Continuous' fun g_1 => x✝ <$> g g_1
[PROOFSTEP]
apply map_continuous' _ _ hg
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f : α → β
g : α →𝒄 β
h : f = ↑g
⊢ Continuous (OrderHom.copy g.toOrderHom f h)
[PROOFSTEP]
rw [OrderHom.copy_eq]
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
f : α → β
g : α →𝒄 β
h : f = ↑g
⊢ Continuous g.toOrderHom
[PROOFSTEP]
exact g.cont
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z) ↔ ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i j : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z) → ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
[PROOFSTEP]
introv h
[GOAL]
case mpr
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z) → ∀ (i j : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z
[PROOFSTEP]
introv h
[GOAL]
case mp
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i j : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z
i : ℕ
⊢ ↑(↑c₀ i) (↑c₁ i) ≤ z
[PROOFSTEP]
apply h
[GOAL]
case mpr
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ ↑(↑c₀ i) (↑c₁ j) ≤ z
[PROOFSTEP]
apply le_trans _ (h (max i j))
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ ↑(↑c₀ i) (↑c₁ j) ≤ ↑(↑c₀ (max i j)) (↑c₁ (max i j))
[PROOFSTEP]
trans c₀ i (c₁ (max i j))
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ ↑(↑c₀ i) (↑c₁ j) ≤ ↑(↑c₀ i) (↑c₁ (max i j))
[PROOFSTEP]
apply (c₀ i).monotone
[GOAL]
case a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ ↑c₁ j ≤ ↑c₁ (max i j)
[PROOFSTEP]
apply c₁.monotone
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ j ≤ max i j
[PROOFSTEP]
apply le_max_right
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ ↑(↑c₀ i) (↑c₁ (max i j)) ≤ ↑(↑c₀ (max i j)) (↑c₁ (max i j))
[PROOFSTEP]
apply c₀.monotone
[GOAL]
case a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
i j : ℕ
⊢ i ≤ max i j
[PROOFSTEP]
apply le_max_left
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
⊢ (∀ (j i : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z) ↔ ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z
[PROOFSTEP]
rw [forall_swap, forall_forall_merge]
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain (α →𝒄 β)
c' : Chain α
⊢ ↑(ωSup (Chain.map c toMono)) (ωSup c') = ωSup (Chain.map c' (ωSup (Chain.map c toMono)))
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain (α →𝒄 β)
c' : Chain α
⊢ ∀ (c_1 : β), ↑(ωSup (Chain.map c toMono)) (ωSup c') ≤ c_1 ↔ ωSup (Chain.map c' (ωSup (Chain.map c toMono))) ≤ c_1
[PROOFSTEP]
intro z
[GOAL]
case H
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain (α →𝒄 β)
c' : Chain α
z : β
⊢ ↑(ωSup (Chain.map c toMono)) (ωSup c') ≤ z ↔ ωSup (Chain.map c' (ωSup (Chain.map c toMono))) ≤ z
[PROOFSTEP]
simp only [ωSup_le_iff, (c _).continuous, Chain.map_coe, OrderHom.apply_coe, toMono_coe,
  OrderHom.omegaCompletePartialOrder_ωSup_coe, forall_forall_merge, OrderHomClass.coe_coe, forall_forall_merge',
  (· ∘ ·), Function.eval]
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
x y : (α →𝒄 β) × α
h : x ≤ y
⊢ (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y
[PROOFSTEP]
dsimp
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
x y : (α →𝒄 β) × α
h : x ≤ y
⊢ ↑x.fst x.snd ≤ ↑y.fst y.snd
[PROOFSTEP]
trans y.fst x.snd <;> [apply h.1; apply y.1.monotone h.2]
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
x y : (α →𝒄 β) × α
h : x ≤ y
⊢ ↑x.fst x.snd ≤ ↑y.fst y.snd
[PROOFSTEP]
trans y.fst x.snd
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
x y : (α →𝒄 β) × α
h : x ≤ y
⊢ ↑x.fst x.snd ≤ ↑y.fst x.snd
[PROOFSTEP]
apply h.1
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
x y : (α →𝒄 β) × α
h : x ≤ y
⊢ ↑y.fst x.snd ≤ ↑y.fst y.snd
[PROOFSTEP]
apply y.1.monotone h.2
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
⊢ Continuous
    { toFun := fun f => ↑f.fst f.snd,
      monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
[PROOFSTEP]
intro c
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
⊢ ↑{ toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
      (ωSup c) =
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
⊢ ↑{ toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
      (ωSup c) ≤
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
[PROOFSTEP]
apply ωSup_le
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
⊢ ∀ (i : ℕ),
    ↑(Chain.map (Chain.map (Chain.map c OrderHom.fst) toMono) (OrderHom.apply (ωSup c).snd)) i ≤
      ωSup
        (Chain.map c
          { toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
[PROOFSTEP]
intro i
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ↑(Chain.map (Chain.map (Chain.map c OrderHom.fst) toMono) (OrderHom.apply (ωSup c).snd)) i ≤
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
[PROOFSTEP]
dsimp
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ↑(↑c i).fst (ωSup (Chain.map c OrderHom.snd)) ≤
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → ↑x.fst x.snd ≤ ↑y.fst y.snd) })
[PROOFSTEP]
rw [(c _).fst.continuous]
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ωSup (Chain.map (Chain.map c OrderHom.snd) ↑(↑c i).fst) ≤
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → ↑x.fst x.snd ≤ ↑y.fst y.snd) })
[PROOFSTEP]
apply ωSup_le
[GOAL]
case a.a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ∀ (i_1 : ℕ),
    ↑(Chain.map (Chain.map c OrderHom.snd) ↑(↑c i).fst) i_1 ≤
      ωSup
        (Chain.map c
          { toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → ↑x.fst x.snd ≤ ↑y.fst y.snd) })
[PROOFSTEP]
intro j
[GOAL]
case a.a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i j : ℕ
⊢ ↑(Chain.map (Chain.map c OrderHom.snd) ↑(↑c i).fst) j ≤
    ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → ↑x.fst x.snd ≤ ↑y.fst y.snd) })
[PROOFSTEP]
apply le_ωSup_of_le (max i j)
[GOAL]
case a.a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i j : ℕ
⊢ ↑(Chain.map (Chain.map c OrderHom.snd) ↑(↑c i).fst) j ≤
    ↑(Chain.map c
          { toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → ↑x.fst x.snd ≤ ↑y.fst y.snd) })
      (max i j)
[PROOFSTEP]
apply apply_mono
[GOAL]
case a.a.a.h₁
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i j : ℕ
⊢ (↑c i).fst ≤ (↑c (max i j)).fst
case a.a.a.h₂
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i j : ℕ
⊢ ↑(Chain.map c OrderHom.snd) j ≤ (↑c (max i j)).snd
[PROOFSTEP]
exact monotone_fst (OrderHom.mono _ (le_max_left _ _))
[GOAL]
case a.a.a.h₂
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i j : ℕ
⊢ ↑(Chain.map c OrderHom.snd) j ≤ (↑c (max i j)).snd
[PROOFSTEP]
exact monotone_snd (OrderHom.mono _ (le_max_right _ _))
[GOAL]
case a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
⊢ ωSup
      (Chain.map c
        { toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }) ≤
    ↑{ toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
      (ωSup c)
[PROOFSTEP]
apply ωSup_le
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
⊢ ∀ (i : ℕ),
    ↑(Chain.map c
            { toFun := fun f => ↑f.fst f.snd,
              monotone' :=
                (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
        i ≤
      ↑{ toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
        (ωSup c)
[PROOFSTEP]
intro i
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ↑(Chain.map c
          { toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
      i ≤
    ↑{ toFun := fun f => ↑f.fst f.snd,
          monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) }
      (ωSup c)
[PROOFSTEP]
apply le_ωSup_of_le i
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ↑(Chain.map c
          { toFun := fun f => ↑f.fst f.snd,
            monotone' := (_ : ∀ (x y : (α →𝒄 β) × α), x ≤ y → (fun f => ↑f.fst f.snd) x ≤ (fun f => ↑f.fst f.snd) y) })
      i ≤
    ↑(Chain.map (Chain.map (Chain.map c OrderHom.fst) toMono) (OrderHom.apply (ωSup c).snd)) i
[PROOFSTEP]
dsimp
[GOAL]
case a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ ↑(↑c i).fst (↑c i).snd ≤ ↑(↑c i).fst (ωSup (Chain.map c OrderHom.snd))
[PROOFSTEP]
apply OrderHom.mono _
[GOAL]
case a.a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ (↑c i).snd ≤ ωSup (Chain.map c OrderHom.snd)
[PROOFSTEP]
apply le_ωSup_of_le i
[GOAL]
case a.a.a
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c : Chain ((α →𝒄 β) × α)
i : ℕ
⊢ (↑c i).snd ≤ ↑(Chain.map c OrderHom.snd) i
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
⊢ ↑(ωSup c₀) (ωSup c₁) = ↑Prod.apply (ωSup (Chain.zip c₀ c₁))
[PROOFSTEP]
simp [Prod.apply_apply, Prod.ωSup_zip]
[GOAL]
α✝ : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α✝
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
α : Type u_5
f : α → β →𝒄 γ
⊢ Continuous { toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) }
[PROOFSTEP]
intro _
[GOAL]
α✝ : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α✝
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
α : Type u_5
f : α → β →𝒄 γ
c✝ : Chain β
⊢ ↑{ toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) } (ωSup c✝) =
    ωSup
      (Chain.map c✝
        { toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) })
[PROOFSTEP]
ext x
[GOAL]
case h
α✝ : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α✝
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
α : Type u_5
f : α → β →𝒄 γ
c✝ : Chain β
x : α
⊢ ↑{ toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) } (ωSup c✝)
      x =
    ωSup
      (Chain.map c✝
        { toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) })
      x
[PROOFSTEP]
change f _ _ = _
[GOAL]
case h
α✝ : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α✝
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
α : Type u_5
f : α → β →𝒄 γ
c✝ : Chain β
x : α
⊢ ↑(f x) (ωSup c✝) =
    ωSup
      (Chain.map c✝
        { toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) })
      x
[PROOFSTEP]
rw [(f _).continuous]
[GOAL]
case h
α✝ : Type u
α' : Type u_1
β : Type v
β' : Type u_2
γ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α✝
inst✝⁴ : OmegaCompletePartialOrder β
inst✝³ : OmegaCompletePartialOrder γ
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
α : Type u_5
f : α → β →𝒄 γ
c✝ : Chain β
x : α
⊢ ωSup (Chain.map c✝ ↑(f x)) =
    ωSup
      (Chain.map c✝
        { toFun := fun x y => ↑(f y) x, monotone' := (_ : ∀ (x y : β), x ≤ y → ∀ (a : α), ↑(f a) x ≤ ↑(f a) y) })
      x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ↑(OrderHom.bind (↑f) g.toOrderHom) (ωSup c) = ωSup (Chain.map c (OrderHom.bind (↑f) g.toOrderHom))
[PROOFSTEP]
rw [ωSup_bind, ← f.continuous, g.toOrderHom_eq_coe, ← g.continuous]
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ↑(OrderHom.bind ↑f ↑g) (ωSup c) = ↑f (ωSup c) >>= ↑g (ωSup c)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α →𝒄 Part β
⊢ (fun x => f <$> ↑g x) = ↑(bind g (const (pure ∘ f)))
[PROOFSTEP]
ext1
[GOAL]
case h
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : β → γ
g : α →𝒄 Part β
x✝ : α
⊢ f <$> ↑g x✝ = ↑(bind g (const (pure ∘ f))) x✝
[PROOFSTEP]
simp only [map_eq_bind_pure_comp, bind, coe_mk, OrderHom.bind_coe, coe_apply, coe_toOrderHom, const_apply]
[GOAL]
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α →𝒄 Part (β → γ)
g : α →𝒄 Part β
⊢ (fun x => Seq.seq (↑f x) fun x_1 => ↑g x) = ↑(bind f (flip (_root_.flip map g)))
[PROOFSTEP]
ext
[GOAL]
case h.H
α : Type u
α' : Type u_1
β✝ : Type v
β' : Type u_2
γ✝ : Type u_3
φ : Type u_4
inst✝⁵ : OmegaCompletePartialOrder α
inst✝⁴ : OmegaCompletePartialOrder β✝
inst✝³ : OmegaCompletePartialOrder γ✝
inst✝² : OmegaCompletePartialOrder φ
inst✝¹ : OmegaCompletePartialOrder α'
inst✝ : OmegaCompletePartialOrder β'
β γ : Type v
f : α →𝒄 Part (β → γ)
g : α →𝒄 Part β
x✝ : α
a✝ : γ
⊢ (a✝ ∈ Seq.seq (↑f x✝) fun x => ↑g x✝) ↔ a✝ ∈ ↑(bind f (flip (_root_.flip map g))) x✝
[PROOFSTEP]
simp only [seq_eq_bind_map, Part.bind_eq_bind, Part.mem_bind_iff, flip_apply, _root_.flip, map_apply, bind_apply]
