-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem scottContinuous_of_continuous {α β} [OmegaCompletePartialOrder α]
    [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : _root_.Continuous f) :
    OmegaCompletePartialOrder.ωScottContinuous f

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

Tactic:
have h : Monotone f := fun x y h ↦ by
  have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
  simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h

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

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

Tactic:
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : Continuous f
x y : Scott α
h : x ≤ y
hf : IsUpperSet {x | ¬f x ≤ f y}
⊢ f x ≤ f y

Tactic:
simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : ∀ (c : Chain α),
  (ωSup c ∈ f ⁻¹' notBelow z) = ωSup (c.map { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := ⋯ }) :=
  (ωScottContinuous.monotone_map_ωSup hf'').2
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
specialize hf' c

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (ωSup c ∈ f ⁻¹' notBelow z) = ωSup (c.map { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := ⋯ })
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (ωSup c ∈ f ⁻¹' notBelow z) = ωSup (c.map { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := ⋯ })
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
simp only [OrderHom.coe_mk, mem_preimage, notBelow, mem_setOf_eq] at hf'

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ (∃ a, (∃ y, ¬f (c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (c x) ≤ z

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
let hf' := hf''.monotone_map_ωSup.2

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : ∀ (c : Chain α),
  (ωSup c ∈ f ⁻¹' notBelow z) = ωSup (c.map { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := ⋯ }) :=
  (ωScottContinuous.monotone_map_ωSup hf'').2
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
⊢ ωScottContinuous f

Tactic:
rw [ωScottContinuous_iff_monotone_map_ωSup]

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

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ ¬f (ωSup c) ≤ z ↔ ¬ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
simp only [ωSup_le_iff, hf', ωSup, iSup, sSup, mem_range, Chain.map_coe, Function.comp_apply,
  eq_iff_iff, not_forall, OrderHom.coe_mk]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ (∃ a, (∃ y, ¬f (c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (c x) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
rcases (notBelow_isOpen z).preimage hf with hf''

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
x y : Scott α
h : x ≤ y
⊢ f x ≤ f y

Tactic:
have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : Continuous f
x y : Scott α
h : x ≤ y
hf : IsUpperSet {x | ¬f x ≤ f y}
⊢ f x ≤ f y