-- Mathlib/Topology/Order/ScottTopology.lean
@[simp] lemma scottContinuous_iff_continuous {D : Set (Set α)} [Topology.IsScott α D]
    (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D) : ScottContinuousOn D f ↔ Continuous f

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen u
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Tactic:
exact ⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD),
  fun t h₀ hd₁ hd₂ a hd₃ ha ↦ image_inter_nonempty_iff.mp <|
    (isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
    (directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsOpen (f ⁻¹' u)
⊢ False

Tactic:
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
⊢ False

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
⊢ False

Tactic:
obtain ⟨c, hcd, hfcb⟩ := hu.2 h₀ d₁ d₂ d₃ h

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
⊢ False

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
⊢ False

Tactic:
have hu : IsOpen (f ⁻¹' u) := (isOpen_compl_iff.2 Topology.IsScott.isClosed_Iic).preimage hf

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsOpen (f ⁻¹' u)
⊢ False

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ Continuous f → ScottContinuousOn D f

Tactic:
refine fun hf t h₀ d₁ d₂ a d₃ ↦
  ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
  fun b hb ↦ ?_⟩

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
⊢ f a ≤ b

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
⊢ False

Tactic:
simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  mem_setOf] at hb

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
hb : ∀ a ∈ t, f a ≤ b
⊢ False

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen u
⊢ IsOpen (f ⁻¹' u)

Tactic:
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)]

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen u
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
hb : ∀ a ∈ t, f a ≤ b
⊢ False

Tactic:
exact hfcb <| hb _ hcd

Result:
no goals