-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_bind {β γ : Type v} (c : Chain α) (f : α →o Part β) (g : α →o β → Part γ) :
    ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)

Proof state:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ (Pi.evalOrderHom b) (g (c i))
j : ℕ
hb : b ∈ (c.map f) j
⊢ y ∈ x

Tactic:
replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb

Result:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ (Pi.evalOrderHom b) (g (c i))
j : ℕ
hb : b ∈ f (c (i ⊔ j))
⊢ y ∈ x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ((c.map g).map (Pi.evalOrderHom b)) i
hb : Part.some b ∈ c.map f
⊢ y ∈ x

Tactic:
rcases hb with ⟨j, hb⟩

Result:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ ((c.map g).map (Pi.evalOrderHom b)) i
j : ℕ
hb : Part.some b = (c.map f) j
⊢ y ∈ x

Proof state:
case H
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
⊢ (∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x) ↔ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

Tactic:
constructor <;> intro h'''

Result:
case H.mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
⊢ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
⊢ ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x

Proof state:
case H.mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
⊢ ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x

Tactic:
intro b hb

Result:
case H.mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
⊢ ωSup (c.map g) b ≤ x

Proof state:
case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : y ∈ (c.map (f.partBind g)) i
⊢ y ∈ x

Tactic:
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe,
  Function.comp_apply, OrderHom.partBind_coe] at hy

Result:
case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : ∃ a ∈ f (c i), y ∈ g (c i) a
⊢ y ∈ x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)

Tactic:
apply eq_of_forall_ge_iff

Result:
case H
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1

Proof state:
case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
⊢ (c.map (f.partBind g)) i ≤ x

Tactic:
intro y hy

Result:
case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : y ∈ (c.map (f.partBind g)) i
⊢ y ∈ x

Proof state:
case H.mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
⊢ ωSup (c.map g) b ≤ x

Tactic:
apply ωSup_le _ _ _

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
⊢ ∀ (i : ℕ), ((c.map g).map (Pi.evalOrderHom b)) i ≤ x

Proof state:
case H.mpr.intro.intro.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ ωSup (c.map g) b

Tactic:
apply le_ωSup (c.map g) _ _ _ hb₁

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ b ∈ ωSup (c.map f)

Tactic:
apply le_ωSup (c.map f) i _ hb₀

Result:
no goals

Proof state:
case H.mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : ∃ a ∈ f (c i), y ∈ g (c i) a
⊢ y ∈ x

Tactic:
rcases hy with ⟨b, hb₀, hb₁⟩

Result:
case H.mpr.intro.intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ x

Proof state:
case intro.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (i ⊔ j))
hy : y ∈ g (c (i ⊔ j)) b
⊢ ∃ a ∈ f (c (i ⊔ j)), y ∈ g (c (i ⊔ j)) a

Tactic:
exact ⟨_, hb, hy⟩

Result:
no goals

Proof state:
case intro.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (i ⊔ j))
hy : y ∈ g (c (i ⊔ j)) b
⊢ y ∈ (c.map (f.partBind g)) (i ⊔ j)

Tactic:
simp only [exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, Chain.map_coe,
  Function.comp_apply, OrderHom.partBind_coe]

Result:
case intro.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (i ⊔ j))
hy : y ∈ g (c (i ⊔ j)) b
⊢ ∃ a ∈ f (c (i ⊔ j)), y ∈ g (c (i ⊔ j)) a

Proof state:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
hy : y ∈ (Pi.evalOrderHom b) (g (c i))
j : ℕ
hb : b ∈ f (c (i ⊔ j))
⊢ y ∈ x

Tactic:
replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy

Result:
case intro
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (i ⊔ j))
hy : y ∈ g (c (i ⊔ j)) b
⊢ y ∈ x