awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
s : Finset (Finset ι)
hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}
refine :
  Subset.{u_1} (α := Set α)
    (⋃ (x : Compacts α),
      ⋃ (_ : Membership.mem (γ := Set (Compacts α)) (⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}) x),
        (↑x : Set α))
    (⋃ i ∈ s.biUnion id, U i)
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
have refine₁ : ∀ (i : Finset ι) (i_1 : i ∈ s) (i_2 : Compacts α)
  (i : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_3 ∈ i, U i_3} i_2),
  (↑i_2 : Set α) ⊆ ⋃ x ∈ s, ⋃ y ∈ id x, U y
Tactic: classical
  refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
  simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
  exact fun t ht K hK => subset_iUnion₂_of_subset t ht hK
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ CompactSpace.{u_1} (Compacts α) ↔ CompactSpace α
have refine : ∀ (h : CompactSpace.{u_1} (Compacts α)), IsCompact.{u_1} (X := α) univ
Tactic: refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ IsCompact.{u_1} (X := α) univ
have h₁ : Eq.{u_1 + 1} (α := Set α) univ (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
Tactic: convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
have h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α)) univ
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (Compacts α)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (K : Compacts α), ⋃ (_ : Membership.mem (γ := Set (Compacts α)) univ K), (↑K : Set α))
    univ
have h₁ : ∀ (x : α), ∃ (i : Compacts α), x ∈ (↑i : Set α)
Tactic: simp_rw [biUnion_univ, eq_univ_iff_forall, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoncompactSpace.{u_1} (Compacts α) ↔ NoncompactSpace α
have simp_rw : ¬CompactSpace.{u_1} (Compacts α) ↔ ¬CompactSpace α
Tactic: simp_rw [← not_compactSpace_iff, compactSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
⊢ LocallyCompactSpace.{u_1} (Compacts α)
have refine : ∀ (K : Compacts α) (U : Set (Compacts α)) (hU : U ∈ 𝓝 K), ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
Tactic: refine ⟨fun K U hU => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU : U ∈ 𝓝 K
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
have hU₁ : ∃ (x : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
    Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
        K ∧
      {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} ⊆ U
Tactic: rw [isTopologicalBasis.mem_nhds_iff, exists_mem_image] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
hU :
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x ∧
      Membership.mem (γ := Set (Compacts α))
          {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} ⊆ U
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
have obtain : ∀ (u : Set (Set α)) (hu₁ : u.Finite) (hu₂ : ∀ U ∈ u, IsOpen[inst] U)
  (huU : {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ⊆ U) (hKu₁ : (↑K : Set α) ⊆ ⋃₀ u)
  (hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty), ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
Tactic: obtain ⟨u, ⟨hu₁, hu₂⟩, ⟨hKu₁, hKu₂⟩, huU⟩ := hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
U : Set (Compacts α)
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
huU : {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ⊆ U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ U ∧ IsCompact s
have grw : ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
Tactic: grw [← huU]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
have obtain : ∀ (L : Set α) (hL : IsCompact L) (hLK : (↑K : Set α) ⊆ interior L) (hLu : L ⊆ ⋃₀ u),
  ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
Tactic: obtain ⟨L, hL, hLK, hLu⟩ := exists_compact_between K.isCompact (isOpen_sUnion hu₂) hKu₁
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
⊢ ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
have obtain : ∀ (x : α) (hxK : x ∈ (↑K : Set α)) (hxU : x ∈ U),
  ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
Tactic: obtain ⟨x, hxK, hxU⟩ := hKu₂ U hU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
U : Set α
hU : U ∈ u
x : α
hxK : x ∈ (↑K : Set α)
hxU : x ∈ U
⊢ ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
have obtain : ∀ (M : Set α) (hM : IsCompact M),
  x ∈ interior M ∧ M ⊆ U ∩ interior L →
    ∃ (M : Set α), IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ ((↑K : Set α) ∩ interior M).Nonempty
Tactic: obtain ⟨M, hM, _⟩ := exists_compact_subset (U := U ∩ interior L)
        ((hu₂ U hU).inter isOpen_interior) ⟨hxU, hLK hxK⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
have choose! : ∀ (M : (U : Set α) → Set α) (hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U))
  (hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L) (hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U)
  (hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty),
  ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
Tactic: choose! M hM hML hMU hMK using fun U (hU : U ∈ u) =>
    show ∃ M : Set α, IsCompact M ∧ M ⊆ L ∧ M ⊆ U ∧ (↑K ∩ interior M).Nonempty by
      obtain ⟨x, hxK, hxU⟩ := hKu₂ U hU
      obtain ⟨M, hM, _⟩ := exists_compact_subset (U := U ∩ interior L)
        ((hu₂ U hU).inter isOpen_interior) ⟨hxU, hLK hxK⟩
      exact ⟨M, hM, by grind [interior_subset], by grind, x, by grind⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ Subset.{u_1} (α := Set (Compacts α)) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}
    {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have a : ∀ (a : Compacts α), (↑a : Set α) ⊆ L → ∀ a ∈ u, M a ⊆ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
have refine_1 : {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ∈ 𝓝 K
Tactic: refine ⟨{K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}, ?_, by gcongr; grind, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
refine_1 : {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ∈ 𝓝 K
⊢ ∃ s ∈ 𝓝 K, s ⊆ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} ∧ IsCompact s
have refine_2 : IsCompact.{u_1} (X := Compacts α) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}
Tactic: refine ⟨{K' | ↑K' ⊆ L ∧ ∀ U ∈ u, (↑K' ∩ M U).Nonempty}, ?_, by gcongr; grind, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ∈ 𝓝 K
have h : ∀ (K' : Compacts α) (h₁ : (↑K' : Set α) ⊆ interior L) (h₂ : ∀ i ∈ u, ((↑K' : Set α) ∩ interior (M i)).Nonempty),
  (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty
Tactic: filter_upwards [
      (isOpen_subsets_of_isOpen isOpen_interior).mem_nhds hLK,
      (Filter.eventually_all_finite hu₁).mpr fun U hU =>
        (isOpen_inter_nonempty_of_isOpen isOpen_interior).mem_nhds (hMK U hU)] with K' h₁ h₂
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ IsCompact.{u_1} (X := Compacts α) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}
have refine_2 : IsCompact
  (image (α := Compacts α) SetLike.coe {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty})
Tactic: rw [isEmbedding_coe.isCompact_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ IsCompact
    (image (α := Compacts α) SetLike.coe
      {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty})
have refine_2 : ∀ (s : Set α),
  Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s →
    ∀ (hsL : s ⊆ L) (hsu : ∀ L ∈ M '' u, (s ∩ L).Nonempty),
      ∃
        y ∈
          image (α := Compacts α) SetLike.coe
            {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
        s ⤳ y
Tactic: refine vietoris.isCompact_aux hL (s := M '' u) (by grind) (by grind)
      |>.of_subset_of_specializes (by grind) (fun s ⟨hsL, hsu⟩ => ?_)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ L ∈ M '' u, (s ∩ L).Nonempty
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y
have hsu₁ : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
Tactic: rw [forall_mem_image] at hsu
Cleared hypotheses: hsu
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y
have refine_2 : ∀ (U : Set α) (hU : U ∈ u), s ∩ M U ⊆ (↑s' : Set α) ∩ M U
Tactic: refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
refine_2 : ∀ (U : Set α) (hU : U ∈ u), s ∩ M U ⊆ (↑s' : Set α) ∩ M U
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y
have refine_2₁ : s ⊆ (↑s' : Set α)
Tactic: refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
refine_2 : ∀ (U : Set α) (hU : U ∈ u), s ∩ M U ⊆ (↑s' : Set α) ∩ M U
refine_2₁ : s ⊆ (↑s' : Set α)
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y
have refine_2₂ : (↑s' : Set α) ⊆ closure[inst] s
Tactic: refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClosed.{u_1} (X := Compacts α) (range toCompacts)
have rw : IsClosed (X := Compacts α) {⊥}ᶜ
Tactic: rw [range_toCompacts]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsOpen.{u_1} (X := Compacts α) (range toCompacts)
have rw : IsOpen (X := Compacts α) {⊥}ᶜ
Tactic: rw [range_toCompacts]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis.{u_1} (α := NonemptyCompacts α)
    ((fun (u : Set (Set α)) ↦ {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
have refine_1 : ∀ (u : Set (NonemptyCompacts α)),
  Membership.mem (γ := Set (Set (NonemptyCompacts α)))
      ((fun (u : Set (Set α)) ↦
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
        {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
      u →
    IsOpen u
Tactic: refine hB.compacts.isInducing isEmbedding_toCompacts.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_1 :
  ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        u →
      IsOpen u
⊢ IsTopologicalBasis.{u_1} (α := NonemptyCompacts α)
    ((fun (u : Set (Set α)) ↦ {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
have refine_2 : ∀ (u : Set (NonemptyCompacts α)),
  Membership.mem (γ := Set (Set (NonemptyCompacts α)))
      (preimage toCompacts ''
        (fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
      u →
    ∀ x ∈ u,
      ∃ (v : Set (NonemptyCompacts α)),
        Membership.mem (γ := Set (Set (NonemptyCompacts α)))
            ((fun (u : Set (Set α)) ↦
                {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
            v ∧
          x ∈ v ∧ v ⊆ u
Tactic: refine hB.compacts.isInducing isEmbedding_toCompacts.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        u →
      IsOpen u
have refine_1 : ∀ ⦃x : Set (Set α)⦄,
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x →
    IsOpen.{u_1} (X := NonemptyCompacts α)
      {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
Tactic: simp_rw [forall_mem_image]