-- Mathlib/Order/OmegaCompletePartialOrder.lean
/-- `ωScottContinuous f` asserts that `f` is both monotone and distributes over ωSup. -/
lemma ωScottContinuous_iff_monotone_map_ωSup :
    ωScottContinuous f ↔ ∃ hf : Monotone f, ∀ c : Chain α, f (ωSup c) = ωSup (c.map ⟨f, hf⟩)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

Tactic:
refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })) → ωScottContinuous f

Proof state:
case h.e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c => Set.range ⇑c) c) a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [← hf.2 c, ωSup_eq_of_isLUB hda]

Result:
no goals

Proof state:
case h.e'_3
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f '' d✝ = Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [map_coe, OrderHom.coe_mk, ← hc, ← (Set.range_comp f ⇑c)]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ IsLUB (f '' d✝) (f a✝)

Tactic:
convert isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })

Result:
case h.e'_3
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f '' d✝ = Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })

case h.e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Proof state:
case h.e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
rw [← hc] at hda

Result:
case h.e'_4
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB ((fun c => Set.range ⇑c) c) a✝
⊢ f a✝ = ωSup (c.map { toFun := f, monotone' := ⋯ })

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })) → ωScottContinuous f

Tactic:
intro hf _ ⟨c, hc⟩ _ _ _ hda

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c => Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 => x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ IsLUB (f '' d✝) (f a✝)