awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
⊢ ∃ y ∈ t, x ⤳ y
have refine_1 : ∀ (y : α) (hyt : y ∈ t) (hxy : Membership.mem (γ := Set α) (closure[inst] {x}) y), ∃ y ∈ t, x ⤳ y
Tactic: obtain ⟨y, hyt, hxy⟩ := h.mem_closed (s := {u | (u ∩ closure {x}).Nonempty})
      (isClosed_inter_nonempty_of_isClosed isClosed_closure) ⟨x, hx, subset_closure rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
⊢ s ⤳ t
have refine_2 : ∀ (i : Set (Set α))
  (j :
    Membership.mem (γ := Set (Set (Set α)))
      {s : Set (Set α) |
        t ∈ s ∧
          Membership.mem (γ := Set (Set (Set α)))
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
            s}
      i),
  ⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1 ≤
    Filter.principal i
Tactic: simp_rw [Specializes, nhds_generateFrom, le_iInf₂_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
⊢ ⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1 ≤
    Filter.principal (𝒫 U)
have refine_2 : ∀ (x : α) (hx : x ∈ s), x ∈ U
Tactic: refine iInf₂_le U.powerset ⟨fun x hx => ?_, .inl <| mem_image_of_mem _ hU⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
x : α
hx : x ∈ s
⊢ x ∈ U
have refine_2 : ∀ (y : α) (hyt : y ∈ t) (hxy : x ⤳ y), x ∈ U
Tactic: obtain ⟨y, hyt, hxy⟩ := hst x hx
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) t
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
have refine_2 : ∀ (x : α) (hxt : x ∈ t) (hxU : x ∈ U),
  LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
Tactic: obtain ⟨x, hxt, hxU⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
x : α
hxt : x ∈ t
hxU : x ∈ U
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
have refine_2 : ∀ (y : α) (hyU : y ∈ U) (hys : y ∈ s),
  LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
Tactic: obtain ⟨y, hyU, hys⟩ := mem_closure_iff.mp (hts hxt) U hU hxU
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst] s
have simp_rw : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
Tactic: simp_rw [specializes_iff, specializes_iff_eq, existsAndEq, and_true, ← subset_def]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
simp_rw : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst] s
have simp_rw₁ : (∀ x ∈ s, ∃ y ∈ t, x = y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
Tactic: simp_rw [specializes_iff, specializes_iff_eq, existsAndEq, and_true, ← subset_def]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
simp_rw : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₁ : (∀ x ∈ s, ∃ y ∈ t, x = y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst] s
have simp_rw₂ : (∀ x ∈ s, x ∈ t ∧ True) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
Tactic: simp_rw [specializes_iff, specializes_iff_eq, existsAndEq, and_true, ← subset_def]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
simp_rw : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₁ : (∀ x ∈ s, ∃ y ∈ t, x = y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₂ : (∀ x ∈ s, x ∈ t ∧ True) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst] s
have simp_rw₃ : (∀ x ∈ s, x ∈ t) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
Tactic: simp_rw [specializes_iff, specializes_iff_eq, existsAndEq, and_true, ← subset_def]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ F}
have simp_rw : IsOpen.{u_1} (X := Compacts α) {a : Compacts α | ((↑a : Set α) ∩ Fᶜ).Nonempty}
Tactic: simp_rw [← isOpen_compl_iff, Set.compl_setOf, ← Set.inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := Compacts α) {K : Compacts α | ((↑K : Set α) ∩ F).Nonempty}
have simp_rw : IsClosed.{u_1} (X := Compacts α) {a : Compacts α | (↑a : Set α) ⊆ Fᶜ}ᶜ
Tactic: simp_rw +singlePass [← compl_compl F, Set.inter_compl_nonempty_iff, ← Set.compl_setOf]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClopen (X := Compacts α) {⊥}
have h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})
Tactic: convert! vietoris.isClopen_singleton_empty.preimage continuous_coe
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})
have h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {(↑⊥ : Set α)})
Tactic: rw [← coe_bot, ← image_singleton (f := SetLike.coe), SetLike.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {(↑⊥ : Set α)})
⊢ Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})
have h₁ : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' image (α := Compacts α) SetLike.coe {⊥})
Tactic: rw [← coe_bot, ← image_singleton (f := SetLike.coe), SetLike.coe_injective.preimage_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {(↑⊥ : Set α)})
h₁ : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' image (α := Compacts α) SetLike.coe {⊥})
⊢ Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})
have h₂ : Eq (α := Set (Compacts α)) {⊥} {⊥}
Tactic: rw [← coe_bot, ← image_singleton (f := SetLike.coe), SetLike.coe_injective.preimage_image]
-- 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} (α := Compacts α)
    ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u ⊆ B})
have refine_1 : ∀ (u : Set (Compacts α)),
  Membership.mem (γ := Set (Set (Compacts α)))
      ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
        {u : Set (Set α) | u.Finite ∧ u ⊆ B})
      u →
    IsOpen u
Tactic: refine hB.vietoris.isInducing isEmbedding_coe.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 (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        u →
      IsOpen u
⊢ IsTopologicalBasis.{u_1} (α := Compacts α)
    ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u ⊆ B})
have refine_2 : ∀ (u : Set (Compacts α)),
  Membership.mem (γ := Set (Set (Compacts α)))
      (preimage SetLike.coe ''
        (fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
          {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
      u →
    ∀ x ∈ u,
      ∃ (v : Set (Compacts α)),
        Membership.mem (γ := Set (Set (Compacts α)))
            ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ u ⊆ B})
            v ∧
          x ∈ v ∧ v ⊆ u
Tactic: refine hB.vietoris.isInducing isEmbedding_coe.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 (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        u →
      IsOpen u
have refine_1 : ∀ ⦃x : Set (Set α)⦄,
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} x →
    IsOpen.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
Tactic: simp_rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ ∀ (u : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        (preimage SetLike.coe ''
          (fun (p : Set α × Set (Set α)) ↦ {s : Set α | s ⊆ p.1 ∧ ∀ U ∈ p.2, (s ∩ U).Nonempty}) ''
            {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ u
have refine_2 : ∀ ⦃x : Set α × Set (Set α)⦄,
  Membership.mem (γ := Set (Set α × Set (Set α)))
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} x →
    ∀ (x_1 : Compacts α),
      Membership.mem (γ := Set (Compacts α)) (SetLike.coe ⁻¹' {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}) x_1 →
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            x_1 ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ x.1 ∧ ∀ U ∈ x.2, (s ∩ U).Nonempty}
Tactic: simp_rw [forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} u →
    IsOpen.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_1 : ∀ (hu : u.Finite) (huB : u ⊆ B),
  IsOpen.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
Tactic: ⟨hu, huB⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
⊢ IsOpen.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
have refine_1 : IsOpen.{u_1} (X := Compacts α)
  ({a : Compacts α | (↑a : Set α) ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : Compacts α | ((↑x : Set α) ∩ i).Nonempty})
Tactic: simp_rw [setOf_and, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
⊢ Membership.mem (γ := Set (Set α × Set (Set α)))
      {p : Set α × Set (Set α) | IsOpen[inst] p.1 ∧ p.2.Finite ∧ p.2 ⊆ B ∧ ∀ U ∈ p.2, U ⊆ p.1} (V, u) →
    ∀ (x : Compacts α),
      Membership.mem (γ := Set (Compacts α))
          (SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}) x →
        ∃ (v : Set (Compacts α)),
          Membership.mem (γ := Set (Set (Compacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
have refine_2 : ∀ (hV : IsOpen[inst] (V, u).1) (hu : (V, u).2.Finite) (huB : (V, u).2 ⊆ B) (huV : ∀ U ∈ (V, u).2, U ⊆ (V, u).1)
  (x : Compacts α),
  Membership.mem (γ := Set (Compacts α)) (SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty})
      x →
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        x ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
Tactic: ⟨hV, hu, huB, huV⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
huV : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
K : Compacts α
⊢ Membership.mem (γ := Set (Compacts α)) (SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty})
      K →
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
have refine_2 : ∀ (hKV : (↑K : Set α) ⊆ (V, u).1) (hKu : ∀ U ∈ (V, u).2, ((↑K : Set α) ∩ U).Nonempty),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
Tactic: ⟨hKV, hKu⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] (V, u).1
hu : (V, u).2.Finite
huB : (V, u).2 ⊆ B
huV : ∀ U ∈ (V, u).2, U ⊆ (V, u).1
K : Compacts α
hKV : (↑K : Set α) ⊆ (V, u).1
hKu : ∀ U ∈ (V, u).2, ((↑K : Set α) ∩ U).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ (V, u).1 ∧ ∀ U ∈ (V, u).2, (s ∩ U).Nonempty}
have refine_2 : ∃ (v : Set (Compacts α)),
  Membership.mem (γ := Set (Set (Compacts α)))
      ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
        {u : Set (Set α) | u.Finite ∧ u ⊆ B})
      v ∧
    K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: dsimp only at *
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKV : (↑K : Set α) ⊆ V
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀ (w : Set (Set α)) (hwB : w ⊆ B) (hwV : V = ⋃₀ w),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: obtain ⟨w, hwB, hwV⟩ := hB.open_eq_sUnion hV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKV : (↑K : Set α) ⊆ V
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hwB : w ⊆ B
hwV : V = ⋃₀ w
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have hKV₁ : (↑K : Set α) ⊆ ⋃₀ w
Tactic: rw [hwV] at hKV
Cleared hypotheses: hKV, hwB, hwV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : V = ⋃₀ w
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have hwV₁ : ⋃₀ w ⊆ V
Tactic: replace hwV := hwV.symm.subset
Cleared hypotheses: hwV
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have refine_2 : ∀
  (this :
    ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
      (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
      ∃ (v : Set (Compacts α)),
        Membership.mem (γ := Set (Set (Compacts α)))
            ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ u ⊆ B})
            v ∧
          K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
  (hwK : ¬∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty),
  ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
Tactic: wlog hwK : ∀ W ∈ w, ((K : Set α) ∩ W).Nonempty generalizing w