awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
h₁ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h₂ : Eq (α := Set (Compacts α)) {K}
  ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩ {x : Compacts α | (↑K : Set α) ⊆ (↑x : Set α)})
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]
-- 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 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
h₁ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
h₂ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩ {x : Compacts α | (↑K : Set α) ⊆ (↑x : Set α)})
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h₃ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) ⊆ (↑K : Set α) ∧ (↑K : Set α) ⊆ (↑a : Set α)}
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]
-- 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 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
h₁ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
h₂ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩ {x : Compacts α | (↑K : Set α) ⊆ (↑x : Set α)})
h₃ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) ⊆ (↑K : Set α) ∧ (↑K : Set α) ⊆ (↑a : Set α)}
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h₄ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) = (↑K : Set α)}
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]
-- 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 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
h₁ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
h₂ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩ {x : Compacts α | (↑K : Set α) ⊆ (↑x : Set α)})
h₃ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) ⊆ (↑K : Set α) ∧ (↑K : Set α) ⊆ (↑a : Set α)}
h₄ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) = (↑K : Set α)}
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h₅ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | a = K}
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]
-- 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 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
⊢ (fun (x y : Compacts α) ↦
      ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
    K₁ K₂
have inr : ∀
  (this :
    ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
      (fun (x y : Compacts α) ↦
          ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
        K₁ K₂)
  (h' : ¬¬K₁ ≤ K₂),
  ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Tactic: wlog h' : ¬(K₁ ≤ K₂) generalizing K₁ K₂
-- 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 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
inr :
  ∀
    (this :
      ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
        (fun (x y : Compacts α) ↦
            ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
          K₁ K₂)
    (h' : ¬¬K₁ ≤ K₂),
    ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
have wlog : ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
  ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Tactic: wlog h' : ¬(K₁ ≤ K₂) generalizing K₁ K₂
Cleared hypotheses: K₁, K₂, h
-- 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 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ¬K₁ ≤ K₂
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
have h'₁ : ∃ x ∈ K₁, x ∉ K₂
Tactic: rw [SetLike.not_le_iff_exists] at h'
Cleared hypotheses: 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 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ∃ x ∈ K₁, x ∉ K₂
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
have obtain : ∀ (x : α) (hx₁ : x ∈ K₁) (hx₂ : x ∉ K₂),
  ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Tactic: obtain ⟨x, hx₁, hx₂⟩ := h'
Cleared hypotheses: 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 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
have obtain : ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hU' : (↑K₂ : Set α) ⊆ U) (hV' : x ∈ V)
  (hUV : Disjoint U V),
  ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
Tactic: obtain ⟨U, V, hU, hV, hU', hV', hUV⟩ := K₂.isCompact.separation_of_notMem hx₂
-- 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 : RegularSpace α
⊢ RegularSpace.{u_1} (Compacts α)
have simp_rw : ∀ (t : Set (Compacts α)),
  Membership.mem (γ := Set (Set (Compacts α)))
      ((fun (a : Set α) ↦ {a_1 : Compacts α | (↑a_1 : Set α) ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
      t →
    ∀ a ∈ t, ∃ s ∈ 𝓝ˢ tᶜ, ∃ t ∈ 𝓝 a, Disjoint s t
Tactic: simp_rw [regularSpace_generateFrom induced_generateFrom_eq, image_union, image_image, powerset,
    preimage_setOf_eq, Filter.disjoint_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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inl : ∀ (V W : Set α) (hV : IsOpen[inst] V) (hW : IsOpen[inst] W) (hKV : (↑K : Set α) ⊆ V) (hUW : Uᶜ ⊆ W)
  (hVW : Disjoint V W),
  ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
Tactic: obtain ⟨V, W, hV, hW, hKV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl
        (disjoint_compl_right_iff_subset.mpr hK)
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inl : Membership.mem (γ := Filter (Compacts α))
  (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ)
  {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
Tactic: refine ⟨{K | (↑K ∩ W).Nonempty}, ?_, {K | ↑K ⊆ V},
      (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind [Set.Nonempty]⟩
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
have inl : Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ Uᶜ).Nonempty}
  {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
Tactic: simp_rw [(isOpen_inter_nonempty_of_isOpen hW).mem_nhdsSet, compl_setOf,
      ← inter_compl_nonempty_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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ Uᶜ).Nonempty}
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
have inl : Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ W).Nonempty}
  {a : Compacts α | ((↑a : Set α) ∩ W).Nonempty}
Tactic: grw [hUW]
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U) K
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inr : ∀ (x : α) (hx₁ : x ∈ (↑K : Set α)) (hx₂ : x ∈ U),
  ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
Tactic: obtain ⟨x, hx₁, hx₂⟩ := hK
Cleared hypotheses: hK
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inr : ∀ (V W : Set α) (hV : IsOpen[inst] V) (hW : IsOpen[inst] W) (hxV : {x} ⊆ V) (hUW : Uᶜ ⊆ W) (hVW : Disjoint V W),
  ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
Tactic: obtain ⟨V, W, hV, hW, hxV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed (isCompact_singleton (x := x)) hU.isClosed_compl
        (by simpa)
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inr : Membership.mem (γ := Filter (Compacts α))
  (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ)
  {K : Compacts α | (↑K : Set α) ⊆ W}
Tactic: refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inr :
  Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | (↑K : Set α) ⊆ W}
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t
have inr₁ : {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} ∈ 𝓝 K
Tactic: refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | (↑K : Set α) ⊆ W}
have inr : Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | (↑a : Set α) ⊆ Uᶜ} {K : Compacts α | (↑K : Set α) ⊆ W}
Tactic: simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_setOf, not_nonempty_iff_eq_empty,
        ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right]
-- 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 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} ∈ 𝓝 K
have inr : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} K
Tactic: rw [(isOpen_inter_nonempty_of_isOpen hV).mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact.{u_1} (X := Compacts α) {L : Compacts α | (↑L : Set α) ⊆ K}
have rw : IsCompact (image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K})
Tactic: rw [isEmbedding_coe.isCompact_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact (image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K})
have refine : ∀ (s : Set α) (hs : s ∈ 𝒫 K), ∃ y ∈ image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K}, s ⤳ y
Tactic: refine .of_subset_of_specializes hK.powerset_vietoris (by grind) (fun s hs => ?_)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
⊢ IsCompact.{u_1} (X := α) (⋃ K ∈ S, (↑K : Set α))
have rw : ∀ {ι : Type u_1} (U : ι → Set α),
  (∀ (i : ι), IsOpen[inst] (U i)) →
    Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ (i : ι), U i) →
      ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
Tactic: rw [isCompact_iff_finite_subcover]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Compacts α)
hS : IsCompact S
ι : Type u_1
U : ι → Set α
hU : ∀ (i : ι), IsOpen[inst] (U i)
h : Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ (i : ι), U i)
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
have h₁ : ∀ (i : Compacts α) (j : i ∈ S), (↑i : Set α) ⊆ ⋃ (i : ι), U i
Tactic: rw [iUnion₂_subset_iff] at h
Cleared hypotheses: h
-- 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
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
have obtain : ∀ (s : Finset (Finset ι)) (hs : S ⊆ ⋃ i ∈ s, {K : Compacts α | (↑K : Set α) ⊆ ⋃ i_1 ∈ i, U i_1}),
  ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
Tactic: obtain ⟨s, hs⟩ := hS.elim_finite_subcover
    (fun s : Finset ι => {K | (K : Set α) ⊆ ⋃ i ∈ s, U i})
    (fun s => isOpen_subsets_of_isOpen <| isOpen_biUnion fun _ _ => hU _)
    (fun K hK => mem_iUnion.mpr <| K.isCompact.elim_finite_subcover U hU <| h K hK)
-- 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}
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
have 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)
Tactic: refine ⟨s.biUnion id, (biUnion_subset_biUnion_left hs).trans ?_⟩
-- 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}
⊢ 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)
have simp_rw : ∀ (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: simp_rw [biUnion_iUnion, iUnion_subset_iff, Finset.set_biUnion_biUnion]
-- 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}
⊢ ∃ (t : Finset ι), Subset.{u_1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ i ∈ t, U i)
have 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)
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