awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst, inst_1] f
hK : IsCompact K
hU : IsOpen[inst_1] U
hKU : MapsTo f K U
choose! :
  ∀ (V : (x : X) → Set X) (hxV : ∀ (x : X) (hx : x ∈ K), V x ∈ 𝓝 x) (hVc : ∀ (x : X) (hx : x ∈ K), IsCompact (V x))
    (hVU : ∀ (x : X) (hx : x ∈ K), MapsTo f (V x) U), ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
    exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))

Premises used: LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst, inst_1] f
hK : IsCompact K
hU : IsOpen[inst_1] U
hKU : MapsTo f K U
V : (x : X) → Set X
hxV : ∀ (x : X) (hx : x ∈ K), V x ∈ 𝓝 x
hVc : ∀ (x : X) (hx : x ∈ K), IsCompact (V x)
hVU : ∀ (x : X) (hx : x ∈ K), MapsTo f (V x) U
rcases : ∀ (s : Finset X) (hsK : ∀ x ∈ s, x ∈ K) (hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K), ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩

Premises used: IsCompact.elim_nhds_subcover_nhdsSet
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst, inst_1] f
hK : IsCompact K
hU : IsOpen[inst_1] U
hKU : MapsTo f K U
V : (x : X) → Set X
hxV : ∀ (x : X) (hx : x ∈ K), V x ∈ 𝓝 x
hVc : ∀ (x : X) (hx : x ∈ K), IsCompact (V x)
hVU : ∀ (x : X) (hx : x ∈ K), MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦
    hVU x (hsK x hx)⟩

Premises used: Iff.mpr, Finset.isCompact_biUnion, And.intro, Exists.intro, Set.mapsTo_iUnion₂
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous[inst, inst_1] f
hK : IsCompact K
hU : IsOpen[inst_1] U
hKU : MapsTo f K U
V : (x : X) → Set X
hxV : ∀ (x : X) (hx : x ∈ K), V x ∈ 𝓝 x
hVc : ∀ (x : X) (hx : x ∈ K), IsCompact (V x)
hVU : ∀ (x : X) (hx : x ∈ K), MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦
    hVU x (hsK x hx)⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
h_KU : K ⊆ U
⊢ ∃ (L : Set X), IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U

Tactic:
let ⟨L, hKL, hL, hLU⟩ := exists_mem_nhdsSet_isCompact_mapsTo continuous_id hK hU h_KU
  ⟨L, hL, subset_interior_iff_mem_nhdsSet.2 hKL, hLU⟩

Premises used: Iff.mpr, Exists, HasSubset.Subset, exists_mem_nhdsSet_isCompact_mapsTo, And, continuous_id, subset_interior_iff_mem_nhdsSet, And.intro, interior, _private.0.exists_compact_between.match_1, Exists.intro, IsCompact
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ s) → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ t

Tactic:
grind
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
rw : ∀ (i : Set X), IsOpen[inst] i ∧ K ⊆ i → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ i
⊢ (𝓝ˢ K).HasBasis (fun (L : Set X) ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id

Tactic:
rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]

Premises used: hasBasis_nhdsSet, Filter.hasBasis_self, Filter.HasBasis.forall_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
this : ∀ (hU : IsOpen[inst] U) (h_KU : K ⊆ U), ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
⊢ IsOpen[inst] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U

Tactic:
⟨hU, h_KU⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
obtain : ∀ (L : Set X) (hL : IsCompact L) (hKL : K ⊆ interior L) (hLU : L ⊆ U), ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U

Tactic:
obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between hK hU h_KU

Premises used: exists_compact_between
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
rwa rwa₁ rwa₂ rwa₃ : K ⊆ interior L
⊢ L ∈ 𝓝ˢ K

Tactic:
rwa [← subset_interior_iff_mem_nhdsSet]

Premises used: subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst] U
h_KU : K ⊆ U
L : Set X
hL : IsCompact L
hKL : K ⊆ interior L
hLU : L ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U

Tactic:
exact ⟨L, by rwa [← subset_interior_iff_mem_nhdsSet], hL, hLU⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
hf.surjective.forall.2 fun x U hU ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, IsOpenQuotientMap.surjective
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
refine : ∀ (x : X) (U : Set Y) (hU : U ∈ 𝓝 (f x)), ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
refine hf.surjective.forall.2 fun x U hU ↦ ?_

Premises used: Iff.mpr, Function.Surjective.forall, IsOpenQuotientMap.surjective
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
rcases : ∀ (K : Set X) (hKx : K ∈ 𝓝 x) (hKU : K ⊆ f ⁻¹' U) (hKc : IsCompact K), ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Tactic:
rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩

Premises used: IsOpenQuotientMap.continuous, Continuous.continuousAt, local_compact_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
K : Set X
hKx : K ∈ 𝓝 x
hKU : K ⊆ f ⁻¹' U
hKc : IsCompact K
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Tactic:
⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩

Premises used: Iff.mpr, IsOpenQuotientMap.continuous, IsOpenMap.image_mem_nhds, And.intro, Exists.intro, Set.image, Set.image_subset_iff, IsOpenQuotientMap.isOpenMap, IsCompact.image
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
K : Set X
hKx : K ∈ 𝓝 x
hKU : K ⊆ f ⁻¹' U
hKc : IsCompact K
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Tactic:
exact ⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
h : IsLocallyClosed (range f)
rcases :
  ∀ (U Z : Set Y) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z) (hUZ : range f = U ∩ Z), LocallyCompactSpace X
⊢ LocallyCompactSpace X

Tactic:
rcases h with ⟨U, Z, hU, hZ, hUZ⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
x : X
⊢ U ∈ 𝓝 (f x)

Tactic:
have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
rw :
  (comap f (𝓝[Z] f x)).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
⊢ (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)

Tactic:
rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]

Premises used: Topology.IsInducing.nhds_eq_comap, comap_nhdsWithin_range, nhdsWithin_inter_of_mem, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[Z] f x)).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)

Tactic:
(nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _

Premises used: Filter.HasBasis.comap, compact_basis_nhds, Filter.HasBasis.restrict_subset, nhdsWithin_hasBasis
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (comap f (𝓝[Z] f x)).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)

Tactic:
exact (nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _

Premises used: Filter.HasBasis.comap, compact_basis_nhds, Filter.HasBasis.restrict_subset, nhdsWithin_hasBasis
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
⊢ ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)

Tactic:
have (x : X) : (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U)
      (fun s ↦ f ⁻¹' (s ∩ Z)) := by
    have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
    rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]
    exact (nhdsWithin_hasBasis ((compact_basis_nhds (f x)).restrict_subset H) _).comap _
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
⊢ LocallyCompactSpace X

Tactic:
.of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_

Premises used: _private.0.Topology.IsInducing.locallyCompactSpace.match_1, Inter.inter, Set.preimage, LocallyCompactSpace.of_hasBasis, IsCompact
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
refine :
  ∀ (x : X) (s : Set Y),
    (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U → s ∈ 𝓝 (f x) → ∀ (hs : IsCompact s) (hsU : s ⊆ U), IsCompact (f ⁻¹' (s ∩ Z))
⊢ LocallyCompactSpace X

Tactic:
refine .of_hasBasis this fun x s ⟨⟨_, hs⟩, hsU⟩ ↦ ?_
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
rw : IsCompact (s ∩ Z)
rw₁ : s ∩ Z ⊆ range f
⊢ IsCompact (f ⁻¹' (s ∩ Z))

Tactic:
rw [hf.isCompact_preimage_iff]

Premises used: Topology.IsInducing.isCompact_preimage_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (s ∩ Z)

Tactic:
hs.inter_right hZ

Premises used: IsCompact.inter_right
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ s ∩ Z ⊆ U ∩ Z

Tactic:
gcongr
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst_1] U
hZ : IsClosed[inst_1] Z
hUZ : range f = U ∩ Z
this : ∀ (x : X), (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
x : X
s : Set Y
h : (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U
left : s ∈ 𝓝 (f x)
hs : IsCompact s
hsU : s ⊆ U
⊢ IsCompact (s ∩ Z)

Tactic:
exacts [hs.inter_right hZ, hUZ ▸ by gcongr]

Premises used: IsCompact.inter_right
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ LocallyCompactSpace X

Tactic:
hf.isInducing.locallyCompactSpace hf.isClosed_range.isLocallyClosed

Premises used: Topology.IsClosedEmbedding.isInducing, IsClosed.isLocallyClosed, Topology.IsInducing.locallyCompactSpace, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : LocallyCompactSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ LocallyCompactSpace X

Tactic:
hf.isInducing.locallyCompactSpace hf.isOpen_range.isLocallyClosed

Premises used: IsOpen.isLocallyClosed, Topology.IsOpenEmbedding.isOpen_range, Topology.IsOpenEmbedding.isInducing, Topology.IsInducing.locallyCompactSpace
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
s : Set X
hs rwa rwa₁ rwa₂ rwa₃ : IsLocallyClosed s
⊢ IsLocallyClosed.{u_1} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))

Tactic:
rwa [Subtype.range_val]

Premises used: Subtype.range_val
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
s : Set X
hs : IsClosed[inst] s
⊢ LocallyCompactSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isLocallyClosed.locallyCompactSpace

Premises used: IsLocallyClosed.locallyCompactSpace, IsClosed.isLocallyClosed
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
s : Set X
hs : IsOpen[inst] s
⊢ LocallyCompactSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isLocallyClosed.locallyCompactSpace

Premises used: IsLocallyClosed.locallyCompactSpace, IsOpen.isLocallyClosed
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hf : LocallyFinite f
hs : IsCompact s
choose :
  ∀ (U : (x : X) → Set X) (hxU : ∀ (x : X), U x ∈ nhds x)
    (hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}),
    Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
choose U hxU hUf using hf
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
rcases : ∀ (t : Finset X) (hsU : s ⊆ ⋃ x ∈ t, U x), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
rcases hs.elim_nhds_subcover U fun x _ => hxU x with ⟨t, -, hsU⟩

Premises used: IsCompact.elim_nhds_subcover
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
(t.finite_toSet.biUnion fun x _ => hUf x).subset ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
refine : Subset.{u_2} (α := Set ι) {i : ι | (f i ∩ s).Nonempty} (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty})
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ s).Nonempty}

Tactic:
refine (t.finite_toSet.biUnion fun x _ => hUf x).subset ?_

Premises used: Set.Finite.subset, Finset.finite_toSet, Set.Finite.biUnion
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
rcases :
  ∀ (c : X) (hct : c ∈ t) (hcx : x ∈ U c),
    Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i
⊢ Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i

Tactic:
rcases mem_iUnion₂.1 (hsU hx.2) with ⟨c, hct, hcx⟩

Premises used: Set.mem_iUnion₂, And.right, Iff.mp
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
c : X
hct : c ∈ t
hcx : x ∈ U c
⊢ Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i

Tactic:
mem_biUnion hct ⟨x, hx.1, hcx⟩

Premises used: Set.mem_biUnion, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
s : Set X
f : ι → Set X
hs : IsCompact s
U : (x : X) → Set X
hxU : ∀ (x : X), U x ∈ nhds x
hUf : ∀ (x : X), Set.Finite.{u_2} (α := ι) {i : ι | (f i ∩ U x).Nonempty}
t : Finset X
hsU : s ⊆ ⋃ x ∈ t, U x
i : ι
x : X
hx : x ∈ f i ∩ s
c : X
hct : c ∈ t
hcx : x ∈ U c
⊢ Membership.mem (γ := Set ι) (⋃ i ∈ (↑t : Set X), {i_1 : ι | (f i_1 ∩ U i).Nonempty}) i

Tactic:
exact mem_biUnion hct ⟨x, hx.1, hcx⟩
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ Set.Finite.{u_2} (α := ι) {i : ι | (f i).Nonempty}

Tactic:
simpa only [inter_univ] using hf.finite_nonempty_inter_compact isCompact_univ

Premises used: Set.inter_univ, isCompact_univ, LocallyFinite.finite_nonempty_inter_compact
-- Module: Mathlib.Topology.Compactness.LocallyFinite
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ Set.Finite.{u_2} (α := ι) univ

Tactic:
simpa only [hne] using hf.finite_nonempty_of_compact

Premises used: LocallyFinite.finite_nonempty_of_compact
-- Module: Mathlib.Topology.Compactness.NhdsKer
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
simp :
  (∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
⊢ IsCompact (nhdsKer s) ↔ IsCompact s

Tactic:
simp only [isCompact_iff_finite_subcover]

Premises used: isCompact_iff_finite_subcover
-- Module: Mathlib.Topology.Compactness.NhdsKer
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
h :
  ∀ (ι : Type u_1) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)),
    (nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
      s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
⊢ (∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    ∀ {ι : Type u_1} (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
peel with ι U hUo
-- Module: Mathlib.Topology.Compactness.NhdsKer
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
ι : Type u_1
U : ι → Set X
hUo : ∀ (i : ι), IsOpen (U i)
⊢ (nhdsKer s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), nhdsKer s ⊆ ⋃ i ∈ t, U i) ↔
    s ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
simp only [(isOpen_iUnion hUo).nhdsKer_subset,
    (isOpen_iUnion fun i ↦ isOpen_iUnion fun _ ↦ hUo i).nhdsKer_subset]

Premises used: IsOpen.nhdsKer_subset, isOpen_iUnion