awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t_2 : Set X
h : t_2 ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t_2 ⊆ ⋃ (i : ι), U i
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
right : t_2 ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Set ι), t.Countable ∧ t_2 ⊆ ⋃ i ∈ t, U i

Tactic:
use t, htc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t_2 : Set X
h : t_2 ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t_2 ⊆ ⋃ (i : ι), U i
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ t_2 ⊆ ⋃ i ∈ t, U i

Tactic:
subset_of_subset_of_eq hcover (id htu.symm)

Premises used: subset_of_subset_of_eq, id, Eq.symm
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι_1 : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t_1 : Set X
inst_2 : SecondCountableTopology X
t_2 : Set X
h : t_2 ⊆ univ
x : Filter X
ι : Type u
U : ι → Set X
hι : ∀ (i : ι), IsOpen[inst] (U i)
hcover : t_2 ⊆ ⋃ (i : ι), U i
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ t_2 ⊆ ⋃ i ∈ t, U i

Tactic:
exact subset_of_subset_of_eq hcover (id htu.symm)

Premises used: subset_of_subset_of_eq, id, Eq.symm
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
⊢ IsLindelof.{u} (X := X) (⋃ (i : ι), U i)

Tactic:
have : IsLindelof (⋃ i, U i) := HereditarilyLindelofSpace.isLindelof (⋃ i, U i)
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
rcases :
  ∀ (t : Set ι) (htc : t.Countable) (htu : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)),
    ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)

Tactic:
rcases this.elim_countable_subcover U h (Eq.subset rfl) with ⟨t, ⟨htc, htu⟩⟩

Premises used: Eq.subset, IsLindelof.elim_countable_subcover, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
t : Set ι
htc : t.Countable
htu : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)
right : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)

Tactic:
use t, htc
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
this : IsLindelof.{u} (X := X) (⋃ (i : ι), U i)
t : Set ι
htc : t.Countable
htu : Subset.{u} (α := Set X) (⋃ (i : ι), U i) (⋃ i ∈ t, U i)
⊢ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)

Tactic:
apply eq_of_subset_of_subset (iUnion₂_subset_iUnion (fun i ↦ i ∈ t) fun i ↦ U i) htu

Premises used: Membership.mem, Set.iUnion₂_subset_iUnion, Set.eq_of_subset_of_subset
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
obtain :
  ∀ (t : Set ι) (htc : t.Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)),
    ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
obtain ⟨t, htc, htu⟩ := eq_open_union_countable U h

Premises used: eq_open_union_countable
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
inl :
  ∀ (htc : Set.Countable.{u_2} (α := ι) ∅)
    (htu : Eq.{u + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i) (⋃ (i : ι), U i)),
    ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
inr : ∀ (t_ne : t.Nonempty), ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
rcases eq_empty_or_nonempty t with rfl | t_ne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
htc : Set.Countable.{u_2} (α := ι) ∅
htu : Eq.{u + 1} (α := Set X) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), U i) (⋃ (i : ι), U i)
⊢ ∀ (i : ι), U i = ∅

Tactic:
simp_rw [mem_empty_iff_false, iUnion_false, iUnion_empty, eq_comm (a := ∅), iUnion_eq_empty]
      at htu

Premises used: eq_comm, Set.iUnion_eq_empty, Set.iUnion_false, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
htc : Set.Countable.{u_2} (α := ι) ∅
htu : ∀ (i : ι), U i = ∅
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
simp [htu]
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
t : Set ι
htc : t.Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, U i) (⋃ (i : ι), U i)
t_ne : t.Nonempty
inr :
  ∀ (k : ℕ → ι) (htc : (range k).Countable) (htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i))
    (t_ne : (range k).Nonempty), ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
obtain ⟨k, rfl⟩ := htc.exists_eq_range t_ne

Premises used: Set.Countable.exists_eq_range, rfl
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i)
t_ne : (range k).Nonempty
h₁ : Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
use k
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (U i)
k : ℕ → ι
htc : (range k).Countable
htu : Eq.{u + 1} (α := Set X) (⋃ i ∈ range k, U i) (⋃ (i : ι), U i)
t_ne : (range k).Nonempty
h₁ h₂ h₃ h₄ :
  ∀ (htu : Eq.{u + 1} (α := Set X) (⋃ (y : ℕ), U (k y)) (⋃ (i : ι), U i)) (t_ne : (range k).Nonempty),
    Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)
⊢ Eq.{u + 1} (α := Set X) (⋃ (n : ℕ), U (k n)) (⋃ (i : ι), U i)

Tactic:
rwa [biUnion_range] at htu

Premises used: Set.biUnion_range
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
rw : Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i)ᶜ (⋂ (i : ι), C i)ᶜ
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
simp : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i)ᶜ (⋂ (i : ι), C i)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
t : Set ι
rw : Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
| Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)

Tactic:
rw [← compl_inj_iff]; simp

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
conv : ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋂ i ∈ t, C i) (⋂ (i : ι), C i)

Tactic:
conv in _ = _ => rw [← compl_inj_iff]; simp

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)

Tactic:
eq_open_union_countable (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

Premises used: IsClosed.isOpen_compl, Compl.compl, eq_open_union_countable
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (t : Set ι), t.Countable ∧ Eq.{u + 1} (α := Set X) (⋃ i ∈ t, (C i)ᶜ) (⋃ (i : ι), (C i)ᶜ)

Tactic:
exact eq_open_union_countable (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

Premises used: IsClosed.isOpen_compl, Compl.compl, eq_open_union_countable
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
rw : Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n))ᶜ (⋂ (i : ι), C i)ᶜ
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
simp : Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n))ᶜ (⋂ (i : ι), C i)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
k : ℕ → ι
rw : Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
| Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)

Tactic:
rw [← compl_inj_iff]; simp

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
conv : ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋂ (n : ℕ), C (k n)) (⋂ (i : ι), C i)

Tactic:
conv in _ = _ => rw [← compl_inj_iff]; simp

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)

Tactic:
eq_open_union_nat (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

Premises used: IsClosed.isOpen_compl, Compl.compl, eq_open_union_nat
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : HereditarilyLindelofSpace X
ι : Type u_2
inst_2 : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst] (C i)
⊢ ∃ (k : ℕ → ι), Eq.{u + 1} (α := Set X) (⋃ (i : ℕ), (C (k i))ᶜ) (⋃ (i : ι), (C i)ᶜ)

Tactic:
exact eq_open_union_nat (fun i ↦ (C i)ᶜ) (fun i ↦ (h i).isOpen_compl)

Premises used: IsClosed.isOpen_compl, Compl.compl, eq_open_union_nat
-- Module: Mathlib.Topology.Compactness.Lindelof
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
inst_2 : HereditarilyLindelofSpace X
p : X → Prop
⊢ HereditarilyLindelofSpace.{u} { x : X // p x }

Tactic:
HereditarilyLindelofSpace.of_forall_isOpen fun _ _ =>
    Subtype.isLindelof_iff.2 <| HereditarilyLindelofSpace.isLindelof _

Premises used: Iff.mpr, HereditarilyLindelofSpace.of_forall_isOpen, Subtype.isLindelof_iff, HereditarilyLindelofSpace.isLindelof, Set.image, Subtype.val
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι_1 : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
ι : Type u_4
inst_2 : Finite ι
X : ι → Type u_5
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_5} (X i)
f : (i : ι) → X i
choose :
  ∀ (s : (i : ι) → Set (X i)) (hsc : ∀ (i : ι), IsCompact (s i)) (hs : ∀ (i : ι), s i ∈ 𝓝 (f i)),
    ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f
⊢ ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f

Tactic:
choose s hsc hs using fun i ↦ exists_compact_mem_nhds (f i)

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι_1 : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t : Set X_1
ι : Type u_4
inst_2 : Finite ι
X : ι → Type u_5
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_5} (X i)
f : (i : ι) → X i
s : (i : ι) → Set (X i)
hsc : ∀ (i : ι), IsCompact (s i)
hs : ∀ (i : ι), s i ∈ 𝓝 (f i)
⊢ ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f

Tactic:
⟨pi univ s, isCompact_univ_pi hsc, set_pi_mem_nhds univ.toFinite fun i _ ↦ hs i⟩

Premises used: set_pi_mem_nhds, Set.univ, isCompact_univ_pi, Set.toFinite, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι_1 : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s_1 t : Set X_1
ι : Type u_4
inst_2 : Finite ι
X : ι → Type u_5
inst_3 : (i : ι) → TopologicalSpace (X i)
inst_4 : ∀ (i : ι), WeaklyLocallyCompactSpace.{u_5} (X i)
f : (i : ι) → X i
s : (i : ι) → Set (X i)
hsc : ∀ (i : ι), IsCompact (s i)
hs : ∀ (i : ι), s i ∈ 𝓝 (f i)
⊢ ∃ (s : Set ((i : ι) → X i)), IsCompact s ∧ s ∈ 𝓝 f

Tactic:
exact ⟨pi univ s, isCompact_univ_pi hsc, set_pi_mem_nhds univ.toFinite fun i _ ↦ hs i⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
s : Set X
hs : IsClosed[inst] s
⊢ WeaklyLocallyCompactSpace.{u_1} (↑s : Type u_1)

Tactic:
hs.isClosedEmbedding_subtypeVal.weaklyLocallyCompactSpace

Premises used: Topology.IsClosedEmbedding.weaklyLocallyCompactSpace, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 x

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

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 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
refine : ∀ (x : X), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)
⊢ ∀ (x : Y), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 x

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

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 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
rcases : ∀ (K : Set X) (hKc : IsCompact K) (hKx : K ∈ 𝓝 x), ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)
⊢ ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_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 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)

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

Premises used: IsOpenQuotientMap.continuous, IsOpenMap.image_mem_nhds, And.intro, Exists.intro, Set.image, 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 : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ (s : Set Y), IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
choose :
  ∀ (s : (x : X) → Set X) (hc : ∀ (x : X), IsCompact (s x)) (hmem : ∀ (x : X), s x ∈ 𝓝 x),
    ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'

Tactic:
choose s hc hmem using fun x : X ↦ exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : (x : X) → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
rcases : ∀ (I : Finset X) (hIK : K ⊆ ⋃ x ∈ I, interior (s x)), ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'

Tactic:
rcases hK.elim_nhds_subcover _ fun x _ ↦ interior_mem_nhds.2 (hmem x) with ⟨I, -, hIK⟩

Premises used: Iff.mpr, IsCompact.elim_nhds_subcover, interior_mem_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : (x : X) → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'

Tactic:
⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩

Premises used: HasSubset.Subset.trans, Finset.isCompact_biUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : (x : X) → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
refine : Subset.{u_1} (α := Set X) (⋃ x ∈ I, interior (s x)) (interior (⋃ x ∈ I, s x))
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'

Tactic:
refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : (x : X) → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ Subset.{u_1} (α := Set X) (⋃ x ∈ I, interior (s x)) (interior (⋃ x ∈ I, s x))

Tactic:
iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx

Premises used: Set.subset_iUnion₂, Set.iUnion₂_subset, interior_mono
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
K : Set X
hK : IsCompact K
s : (x : X) → Set X
hc : ∀ (x : X), IsCompact (s x)
hmem : ∀ (x : X), s x ∈ 𝓝 x
I : Finset X
hIK : K ⊆ ⋃ x ∈ I, interior (s x)
⊢ Subset.{u_1} (α := Set X) (⋃ x ∈ I, interior (s x)) (interior (⋃ x ∈ I, s x))

Tactic:
exact iUnion₂_subset fun x hx ↦ interior_mono <| subset_iUnion₂ (s := fun x _ ↦ s x) x hx

Premises used: Set.subset_iUnion₂, Set.iUnion₂_subset, interior_mono
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : WeaklyLocallyCompactSpace X
x : X
⊢ Disjoint (𝓝 x) (cocompact X)

Tactic:
let ⟨_, hc, hx⟩ := exists_compact_mem_nhds x
  disjoint_of_disjoint_of_mem disjoint_compl_right hx hc.compl_mem_cocompact

Premises used: IsCompact.compl_mem_cocompact, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, Disjoint, nhds, Filter.disjoint_of_disjoint_of_mem, Filter.cocompact, disjoint_compl_right, _private.0.disjoint_nhds_cocompact.match_1
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsCompact r ∧ r ⊆ t

Tactic:
simpa only [and_comm] using LocallyCompactSpace.local_compact_nhds x

Premises used: and_comm, LocallyCompactSpace.local_compact_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
x : X
n : Set X
h : n ∈ 𝓝 x
⊢ ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
LocallyCompactSpace.local_compact_nhds _ _ h

Premises used: LocallyCompactSpace.local_compact_nhds
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : X → Type u_4
p : (x : X) → ι x → Prop
s : (x : X) → ι x → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
hc : ∀ (x : X) (i : ι x), p x i → IsCompact (s x i)
⊢ LocallyCompactSpace X

Tactic:
⟨fun x _t ht =>
    let ⟨i, hp, ht⟩ := (h x).mem_iff.1 ht
    ⟨s x i, (h x).mem_of_mem hp, ht, hc x i hp⟩⟩

Premises used: Filter.HasBasis.mem_iff, Membership.mem, Exists, nhds, HasSubset.Subset, And, And.intro, Exists.intro, Iff.mp, _private.0.LocallyCompactSpace.of_hasBasis.match_1, LocallyCompactSpace.mk, Filter.HasBasis.mem_of_mem, IsCompact
-- Module: Mathlib.Topology.Compactness.LocallyCompact
Goal:
X_1 : Type u_1
Y_1 : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y_1
s t : Set X_1
X : Type u_4
Y : Type u_5
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : LocallyCompactSpace X
inst_5 : LocallyCompactSpace Y
⊢ LocallyCompactSpace (X × Y)

Tactic:
have := fun x : X × Y => (compact_basis_nhds x.1).prod_nhds' (compact_basis_nhds x.2)
  .of_hasBasis this fun _ _ ⟨⟨_, h₁⟩, _, h₂⟩ => h₁.prod h₂

Premises used: SProd.sprod, IsCompact.prod, Prod.fst, compact_basis_nhds, LocallyCompactSpace.of_hasBasis, Prod.snd, _private.0.Prod.locallyCompactSpace.match_1, Filter.HasBasis.prod_nhds', IsCompact
-- 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 : 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