awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
⊢ ∀ (i : CompactOpens X)
    (i_1 :
      i ∈
        { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
          Order.Ideal (CompactOpens X) }),
    i.toOpens ≤ U

Tactic:
exact fun _ ↦ id

Premises used: id
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
a :
  ∀ (V : Set X) (h₁ : IsOpen[inst] V) (h₂ : IsCompact V) (hxV : x ∈ V) (hVU : V ⊆ (↑U : Set X)),
    Membership.mem (γ := Opens X)
      ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
        ((fun (U : Opens X) ↦
            { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯,
              directed' := ⋯ : Order.Ideal (CompactOpens X) })
          U))
      x
⊢ Membership.mem (γ := Opens X)
    ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U))
    x

Tactic:
obtain ⟨V, ⟨h₁, h₂⟩, hxV, hVU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2

Premises used: PrespectralSpace.isTopologicalBasis, TopologicalSpace.Opens.is_open', TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ (↑U : Set X)
a :
  ∃ (i : CompactOpens X) (_ :
    i ∈
      { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
        Order.Ideal (CompactOpens X) }),
    x ∈ i.toOpens
⊢ Membership.mem (γ := Opens X)
    ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X))
      ((fun (U : Opens X) ↦
          { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
            Order.Ideal (CompactOpens X) })
        U))
    x

Tactic:
simp only [Opens.mem_iSup]

Premises used: TopologicalSpace.Opens.mem_iSup
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ (↑U : Set X)
⊢ ∃ (i : CompactOpens X) (_ :
    i ∈
      { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
        Order.Ideal (CompactOpens X) }),
    x ∈ i.toOpens

Tactic:
⟨⟨⟨_, h₂⟩, h₁⟩, hVU, hxV⟩

Premises used: TopologicalSpace.CompactOpens.mk, TopologicalSpace.Compacts.mk, Exists.intro
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ (↑U : Set X)
⊢ ∃ (i : CompactOpens X) (_ :
    i ∈
      { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
        Order.Ideal (CompactOpens X) }),
    x ∈ i.toOpens

Tactic:
exact ⟨⟨⟨_, h₂⟩, h₁⟩, hVU, hxV⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
a :
  ∀ (U : CompactOpens X),
    U ∈
        (↑((fun (U : Opens X) ↦
                { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯,
                  directed' := ⋯ : Order.Ideal (CompactOpens X) })
              ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X)) I)) :
          Set (CompactOpens X)) ↔
      U ∈ (↑I : Set (CompactOpens X))
⊢ (fun (U : Opens X) ↦
        { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ :
          Order.Ideal (CompactOpens X) })
      ((fun (I : Order.Ideal (CompactOpens X)) ↦ (⨆ U ∈ I, U.toOpens : Opens X)) I) =
    I

Tactic:
ext U
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
a : U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ (↑I : Set (CompactOpens X))
⊢ U ∈
      (↑{ carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑(⨆ U ∈ I, U.toOpens) : Set X)}, lower' := ⋯, nonempty' := ⋯,
            directed' := ⋯ : Order.Ideal (CompactOpens X) } :
        Set (CompactOpens X)) ↔
    U ∈ (↑I : Set (CompactOpens X))

Tactic:
change U.toOpens ≤ _ ↔ _

Premises used: TopologicalSpace.CompactOpens.toOpens
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
⊢ U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ (↑I : Set (CompactOpens X))

Tactic:
⟨fun H ↦ ?_, fun h ↦ le_iSup₂ (f := fun U (h : U ∈ I) ↦ U.toOpens) U h⟩

Premises used: le_iSup₂, Iff.intro
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
a : ∀ (H : U.toOpens ≤ ⨆ U ∈ I, U.toOpens), U ∈ (↑I : Set (CompactOpens X))
⊢ U.toOpens ≤ ⨆ U ∈ I, U.toOpens ↔ U ∈ (↑I : Set (CompactOpens X))

Tactic:
refine ⟨fun H ↦ ?_, fun h ↦ le_iSup₂ (f := fun U (h : U ∈ I) ↦ U.toOpens) U h⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : U.toOpens ≤ ⨆ U ∈ I, U.toOpens
⊢ (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)

Tactic:
simp only [← SetLike.coe_subset_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk] at H

Premises used: TopologicalSpace.Opens.iSup_mk, SetLike.coe_subset_coe, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
a :
  ∀ (s : Set (CompactOpens X)) (hsI : s ⊆ (↑I : Set (CompactOpens X))) (hs : s.Finite)
    (hU : (↑U : Set X) ⊆ ⋃ i ∈ s, (↑i.toOpens : Set X)), U ∈ (↑I : Set (CompactOpens X))
⊢ U ∈ (↑I : Set (CompactOpens X))

Tactic:
obtain ⟨s, hsI, hs, hU⟩ := U.isCompact.elim_finite_subcover_image (fun U _ ↦ U.2) H

Premises used: TopologicalSpace.CompactOpens.isCompact, IsCompact.elim_finite_subcover_image
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
s : Set (CompactOpens X)
hsI : s ⊆ (↑I : Set (CompactOpens X))
hs : s.Finite
hU : (↑U : Set X) ⊆ ⋃ i ∈ s, (↑i.toOpens : Set X)
⊢ U ≤ hs.toFinset (s := s).sup fun (i : CompactOpens X) ↦ i

Tactic:
simpa [← SetLike.coe_subset_coe]

Premises used: SetLike.coe_subset_coe
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
s : Set (CompactOpens X)
hsI : s ⊆ (↑I : Set (CompactOpens X))
hs : s.Finite
hU : (↑U : Set X) ⊆ ⋃ i ∈ s, (↑i.toOpens : Set X)
⊢ (hs.toFinset (s := s).sup fun (i : CompactOpens X) ↦ i) ∈ (↑I : Set (CompactOpens X))

Tactic:
simpa
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : (↑U.toOpens : Set X) ⊆ ⋃ i ∈ I, (↑i.toOpens : Set X)
s : Set (CompactOpens X)
hsI : s ⊆ (↑I : Set (CompactOpens X))
hs : s.Finite
hU : (↑U : Set X) ⊆ ⋃ i ∈ s, (↑i.toOpens : Set X)
⊢ U ∈ (↑I : Set (CompactOpens X))

Tactic:
exact I.lower (a := hs.toFinset.sup fun i ↦ i) (by simpa [← SetLike.coe_subset_coe]) (by simpa)

Premises used: Order.Ideal.lower
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
⊢ (∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)) ↔ U ≤ V

Tactic:
⟨?_, fun H W ↦ (le_trans · H)⟩

Premises used: Iff.intro, le_trans
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
refine : (∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)) → U ≤ V
⊢ (∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)) ↔ U ≤ V

Tactic:
refine ⟨?_, fun H W ↦ (le_trans · H)⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)
x : X
hxU : x ∈ U
obtain : ∀ (W : Set X) (h₁ : IsOpen[inst] W) (h₂ : IsCompact W) (hxW : x ∈ W) (hWU : W ⊆ (↑U : Set X)), x ∈ V
⊢ x ∈ V

Tactic:
obtain ⟨W, ⟨h₁, h₂⟩, hxW, hWU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxU U.2

Premises used: PrespectralSpace.isTopologicalBasis, TopologicalSpace.Opens.is_open', TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)
x : X
hxU : x ∈ U
W : Set X
h₁ : IsOpen[inst] W
h₂ : IsCompact W
hxW : x ∈ W
hWU : W ⊆ (↑U : Set X)
⊢ x ∈ V

Tactic:
H ⟨⟨W, h₂⟩, h₁⟩ hWU hxW

Premises used: TopologicalSpace.CompactOpens.mk, TopologicalSpace.Compacts.mk
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
U V : Opens X
H : ∀ (W : CompactOpens X), (↑W : Set X) ⊆ (↑U : Set X) → (↑W : Set X) ⊆ (↑V : Set X)
x : X
hxU : x ∈ U
W : Set X
h₁ : IsOpen[inst] W
h₂ : IsCompact W
hxW : x ∈ W
hWU : W ⊆ (↑U : Set X)
⊢ x ∈ V

Tactic:
exact H ⟨⟨W, h₂⟩, h₁⟩ hWU hxW

Premises used: TopologicalSpace.CompactOpens.mk, TopologicalSpace.Compacts.mk
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
obtain :
  ∀ (Us : Set (Opens X)) (hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)})
    (heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us),
    ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U

Tactic:
obtain ⟨Us, hUs, heq⟩ := TopologicalSpace.Opens.isBasis_iff_cover.mp
    (PrespectralSpace.isBasis_opens X) ⟨f ⁻¹' U, hU.preimage hfc⟩

Premises used: TopologicalSpace.Opens.mk, Set.preimage, Iff.mp, TopologicalSpace.Opens.isBasis_iff_cover, PrespectralSpace.isBasis_opens, IsOpen.preimage
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
⊢ ∃ (t : Finset (↑Us : Type u_1)), U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i

Tactic:
hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)

Premises used: IsCompact.elim_finite_subcover, SetLike.coe, Set.image, TopologicalSpace.Opens.is_open', Subtype.val
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
refine :
  ∀ (x : Y) (hx : x ∈ U),
    Membership.mem (γ := Set Y)
      (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) x
⊢ ∃ (t : Finset (↑Us : Type u_1)), U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i

Tactic:
refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)

Premises used: IsCompact.elim_finite_subcover, SetLike.coe, Set.image, TopologicalSpace.Opens.is_open', Subtype.val
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : Y
hx : x ∈ U
obtain :
  ∀ (x : X) (hx : f x ∈ U),
    Membership.mem (γ := Set Y)
      (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) x

Tactic:
obtain ⟨x, rfl⟩ := hs hx

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx : f x ∈ U
rwa rwa₁ rwa₂ rwa₃ : x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X }
⊢ x ∈ sSup Us

Tactic:
rwa [← heq]
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx : f x ∈ U
obtain :
  ∀ (i : Opens X) (hi : i ∈ Us) (hx : x ∈ i),
    Membership.mem (γ := Set Y)
      (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)

Tactic:
obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]

Premises used: TopologicalSpace.Opens.mem_sSup, Iff.mp
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx_1 : f x ∈ U
i : Opens X
hi : i ∈ Us
hx : x ∈ i
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)

Tactic:
Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩

Premises used: Iff.mpr, Set.Mem, Set.mem_iUnion, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
x : X
hx_1 : f x ∈ U
i : Opens X
hi : i ∈ Us
hx : x ∈ i
⊢ Membership.mem (γ := Set Y)
    (⋃ (i : (↑Us : Type u_1)), (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i) (f x)

Tactic:
exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
obtain :
  ∀ (t : Finset (↑Us : Type u_1)) (ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i),
    ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U

Tactic:
obtain ⟨t, ht⟩ := by
    refine hc.elim_finite_subcover (fun s : Us ↦ f '' s.1) (fun s ↦ h _ s.1.2) (fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := hs hx
    obtain ⟨i, hi, hx⟩ := mem_sSup.mp <| by rwa [← heq]
    exact Set.mem_iUnion.mpr ⟨⟨i, hi⟩, x, hx, rfl⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U

Tactic:
⟨⨆ s ∈ t, s.1, ?_, ?_⟩

Premises used: iSup, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
refine_1 : IsCompact.{u_1} (X := X) (carrier (⨆ s ∈ t, (↑s : Opens X)))
refine_2 : f '' (↑(⨆ s ∈ t, (↑s : Opens X)) : Set X) = U
⊢ ∃ (V : Opens X), IsCompact V.carrier ∧ f '' (↑V : Set X) = U

Tactic:
refine ⟨⨆ s ∈ t, s.1, ?_, ?_⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
refine_1 : IsCompact.{u_1} (X := X) (⋃ i ∈ t, (↑i.1 : Set X))
⊢ IsCompact.{u_1} (X := X) (carrier (⨆ s ∈ t, (↑s : Opens X)))

Tactic:
simp only [iSup_mk, carrier_eq_coe, coe_mk]

Premises used: TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ t, (↑i.1 : Set X))

Tactic:
t.finite_toSet.isCompact_biUnion fun i _ ↦ hUs i.2

Premises used: Set.Finite.isCompact_biUnion, Finset.finite_toSet, Subtype.property
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ t, (↑i.1 : Set X))

Tactic:
exact t.finite_toSet.isCompact_biUnion fun i _ ↦ hUs i.2

Premises used: Set.Finite.isCompact_biUnion, Finset.finite_toSet, Subtype.property
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
refine_2 :
  ⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X) = U
⊢ f '' (↑(⨆ s ∈ t, (↑s : Opens X)) : Set X) = U

Tactic:
simp only [iSup_mk, carrier_eq_coe, Set.iUnion_coe_set, coe_mk, Set.image_iUnion]

Premises used: TopologicalSpace.Opens.iSup_mk, Set.iUnion_coe_set, Set.image_iUnion, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
h₁ :
  Eq.{u_2 + 1} (α := Set Y)
    (⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X))
    (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X))
refine_2 : ⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X) = U
⊢ ⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X) = U

Tactic:
convert_to ⋃ i ∈ t, f '' i.1 = U