awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
apply : ∀ᶠ (x : ι) in l, ¬(fun (n : ι) ↦ y n ∈ s) x
⊢ False

Tactic:
apply this
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
h : ∀ (n : ι) (hn : n ∈ y ⁻¹' t) (hyn : y n ∈ s), False
⊢ ∀ᶠ (x : ι) in l, ¬(fun (n : ι) ↦ y n ∈ s) x

Tactic:
filter_upwards [hy₀ ht] with n hn hyn
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
n : ι
hn : n ∈ y ⁻¹' t
hyn : y n ∈ s
⊢ False

Tactic:
hst.notMem_of_mem_left hyn hn

Premises used: Disjoint.notMem_of_mem_left
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this_1 : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
this : ∃ᶠ (n : ι) in l, y n ∈ s
n : ι
hn : n ∈ y ⁻¹' t
hyn : y n ∈ s
⊢ False

Tactic:
exact hst.notMem_of_mem_left hyn hn

Premises used: Disjoint.notMem_of_mem_left
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
suffices : ∃ᶠ (n : ι) in l, y n ∈ s
⊢ False

Tactic:
suffices ∃ᶠ n in l, y n ∈ s by
    apply this
    filter_upwards [hy₀ ht] with n hn hyn
    exact hst.notMem_of_mem_left hyn hn
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
apply : ∀ᶠ (x_1 : ι) in l, y x_1 ∈ f (x x_1) → y x_1 ∈ s
⊢ ∃ᶠ (n : ι) in l, y n ∈ s

Tactic:
apply hy.mp

Premises used: Filter.Frequently.mp
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
h : ∀ (n : ι) (hn : n ∈ x ⁻¹' {x : α | s ∈ 𝓝ˢ (f x)}) (hyn : y n ∈ f (x n)), y n ∈ s
⊢ ∀ᶠ (x_1 : ι) in l, y x_1 ∈ f (x x_1) → y x_1 ∈ s

Tactic:
filter_upwards [hx (hf s hs)] with n hn hyn
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
n : ι
hn : n ∈ x ⁻¹' {x : α | s ∈ 𝓝ˢ (f x)}
hyn : y n ∈ f (x n)
⊢ f (x n) ⊆ interior s

Tactic:
simp only [← subset_interior_iff_mem_nhdsSet, preimage_setOf_eq, mem_setOf_eq] at hn

Premises used: Set.mem_setOf_eq, Set.preimage_setOf_eq, subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
n : ι
hyn : y n ∈ f (x n)
hn : f (x n) ⊆ interior s
⊢ y n ∈ s

Tactic:
interior_subset <| hn hyn

Premises used: interior_subset
-- Module: Mathlib.Topology.Semicontinuity.Hemicontinuity
Goal:
α : Type u_5
β : Type u_6
ι : Type u_7
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : RegularSpace β
f : α → Set β
x₀ : α
l : Filter ι
hf : UpperHemicontinuousAt f x₀
hf_closed : IsClosed[inst_1] (f x₀)
x : ι → α
hx : Tendsto x l (𝓝 x₀)
y : ι → β
hy : ∃ᶠ (n : ι) in l, y n ∈ f (x n)
y₀ : β
hy₀ : Tendsto y l (𝓝 y₀)
this : y₀ ∉ f x₀
s : Set β
hs : s ∈ 𝓝ˢ (f x₀)
t : Set β
ht : t ∈ 𝓝 y₀
hst : Disjoint s t
n : ι
hyn : y n ∈ f (x n)
hn : f (x n) ⊆ interior s
⊢ y n ∈ s

Tactic:
exact interior_subset <| hn hyn

Premises used: interior_subset
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : IsGLB 𝓕 s
simp_rw :
  ∀ (h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)),
    ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsGLB 𝓕' s

Tactic:
simp_rw [isGLB_pi] at *

Premises used: isGLB_pi
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
rcases :
  ∀ (D : Set E) (D_count : D.Countable) (D_dense : Dense D),
    ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)

Tactic:
rcases exists_countable_dense E with ⟨D, D_count, D_dense⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
⊢ ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)

Tactic:
have U_open {f} (hf : f ∈ 𝓕) (d : E) : IsOpen (U f d) := h𝓕_cont f hf |>.isOpen_preimage d
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
d : E
h :
  ∀ (x : X),
    Membership.mem (γ := Set X) {x : X | s x < d} x ↔
      Membership.mem (γ := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) x
⊢ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)

Tactic:
ext x
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
d : E
x : X
⊢ Membership.mem (γ := Set X) {x : X | s x < d} x ↔
    Membership.mem (γ := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) x

Tactic:
simp [U, isGLB_lt_iff (h𝓕 x)]

Premises used: isGLB_lt_iff
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
⊢ ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)

Tactic:
have (d : E) : {x | s x < d} = ⋃ f : 𝓕, U f d := by
    ext x
    simp [U, isGLB_lt_iff (h𝓕 x)]
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
simp_rw :
  ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
⊢ ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)

Tactic:
simp_rw [this d]
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
rcases :
  ∀ (t : Set (↑𝓕 : Type (max u_1 u_2))) (t_count : t.Countable)
    (ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)),
    ∃ A ⊆ 𝓕,
      A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)
⊢ ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)

Tactic:
rcases eq_open_union_countable (fun f : 𝓕 ↦ U f d) (fun f ↦ U_open f.2 d) with ⟨t, t_count, ht⟩

Premises used: eq_open_union_countable, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
t : Set (↑𝓕 : Type (max u_1 u_2))
t_count : t.Countable
ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)
right :
  Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
    (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
⊢ ∃ A ⊆ 𝓕,
    A.Countable ∧ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d) (⋃ f ∈ A, U f d)

Tactic:
use (↑) '' t, image_val_subset, t_count.image _

Premises used: Set.Countable.image, Set.image_val_subset
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
d : E
t : Set (↑𝓕 : Type (max u_1 u_2))
t_count : t.Countable
ht : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ (i : (↑𝓕 : Type (max u_1 u_2))), U (↑i : X → E) d)
right :
  Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)
right₁ right₂ : Eq.{u_1 + 1} (α := Set X) (⋃ i ∈ t, U (↑i : X → E) d) (⋃ y ∈ t, U (↑y : X → E) d)
⊢ Eq.{u_1 + 1} (α := Set X) (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
    (⋃ f ∈ Subtype.val (p := fun (x : X → E) ↦ x ∈ 𝓕) '' t, U f d)

Tactic:
rw [← ht, biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
⊢ ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)

Tactic:
have (d : E) : ∃ A ⊆ 𝓕, A.Countable ∧ {x | s x < d} = ⋃ f ∈ A, U f d := by
    simp_rw [this d]
    rcases eq_open_union_countable (fun f : 𝓕 ↦ U f d) (fun f ↦ U_open f.2 d) with ⟨t, t_count, ht⟩
    use (↑) '' t, image_val_subset, t_count.image _
    rw [← ht, biUnion_image]
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this_1 : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
this : ∀ (d : E), ∃ A ⊆ 𝓕, A.Countable ∧ Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A, U f d)
choose :
  ∀ (A : (d : E) → Set (X → E)) (A_sub : ∀ (d : E), A d ⊆ 𝓕) (A_count : ∀ (d : E), (A d).Countable)
    (hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)),
    ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)

Tactic:
choose A A_sub A_count hA using this
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
⊢ 𝓕' ⊆ 𝓕

Tactic:
have 𝓕'_sub : 𝓕' ⊆ 𝓕 := iUnion₂_subset fun d _ ↦ A_sub d
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
right : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)

Tactic:
use 𝓕', 𝓕'_sub, D_count.biUnion fun d _ ↦ A_count d

Premises used: Set.Countable.biUnion
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
⊢ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)

Tactic:
fun x ↦ ⟨lowerBounds_mono_set (image_mono 𝓕'_sub) (h𝓕 x).1, fun e he ↦ ?_⟩

Premises used: Set.image_mono, lowerBounds_mono_set, IsGreatest, And.left, IsGLB, And.intro
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
right : ∀ (x : X) (e : E) (he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')), e ≤ s x
⊢ ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕') (s a)

Tactic:
refine fun x ↦ ⟨lowerBounds_mono_set (image_mono 𝓕'_sub) (h𝓕 x).1, fun e he ↦ ?_⟩
-- Module: Mathlib.Topology.Semicontinuity.Lindelof
Goal:
X : Type u_1
E : Type u_2
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
inst_2 : LinearOrder E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
inst_5 : DenselyOrdered E
inst_6 : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval (β := fun (a : X) ↦ E) a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (f : X → E) → (d : E) → Set X := fun (f : X → E) (d : E) ↦ {x : X | f x < d}
U_open : ∀ {f : X → E} (hf : f ∈ 𝓕) (d : E), IsOpen (U f d)
this : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ (f : (↑𝓕 : Type (max u_1 u_2))), U (↑f : X → E) d)
A : (d : E) → Set (X → E)
A_sub : ∀ (d : E), A d ⊆ 𝓕
A_count : ∀ (d : E), (A d).Countable
hA : ∀ (d : E), Eq.{u_1 + 1} (α := Set X) {x : X | s x < d} (⋃ f ∈ A d, U f d)
𝓕' : Set (X → E) := ⋃ d ∈ D, A d
𝓕'_sub : 𝓕' ⊆ 𝓕
x : X
e : E
he : e ∈ lowerBounds (Function.eval (β := fun (a : X) ↦ E) x '' 𝓕')
right : ∀ (H : s x < e), False
⊢ e ≤ s x

Tactic:
by_contra! H