case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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)
apply eq_of_forall_ge_iff
case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
intro x
case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
simp only [ωSup_le_iff, Part.bind_le, Chain.mem_map_iff, and_imp, OrderHom.bind_coe, exists_imp]
case H.mp
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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

case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
constructor <;> intro h'''
case H.mp
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mp
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
intro b hb
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mp
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
apply ωSup_le _ _ _
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
rintro i y hy
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
simp only [Part.mem_ωSup] at hb
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
rcases hb with ⟨j, hb⟩
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
replace hb := hb.symm
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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 j)
⊢ y ∈ x
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
simp only [Part.eq_some_iff, Chain.map_coe, Function.comp_apply, OrderHom.apply_coe] at hy hb
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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 j)
⊢ y ∈ x
replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
case intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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)
case intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
apply h''' (max i j)
case intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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)
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe,
  Function.comp_apply, OrderHom.bind_coe]
no goals
case intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
exact ⟨_, hb, hy⟩
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
intro i
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
intro y hy
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe,
  Function.comp_apply, OrderHom.bind_coe] at hy
case H.mpr.intro.intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
case H.mpr
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
rcases hy with ⟨b, hb₀, hb₁⟩
case H.mpr.intro.intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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

α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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)
case H.mpr.intro.intro
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
apply h''' b _
no goals
case H.mpr.intro.intro.a
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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
apply le_ωSup (c.map g) _ _ _ hb₁
no goals
α : Type u
α' : Type ?u.55703
β✝ : Type v
β' : Type ?u.55708
γ✝ : Type ?u.55711
φ : Type ?u.55714
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)
apply le_ωSup (c.map f) i _ hb₀