awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : ∃ (I : Set ι), I.Finite ∧ ∃ (t_2 : (i : ι) → Set (X i)), (∀ (i : ι), t_2 i ∈ 𝓝 (t i)) ∧ I.pi (α := X) t_2 ⊆ n
obtain :
  ∀ (s : Set ι) (n' : (i : ι) → Set (X i)) (hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)) (hsub : s.pi (α := X) n' ⊆ n),
    ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
obtain ⟨s, -, n', hn', hsub⟩ := hn
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
choose :
  ∀ (n'' : (i : ι) → Set (X i)) (hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)) (hsub' : ∀ (i : ι), n'' i ⊆ n' i)
    (hc : ∀ (i : ι), IsCompact (n'' i)), ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)

Premises used: LocallyCompactSpace.local_compact_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩

Premises used: Set.univ, subset_trans, isCompact_univ_pi, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
refine_1 : Set.pi (α := X) univ n'' ∈ 𝓝 t
refine_2 : ∀ (x : (i : ι) → X i) (h : x ∈ Set.pi (α := X) univ n''), x ∈ s.pi (α := X) n'
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ Set.pi (α := X) univ n'' ∈ 𝓝 t

Tactic:
(set_pi_mem_nhds_iff (@Set.finite_univ ι _) _).mpr fun i _ => hn'' i

Premises used: Iff.mpr, Set.finite_univ, set_pi_mem_nhds_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ Set.pi (α := X) univ n'' ∈ 𝓝 t

Tactic:
exact (set_pi_mem_nhds_iff (@Set.finite_univ ι _) _).mpr fun i _ => hn'' i

Premises used: Iff.mpr, Set.finite_univ, set_pi_mem_nhds_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x : (i : ι) → X i
h : x ∈ Set.pi (α := X) univ n''
⊢ x ∈ s.pi (α := X) n'

Tactic:
fun i _ => hsub' i (h i trivial)

Premises used: trivial, Set.Mem, setOf, Set.pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x : (i : ι) → X i
h : x ∈ Set.pi (α := X) univ n''
⊢ x ∈ s.pi (α := X) n'

Tactic:
exact fun i _ => hsub' i (h i trivial)

Premises used: trivial
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ (I : Set ι), I.Finite ∧ ∃ (t_2 : (i : ι) → Set (X i)), (∀ (i : ι), t_2 i ∈ 𝓝 (t i)) ∧ I.pi (α := X) t_2 ⊆ n

Tactic:
rw [nhds_pi, Filter.mem_pi] at hn

Premises used: nhds_pi, Filter.mem_pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : ∃ (I : Set ι), I.Finite ∧ ∃ (t_2 : (i : ι) → Set (X i)), (∀ (i : ι), t_2 i ∈ 𝓝 (t i)) ∧ I.pi (α := X) t_2 ⊆ n
obtain :
  ∀ (s : Set ι) (hs : s.Finite) (n' : (i : ι) → Set (X i)) (hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i))
    (hsub : s.pi (α := X) n' ⊆ n), ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
obtain ⟨s, hs, n', hn', hsub⟩ := hn
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
choose :
  ∀ (n'' : (i : ι) → Set (X i)) (hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)) (hsub' : ∀ (i : ι), n'' i ⊆ n' i)
    (hc : ∀ (i : ι), IsCompact (n'' i)), ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)

Premises used: LocallyCompactSpace.local_compact_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩

Premises used: subset_trans, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
refine_1 : s.pi (α := X) n'' ∈ 𝓝 t
refine_2 : ∀ x ∈ s.pi (α := X) n'', x ∈ s.pi (α := X) n'
refine_3 : IsCompact (s.pi (α := X) n'')
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ s.pi (α := X) n'' ∈ 𝓝 t

Tactic:
(set_pi_mem_nhds_iff hs _).mpr fun i _ => hn'' i

Premises used: Iff.mpr, set_pi_mem_nhds_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ s.pi (α := X) n'' ∈ 𝓝 t

Tactic:
exact (set_pi_mem_nhds_iff hs _).mpr fun i _ => hn'' i

Premises used: Iff.mpr, set_pi_mem_nhds_iff
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x : (i : ι) → X i
⊢ x ∈ s.pi (α := X) n'' → x ∈ s.pi (α := X) n'

Tactic:
forall₂_imp fun i _ hi' => hsub' i hi'

Premises used: Set.Mem, forall₂_imp, setOf, Set.pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x : (i : ι) → X i
⊢ x ∈ s.pi (α := X) n'' → x ∈ s.pi (α := X) n'

Tactic:
exact forall₂_imp fun i _ hi' => hsub' i hi'

Premises used: forall₂_imp
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
refine_3 : IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)
⊢ IsCompact (s.pi (α := X) n'')

Tactic:
rw [← Set.univ_pi_ite]

Premises used: Set.univ_pi_ite
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)

Tactic:
isCompact_univ_pi fun i => ?_

Premises used: isCompact_univ_pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
refine_3 : ∀ (i : ι), IsCompact (if i ∈ s then n'' i else univ)
⊢ IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)

Tactic:
refine isCompact_univ_pi fun i => ?_

Premises used: isCompact_univ_pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
pos : ∀ (h : i ∈ s), IsCompact (if i ∈ s then n'' i else univ)
neg : ∀ (h : i ∉ s), IsCompact (if i ∈ s then n'' i else univ)
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
by_cases h : i ∈ s
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∈ s
pos : IsCompact (n'' i)
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
rw [if_pos h]

Premises used: if_pos
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∈ s
⊢ IsCompact (n'' i)

Tactic:
hc i
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∈ s
⊢ IsCompact (n'' i)

Tactic:
exact hc i
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
neg : IsCompact.{u_4} (X := X i) univ
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
rw [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
⊢ IsCompact.{u_4} (X := X i) univ

Tactic:
CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
⊢ IsCompact.{u_4} (X := X i) univ

Tactic:
exact CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t_1 : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : ∀ (i : ι), CompactSpace.{u_4} (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi (α := X) n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
refine_3 refine_3₁ refine_3₂ :
  IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)
refine_3₃ : ∀ (i : ι), IsCompact (if i ∈ s then n'' i else univ)
pos : ∀ (i : ι) (h : i ∈ s), IsCompact (if i ∈ s then n'' i else univ)
neg neg₁ : ∀ (i : ι) (h : i ∉ s), IsCompact (if i ∈ s then n'' i else univ)
⊢ IsCompact (s.pi (α := X) n'')

Tactic:
classical
      rw [← Set.univ_pi_ite]
      refine isCompact_univ_pi fun i => ?_
      by_cases h : i ∈ s
      · rw [if_pos h]
        exact hc i
      · rw [if_neg h]
        exact CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ, isCompact_univ_pi, Set.univ_pi_ite
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : Finite ι
inst_5 : LocallyCompactSpace Y
⊢ LocallyCompactSpace (ι → Y)

Tactic:
Pi.locallyCompactSpace_of_finite

Premises used: Pi.locallyCompactSpace_of_finite
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), LocallyCompactSpace.{u_4} (X i)
inst_4 : LocallyCompactSpace Y
inst_5 : CompactSpace Y
⊢ LocallyCompactSpace (ι → Y)

Tactic:
Pi.locallyCompactSpace

Premises used: Pi.locallyCompactSpace
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst] U
hx : x ∈ U
rcases :
  ∀ (K : Set X) (h1K : K ∈ 𝓝 x) (h2K : K ⊆ U) (h3K : IsCompact K), ∃ (K : Set X), IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
⊢ ∃ (K : Set X), IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
rcases LocallyCompactSpace.local_compact_nhds x U (hU.mem_nhds hx) with ⟨K, h1K, h2K, h3K⟩

Premises used: LocallyCompactSpace.local_compact_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst] U
hx : x ∈ U
K : Set X
h1K : K ∈ 𝓝 x
h2K : K ⊆ U
h3K : IsCompact K
⊢ ∃ (K : Set X), IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
x : X
U : Set X
hU : IsOpen[inst] U
hx : x ∈ U
K : Set X
h1K : K ∈ 𝓝 x
h2K : K ⊆ U
h3K : IsCompact K
⊢ ∃ (K : Set X), IsCompact K ∧ x ∈ interior K ∧ K ⊆ U

Tactic:
exact ⟨K, h3K, mem_interior_iff_mem_nhds.2 h1K, h2K⟩