awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : SpectralMap β γ
g : SpectralMap α β
⊢ Eq (α := (a : α) → γ) (⇑(f.comp g) : (a : α) → γ)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : SpectralMap β γ
g : SpectralMap α β
a : α
⊢ Eq.{u_4 + 1} (α := γ) ((f.comp g : (a : α) → γ) a : γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : SpectralMap β γ
g : SpectralMap α β
⊢ Eq (α := α → γ) (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β))
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := β) (⇑(↑f : C(β, γ)) : (a : β) → γ) (⇑(↑g : C(α, β)) : (a : α) → β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : SpectralMap β γ
g : SpectralMap α β
⊢ Eq (α := C(α, γ)) (↑(f.comp g) : C(α, γ)) (ContinuousMap.comp (↑f : C(β, γ)) (↑g : C(α, β)))

Tactic:
rfl

Premises used: ContinuousMap.comp, toContinuousMap, rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : SpectralMap γ δ
g : SpectralMap β γ
h : SpectralMap α β
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: SpectralMap.comp, SpectralMap.toContinuousMap, rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : SpectralMap α β
⊢ f.comp (SpectralMap.id α) = f

Tactic:
ext fun _a => rfl

Premises used: SpectralMap.ext, rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : SpectralMap α β
⊢ comp (SpectralMap.id β) f = f

Tactic:
ext fun _a => rfl

Premises used: SpectralMap.ext, rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g₁ g₂ : SpectralMap β γ
f : SpectralMap α β
hf : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h,
   fun a => of_eq (congrFun (congrArg comp a) f)⟩

Premises used: Iff.mpr, SpectralMap.comp, Function.Surjective.forall, congrArg, DFunLike.ext_iff, of_eq, SpectralMap.ext, congrFun, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : SpectralMap β γ
f₁ f₂ : SpectralMap α β
hg : Injective.{u_3 + 1, u_4 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq.{u_4 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₁ : Eq.{u_4 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)
⊢ Eq.{u_4 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) a : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) a : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: SpectralMap.comp_apply
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
b : ι → Set X
basis : IsTopologicalBasis (Set.range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
⊢ ∀ U ∈ Set.range b, IsCompact U

Tactic:
simp_all
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NoetherianSpace X
⊢ PrespectralSpace X

Tactic:
.of_isTopologicalBasis isTopologicalBasis_opens fun _ _ ↦ NoetherianSpace.isCompact _

Premises used: PrespectralSpace.of_isTopologicalBasis, TopologicalSpace.isTopologicalBasis_opens, TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : PrespectralSpace X
⊢ TotallySeparatedSpace X

Tactic:
totallySeparatedSpace_iff_exists_isClopen.mpr fun _ _ hxy ↦
    have ⟨U, ⟨hU₁, hU₂⟩, hxU, hyU⟩ :=
      isTopologicalBasis.exists_subset_of_mem_open hxy isClosed_singleton.isOpen_compl
    ⟨U, ⟨hU₂.isClosed, hU₁⟩, hxU, fun h ↦ hyU h rfl⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, Compl.compl, Membership.mem, Exists, _private.0.instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace.match_1, PrespectralSpace.isTopologicalBasis, And, And.intro, Exists.intro, IsClopen, totallySeparatedSpace_iff_exists_isClopen, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open, IsCompact.isClosed
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
⊢ PrespectralSpace X

Tactic:
.of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_

Premises used: PrespectralSpace.of_isTopologicalBasis, PrespectralSpace.isTopologicalBasis, TopologicalSpace.IsOpenCover.isTopologicalBasis
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
refine :
  ∀ (U_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (i : ι),
          (fun (x : Set ↥(U i)) ↦ Subtype.val (p := fun (x : X) ↦ x ∈ U i) '' x) ''
            {U_2 : Set ↥(U i) | IsOpen[instTopologicalSpaceSubtype] U_2 ∧ IsCompact U_2})
        U_1 →
      IsCompact U_1
⊢ PrespectralSpace X

Tactic:
refine .of_isTopologicalBasis (hU.isTopologicalBasis fun i ↦ isTopologicalBasis) ?_
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
simp :
  ∀ (b : ι) (b_1 : Set ↥(U b)) (a : IsOpen[instTopologicalSpaceSubtype] b_1),
    IsCompact b_1 → IsCompact (Subtype.val (p := fun (x : X) ↦ x ∈ U b) '' b_1)
⊢ ∀ (U_1 : Set X),
    Membership.mem (γ := Set (Set X))
        (⋃ (i : ι),
          (fun (x : Set ↥(U i)) ↦ Subtype.val (p := fun (x : X) ↦ x ∈ U i) '' x) ''
            {U_2 : Set ↥(U i) | IsOpen[instTopologicalSpaceSubtype] U_2 ∧ IsCompact U_2})
        U_1 →
      IsCompact U_1

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
    forall_comm (α := Set _), forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_iUnion, Set.mem_image, forall_comm, forall_exists_index, Set.mem_setOf_eq, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
⊢ ∀ (b : ι) (b_1 : Set ↥(U b)) (a : IsOpen[instTopologicalSpaceSubtype] b_1),
    IsCompact b_1 → IsCompact (Subtype.val (p := fun (x : X) ↦ x ∈ U b) '' b_1)

Tactic:
fun i V hV hV' ↦ hV'.image continuous_subtype_val

Premises used: continuous_subtype_val, IsCompact.image
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
U : ι → Opens X
hU : IsOpenCover U
inst_1 : ∀ (i : ι), PrespectralSpace.{u_1} ↥(U i)
⊢ ∀ (b : ι) (b_1 : Set ↥(U b)) (a : IsOpen[instTopologicalSpaceSubtype] b_1),
    IsCompact b_1 → IsCompact (Subtype.val (p := fun (x : X) ↦ x ∈ U b) '' b_1)

Tactic:
exact fun i V hV hV' ↦ hV'.image continuous_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 Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
simp : ∀ (U : Set X) (x : Set Y), IsOpen[inst_1] x → IsCompact x → f ⁻¹' x = U → IsCompact U
⊢ ∀ U ∈ Set.preimage f '' {U : Set Y | IsOpen[inst_1] U ∧ IsCompact U}, IsCompact U

Tactic:
simp only [Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
U : Set Y
h₁ : IsOpen[inst_1] U
h₂ : IsCompact U
⊢ IsCompact (f ⁻¹' U)

Tactic:
hf'.isCompact_preimage_of_isOpen h₁ h₂

Premises used: IsSpectralMap.isCompact_preimage_of_isOpen
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsInducing f
hf' : IsSpectralMap f
U : Set Y
h₁ : IsOpen[inst_1] U
h₂ : IsCompact U
⊢ IsCompact (f ⁻¹' U)

Tactic:
exact hf'.isCompact_preimage_of_isOpen h₁ h₂

Premises used: IsSpectralMap.isCompact_preimage_of_isOpen
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ PrespectralSpace X

Tactic:
.of_isInducing f hf.isInducing hf.isProperMap.isSpectralMap

Premises used: Topology.IsClosedEmbedding.isInducing, IsProperMap.isSpectralMap, Topology.IsClosedEmbedding.isProperMap, PrespectralSpace.of_isInducing
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
apply :
  ∀ (x : X) (U : Set X) (hx : x ∈ U) (hU : IsOpen[inst] U),
    ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
⊢ IsTopologicalBasis.{u_1} (α := X) {U : Set X | IsOpen[inst] U ∧ IsCompact U}

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds (fun U hU ↦ hU.1) <| fun x U hx hU ↦ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
⊢ ∃ (V : Set Y), Membership.mem (γ := Set (Set Y)) {V : Set Y | IsOpen[inst_1] V ∧ IsCompact V} V ∧ f x ∈ V ∧ V ⊆ f '' U

Tactic:
(PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, PrespectralSpace.isTopologicalBasis, And.intro, Exists.intro, Iff.mp, 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 Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
obtain :
  ∀ (V : Set Y) (hoV : IsOpen[inst_1] V) (hcV : IsCompact V) (hfx : f x ∈ V) (hVf : V ⊆ f '' U),
    ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨V, ⟨hoV, hcV⟩, hfx, hVf⟩ : ∃ V ∈ {V | IsOpen V ∧ IsCompact V}, f x ∈ V ∧ V ⊆ f '' U :=
      (PrespectralSpace.isTopologicalBasis (X := Y)).isOpen_iff.mp
        (hf.isOpen_iff_image_isOpen.mp hU) (f x) ⟨x, hx, rfl⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, Topology.IsOpenEmbedding.isOpen_iff_image_isOpen, PrespectralSpace.isTopologicalBasis, And.intro, Exists.intro, Iff.mp, 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 Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U

Tactic:
⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩

Premises used: Topology.IsOpenEmbedding.continuous, Set.preimage, And.intro, Exists.intro, 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 Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
refine_1 : IsCompact (f ⁻¹' V)
refine_2 : ∀ (y : X) (hy : y ∈ f ⁻¹' V), y ∈ U
⊢ ∃ (v : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} v ∧ x ∈ v ∧ v ⊆ U

Tactic:
refine ⟨f ⁻¹' V, ⟨hoV.preimage hf.continuous, ?_⟩, ⟨hfx, fun y hy ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ IsCompact (f ⁻¹' V)

Tactic:
hf.toIsInducing.isCompact_preimage' hcV <| Set.SurjOn.subset_range hVf

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsInducing.isCompact_preimage', Topology.IsEmbedding.toIsInducing, Set.SurjOn.subset_range
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
⊢ IsCompact (f ⁻¹' V)

Tactic:
exact hf.toIsInducing.isCompact_preimage' hcV <| Set.SurjOn.subset_range hVf

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsInducing.isCompact_preimage', Topology.IsEmbedding.toIsInducing, Set.SurjOn.subset_range
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
y : X
hy : y ∈ f ⁻¹' V
⊢ y ∈ U

Tactic:
hf.injective.mem_set_image.mp (hVf hy)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Iff.mp, Function.Injective.mem_set_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 Y
f : X → Y
hf : IsOpenEmbedding f
x : X
U : Set X
hx : x ∈ U
hU : IsOpen[inst] U
V : Set Y
hoV : IsOpen[inst_1] V
hcV : IsCompact V
hfx : f x ∈ V
hVf : V ⊆ f '' U
y : X
hy : y ∈ f ⁻¹' V
⊢ y ∈ U

Tactic:
exact hf.injective.mem_set_image.mp (hVf hy)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Topology.IsEmbedding.injective, Iff.mp, Function.Injective.mem_set_image
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
U : Set ((i : ι) × X i)
hU :
  Membership.mem (γ := Set (Set ((i : ι) × X i)))
    (⋃ (i : ι),
      (fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
        {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
    U
⊢ ∃ (i : ι),
    Membership.mem (γ := Set (Set ((i : ι) × X i)))
      ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
        {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
      U

Tactic:
simp_rw [Set.mem_iUnion] at hU

Premises used: Set.mem_iUnion
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
U : Set ((i : ι) × X i)
hU :
  ∃ (i : ι),
    Membership.mem (γ := Set (Set ((i : ι) × X i)))
      ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) ''
        {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U})
      U
obtain :
  ∀ (i : ι) (V : Set (X i))
    (hV : Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U} V),
    IsCompact (X := (i : ι) × X i) ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) V)
⊢ IsCompact U

Tactic:
obtain ⟨i, V, hV, rfl⟩ := hU

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
i : ι
V : Set (X i)
hV : Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U} V
⊢ IsCompact (X := (i : ι) × X i) ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) V)

Tactic:
hV.2.image continuous_sigmaMk

Premises used: continuous_sigmaMk, And.right, IsCompact.image
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), PrespectralSpace.{u_4} (X i)
i : ι
V : Set (X i)
hV : Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst_2 i] U ∧ IsCompact U} V
⊢ IsCompact (X := (i : ι) × X i) ((fun (u : Set (X i)) ↦ Sigma.mk (β := fun (i : ι) ↦ X i) i '' u) V)

Tactic:
exact hV.2.image continuous_sigmaMk

Premises used: continuous_sigmaMk, And.right, IsCompact.image
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
⊢ IsTopologicalBasis.{u_1} (α := X) {U : Set X | IsOpen[inst] U ∧ IsCompact U}

Tactic:
isTopologicalBasis (X := X)

Premises used: PrespectralSpace.isTopologicalBasis
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
h :
  Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} =
    {U : Set X | IsOpen[inst] U ∧ IsCompact U}
⊢ IsTopologicalBasis (Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)})

Tactic:
convert! isTopologicalBasis (X := X)

Premises used: PrespectralSpace.isTopologicalBasis
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
h :
  ∀ (s : Set X),
    s ∈ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} ↔
      Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} s
⊢ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} =
    {U : Set X | IsOpen[inst] U ∧ IsCompact U}

Tactic:
ext s
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
s : Set X
⊢ s ∈ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} ↔
    Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} s

Tactic:
⟨fun ⟨V, hV, heq⟩ ↦ heq ▸ ⟨V.2, hV⟩, fun h ↦ ⟨⟨s, h.1⟩, h.2, rfl⟩⟩

Premises used: setOf, Membership.mem, Eq.rec, _private.0.PrespectralSpace.isBasis_opens.match_1, And, And.right, TopologicalSpace.Opens.mk, And.left, And.intro, Iff.intro, Exists.intro, IsOpen, TopologicalSpace.Opens.is_open', rfl, IsCompact
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
s : Set X
⊢ s ∈ Set.image (α := Opens X) SetLike.coe {U : Opens X | IsCompact (↑U : Set X)} ↔
    Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} s

Tactic:
exact ⟨fun ⟨V, hV, heq⟩ ↦ heq ▸ ⟨V.2, hV⟩, fun h ↦ ⟨⟨s, h.1⟩, h.2, 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
U : Opens X
⊢ Membership.mem (γ := Set (CompactOpens X))
    (LowerSet.carrier { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯ }) ⊥

Tactic:
simp
-- 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
U₁ : CompactOpens X
h₁ :
  Membership.mem (γ := Set (CompactOpens X))
    (LowerSet.carrier { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯ }) U₁
U₂ : CompactOpens X
h₂ :
  Membership.mem (γ := Set (CompactOpens X))
    (LowerSet.carrier { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯ }) U₂
⊢ Membership.mem (γ := Set (CompactOpens X))
    (LowerSet.carrier { carrier := {V : CompactOpens X | (↑V : Set X) ⊆ (↑U : Set X)}, lower' := ⋯ }) (U₁ ⊔ U₂)

Tactic:
aesop
-- 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
a :
  (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) ≤
    U
a₁ :
  U ≤
    (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)
⊢ (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) =
    U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
a :
  ∀ (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
⊢ (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) ≤
    U

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- 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:
fun _ ↦ id

Premises used: Set.Mem, setOf, id, Set.Subset