awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ (K' : Set X), IsCompact K' ∧ K ⊆ interior K'
have rcases : ∀ (I : Finset X) (hIK : K ⊆ ⋃ x ∈ I, interior (s x)), ∃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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'
have refine : Subset.{u_1} (α := Set X) (⋃ x ∈ I, interior (s x)) (interior (⋃ x ∈ I, s x))
Tactic: refine ⟨⋃ x ∈ I, s x, I.isCompact_biUnion fun _ _ ↦ hc _, hIK.trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (hypothesis)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have hn₁ : ∃ (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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have 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
Tactic: obtain ⟨s, -, n', hn', hsub⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have 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
Tactic: choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
have refine_1 : Set.pi (α := X) univ n'' ∈ 𝓝 t
Tactic: refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have refine_2 : ∀ (x : (i : ι) → X i) (h : x ∈ Set.pi (α := X) univ n''), x ∈ s.pi (α := X) n'
Tactic: refine ⟨(Set.univ : Set ι).pi n'', ?_, subset_trans (fun _ h => ?_) hsub, isCompact_univ_pi hc⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (hypothesis)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have hn₁ : ∃ (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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have 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
Tactic: obtain ⟨s, hs, n', hn', hsub⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have 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
Tactic: choose n'' hn'' hsub' hc using fun i =>
      LocallyCompactSpace.local_compact_nhds (t i) (n' i) (hn' i)
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
have refine_1 : s.pi (α := X) n'' ∈ 𝓝 t
Tactic: refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have refine_2 : ∀ x ∈ s.pi (α := X) n'', x ∈ s.pi (α := X) n'
Tactic: refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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'
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
have refine_3 : IsCompact (s.pi (α := X) n'')
Tactic: refine ⟨s.pi n'', ?_, subset_trans (fun _ => ?_) hsub, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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 (s.pi (α := X) n'')
have refine_3 : IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)
Tactic: rw [← Set.univ_pi_ite]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
have refine_3 : ∀ (i : ι), IsCompact (if i ∈ s then n'' i else univ)
Tactic: refine isCompact_univ_pi fun i => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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 : ι
⊢ IsCompact (if i ∈ s then n'' i else univ)
have pos : ∀ (h : i ∈ s), IsCompact (if i ∈ s then n'' i else univ)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ IsCompact (if i ∈ s then n'' i else univ)
have neg : ∀ (h : i ∉ s), IsCompact (if i ∈ s then n'' i else univ)
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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 (if i ∈ s then n'' i else univ)
have pos : IsCompact (n'' i)
Tactic: rw [if_pos h]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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 (if i ∈ s then n'' i else univ)
have neg : IsCompact.{u_4} (X := X i) univ
Tactic: rw [if_neg h]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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 (s.pi (α := X) n'')
have refine_3 : IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ if i ∈ s then n'' i else univ)
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ IsCompact (s.pi (α := X) n'')
have refine_3₃ : ∀ (i : ι), IsCompact (if i ∈ s then n'' i else univ)
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ IsCompact (s.pi (α := X) n'')
have pos : ∀ (i : ι) (h : i ∈ s), IsCompact (if i ∈ s then n'' i else univ)
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ IsCompact (s.pi (α := X) n'')
have neg : ∀ (i : ι) (h : i ∉ s), IsCompact (if i ∈ s then n'' i else univ)
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
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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), IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
have rcases : ∀ (K : Set X) (h1K : K ∈ 𝓝 x) (h2K : K ⊆ U) (h3K : IsCompact K), ∃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
have 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
Tactic: choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
    exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
have rcases : ∀ (s : Finset X) (hsK : ∀ x ∈ s, x ∈ K) (hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K), ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
Tactic: rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun (L : Set X) ↦ L ∈ 𝓝ˢ K ∧ IsCompact L) id
have rw : ∀ (i : Set X), IsOpen[inst] i ∧ K ⊆ i → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ i
Tactic: rw [hasBasis_self, (hasBasis_nhdsSet _).forall_iff (by grind)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
⊢ IsOpen[inst] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
have this : ∀ (hU : IsOpen[inst] U) (h_KU : K ⊆ U), ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
Tactic: ⟨hU, h_KU⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
⊢ ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
have obtain : ∀ (L : Set X) (hL : IsCompact L) (hKL : K ⊆ interior L) (hLU : L ⊆ U), ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
Tactic: obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between hK hU h_KU
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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
have refine : ∀ (x : X) (U : Set Y) (hU : U ∈ 𝓝 (f x)), ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
Tactic: refine hf.surjective.forall.2 fun x U hU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
have rcases : ∀ (K : Set X) (hKx : K ∈ 𝓝 x) (hKU : K ⊆ f ⁻¹' U) (hKc : IsCompact K), ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
Tactic: rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ LocallyCompactSpace X
have rcases : ∀ (U Z : Set Y) (hU : IsOpen[inst_1] U) (hZ : IsClosed[inst_1] Z) (hUZ : range f = U ∩ Z), LocallyCompactSpace X
Tactic: rcases h with ⟨U, Z, hU, hZ, hUZ⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (hypothesis)
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)
have H : U ∈ 𝓝 (f x)
Tactic: have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1
-- Lean 4 proof step from Mathlib.Topology.Compactness.LocallyCompact (goal)
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)
⊢ (𝓝 x).HasBasis (fun (s : Set Y) ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun (s : Set Y) ↦ f ⁻¹' (s ∩ Z)
have 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)
Tactic: rw [hf.nhds_eq_comap, ← comap_nhdsWithin_range, hUZ,
      nhdsWithin_inter_of_mem (nhdsWithin_le_nhds H)]