awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 := NonemptyCompacts α)
    ({a : NonemptyCompacts α | (↑a : Set α) ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : NonemptyCompacts α | ((↑x : Set α) ∩ i).Nonempty})

Tactic:
.inter
      (isOpen_subsets_of_isOpen <| isOpen_sUnion fun U hU => hB.isOpen <| huB hU)
      (hu.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hU)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen, TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen, IsOpen.inter, Set.Finite.isOpen_biInter, isOpen_sUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 := NonemptyCompacts α)
    ({a : NonemptyCompacts α | (↑a : Set α) ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : NonemptyCompacts α | ((↑x : Set α) ∩ i).Nonempty})

Tactic:
exact .inter
      (isOpen_subsets_of_isOpen <| isOpen_sUnion fun U hU => hB.isOpen <| huB hU)
      (hu.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen <| hB.isOpen <| huB hU)
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
refine_2 :
  ∀ (hu : u.Finite) (huB : u ⊆ B) (x : NonemptyCompacts α),
    Membership.mem (γ := Set (NonemptyCompacts α))
        (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) x →
      ∃ (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 ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} u →
    ∀ (x : NonemptyCompacts α),
      Membership.mem (γ := Set (NonemptyCompacts α))
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) x →
        ∃ (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 ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
⟨hu, huB⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
refine_2 :
  ∀ (hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u) (hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty),
    ∃ (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 ∧
        K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (NonemptyCompacts α))
      (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) K →
    ∃ (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 ∧
        K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
⟨hK₁, hK₂⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
refine_2 :
  ∀ (hu : Set.Finite.{u_1} (α := Set α) ∅) (huB : ∅ ⊆ B) (hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅)
    (hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty),
    ∃ (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 ∧
        K ∈ v ∧
          v ⊆
            toCompacts ⁻¹'
              {K : Compacts α |
                (↑K : Set α) ⊆ ⋃₀ ∅ ∧
                  ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K : Set α) ∩ U).Nonempty}
refine_2₁ :
  ∀ (hu' : u.Nonempty),
    ∃ (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 ∧
        K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
⊢ ∃ (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 ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
rcases eq_empty_or_nonempty u with rfl | hu'

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : Set.Finite.{u_1} (α := Set α) ∅
huB : ∅ ⊆ B
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅
hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty
⊢ ¬?_mvar.252760

Tactic:
K.nonempty.mono hK₁

Premises used: Set.Nonempty.mono, TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : Set.Finite.{u_1} (α := Set α) ∅
huB : ∅ ⊆ B
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅
hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty
refine_2 : ¬Set.Nonempty.{u_1} (α := α) (⋃₀ ∅)
⊢ ∃ (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 ∧
      K ∈ v ∧
        v ⊆
          toCompacts ⁻¹'
            {K : Compacts α |
              (↑K : Set α) ⊆ ⋃₀ ∅ ∧ ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K : Set α) ∩ U).Nonempty}

Tactic:
absurd K.nonempty.mono hK₁

Premises used: Set.Nonempty.mono, TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
K : NonemptyCompacts α
hu : Set.Finite.{u_1} (α := Set α) ∅
huB : ∅ ⊆ B
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ ∅
hK₂ : ∀ (U : Set α), Membership.mem (γ := Set (Set α)) ∅ U → ((↑K.toCompacts : Set α) ∩ U).Nonempty
⊢ ¬Set.Nonempty.{u_1} (α := α) (⋃₀ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
hu' : u.Nonempty
refine_2 :
  ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x ∧
      Membership.mem (γ := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        Subset.{u_1} (α := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})
⊢ ∃ (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 ∧
      K ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
rw [exists_mem_image]

Premises used: Set.exists_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
K : NonemptyCompacts α
hK₁ : (↑K.toCompacts : Set α) ⊆ ⋃₀ u
hK₂ : ∀ U ∈ u, ((↑K.toCompacts : Set α) ∩ U).Nonempty
hu' : u.Nonempty
refine_2 refine_2₁ :
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} u ∧
    Membership.mem (γ := Set (NonemptyCompacts α))
        {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty} K ∧
      Subset.{u_1} (α := Set (NonemptyCompacts α))
        {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}
        (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x ∧
      Membership.mem (γ := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        Subset.{u_1} (α := Set (NonemptyCompacts α))
          {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
          (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty})

Tactic:
exists u
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ 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 ∈ u, IsOpen[inst] U})

Tactic:
isTopologicalBasis_opens.nonemptyCompacts

Premises used: Set.Mem, setOf, TopologicalSpace.isTopologicalBasis_opens, Set.Subset, TopologicalSpace.IsTopologicalBasis.nonemptyCompacts, IsOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsEmbedding (Y := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
isEmbedding_coe.of_comp_iff.mp vietoris.isEmbedding_singleton

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_coe, TopologicalSpace.vietoris.isEmbedding_singleton, Iff.mp, Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[inst, _] fun (x : α) ↦ {x}

Tactic:
isEmbedding_singleton.continuous

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_singleton, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ IsClosedEmbedding (Y := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
isClosedEmbedding_toCompacts.of_comp_iff.mp Compacts.isClosedEmbedding_singleton

Premises used: Topology.IsClosedEmbedding.of_comp_iff, TopologicalSpace.Compacts.isClosedEmbedding_singleton, Iff.mp, TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
continuous_sup : Continuous (Y := NonemptyCompacts α) fun (p : NonemptyCompacts α × NonemptyCompacts α) ↦ p.1 ⊔ p.2
⊢ ContinuousSup.{u_1} (NonemptyCompacts α)

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
continuous_sup :
  Continuous (Y := Compacts α) fun (x : NonemptyCompacts α × NonemptyCompacts α) ↦ x.1.toCompacts ⊔ x.2.toCompacts
⊢ Continuous (Y := NonemptyCompacts α) fun (p : NonemptyCompacts α × NonemptyCompacts α) ↦ p.1 ⊔ p.2

Tactic:
simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_sup]

Premises used: Function.comp_def, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsEmbedding.continuous_iff, TopologicalSpace.NonemptyCompacts.toCompacts_sup
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ Continuous (Y := Compacts α) fun (x : NonemptyCompacts α × NonemptyCompacts α) ↦ x.1.toCompacts ⊔ x.2.toCompacts

Tactic:
fun_prop
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
simp_rw :
  Continuous (Y := Compacts (α × β)) fun (x : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
    x.1.toCompacts ×ˢ x.2.toCompacts
⊢ Continuous (Y := NonemptyCompacts (α × β)) fun (p : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
    p.1 ×ˢ p.2

Tactic:
simp_rw [isEmbedding_toCompacts.continuous_iff, Function.comp_def, toCompacts_prod]

Premises used: Function.comp_def, TopologicalSpace.NonemptyCompacts.toCompacts_prod, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous (Y := Compacts (α × β)) fun (x : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
    x.1.toCompacts ×ˢ x.2.toCompacts

Tactic:
fun_prop
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ Continuous (NonemptyCompacts.map f hf)

Tactic:
isEmbedding_toCompacts.continuous_iff.mpr <| hf.compacts_map.comp continuous_toCompacts

Premises used: Iff.mpr, Continuous.comp, TopologicalSpace.NonemptyCompacts.continuous_toCompacts, Continuous.compacts_map, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
⊢ IsInducing (NonemptyCompacts.map f ⋯)

Tactic:
.of_comp hf.continuous.nonemptyCompacts_map continuous_toCompacts <|
    hf.compacts_map.comp isEmbedding_toCompacts.isInducing

Premises used: Continuous.nonemptyCompacts_map, TopologicalSpace.NonemptyCompacts.continuous_toCompacts, Topology.IsInducing.comp, Topology.IsEmbedding.isInducing, Topology.IsInducing.compacts_map, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsInducing.continuous, Topology.IsInducing.of_comp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
⊢ IsOpenEmbedding (NonemptyCompacts.map f ⋯)

Tactic:
.of_comp _ isOpenEmbedding_toCompacts <| hf.compacts_map.comp isOpenEmbedding_toCompacts

Premises used: Topology.IsOpenEmbedding.compacts_map, TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts, Topology.IsOpenEmbedding.comp, Topology.IsOpenEmbedding.of_comp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
⊢ IsClosedEmbedding (NonemptyCompacts.map f ⋯)

Tactic:
isClosedEmbedding_toCompacts.of_comp_iff.mp <| hf.compacts_map.comp isClosedEmbedding_toCompacts

Premises used: Topology.IsClosedEmbedding.of_comp_iff, Topology.IsClosedEmbedding.comp, Topology.IsClosedEmbedding.compacts_map, Iff.mp, TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
⊢ DiscreteTopology.{u_1} (NonemptyCompacts α)

Tactic:
isEmbedding_toCompacts.discreteTopology

Premises used: Topology.IsEmbedding.discreteTopology, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology.{u_1} (NonemptyCompacts α) ↔ DiscreteTopology α

Tactic:
⟨fun _ => isEmbedding_singleton.discreteTopology, fun _ => inferInstance⟩

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_singleton, inferInstance, Topology.IsEmbedding.discreteTopology, Iff.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T1Space α
⊢ T0Space.{u_1} (NonemptyCompacts α)

Tactic:
isEmbedding_toCompacts.t0Space

Premises used: Topology.IsEmbedding.t0Space, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
⊢ T2Space.{u_1} (NonemptyCompacts α)

Tactic:
isEmbedding_toCompacts.t2Space

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ T2Space.{u_1} (NonemptyCompacts α) ↔ T2Space α

Tactic:
⟨fun _ => isEmbedding_singleton.t2Space, fun _ => inferInstance⟩

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_singleton, inferInstance, Iff.intro, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
⊢ RegularSpace.{u_1} (NonemptyCompacts α)

Tactic:
isEmbedding_toCompacts.regularSpace

Premises used: Topology.IsEmbedding.toIsInducing, Topology.IsInducing.regularSpace, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ RegularSpace.{u_1} (NonemptyCompacts α) ↔ RegularSpace α

Tactic:
⟨fun _ => isEmbedding_singleton.regularSpace, fun _ => inferInstance⟩

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_singleton, inferInstance, Iff.intro, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.regularSpace
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ T3Space.{u_1} (NonemptyCompacts α) ↔ T3Space α

Tactic:
⟨fun _ => isEmbedding_singleton.t3Space, fun _ => inferInstance⟩

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_singleton, inferInstance, Topology.IsEmbedding.t3Space, Iff.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : CompactSpace α
⊢ CompactSpace.{u_1} (NonemptyCompacts α)

Tactic:
isClosedEmbedding_toCompacts.compactSpace

Premises used: Topology.IsClosedEmbedding.compactSpace, TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact.{u_1} (X := NonemptyCompacts α) {L : NonemptyCompacts α | (↑L : Set α) ⊆ K}

Tactic:
isClosedEmbedding_toCompacts.isCompact_preimage (Compacts.isCompact_subsets_of_isCompact hK)

Premises used: Set.Mem, setOf, Set.preimage, Topology.IsClosedEmbedding.isCompact_preimage, TopologicalSpace.Compacts.isCompact_subsets_of_isCompact, TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
⊢ IsCompact.{u_1} (X := α) (⋃ K ∈ toCompacts '' S, (↑K : Set α))

Tactic:
Compacts.isCompact_biUnion_coe_of_isCompact (hs.image continuous_toCompacts)

Premises used: TopologicalSpace.NonemptyCompacts.continuous_toCompacts, TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact, IsCompact.image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
h : Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ K ∈ toCompacts '' S, (↑K : Set α))
⊢ IsCompact.{u_1} (X := α) (⋃ K ∈ S, (↑K : Set α))

Tactic:
convert! Compacts.isCompact_biUnion_coe_of_isCompact (hs.image continuous_toCompacts)

Premises used: TopologicalSpace.NonemptyCompacts.continuous_toCompacts, TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact, IsCompact.image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (NonemptyCompacts α)
hs : IsCompact S
h : Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ y ∈ S, (↑y.toCompacts : Set α))
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ K ∈ S, (↑K : Set α)) (⋃ K ∈ toCompacts '' S, (↑K : Set α))

Tactic:
simp_rw [biUnion_image, coe_toCompacts]

Premises used: TopologicalSpace.NonemptyCompacts.coe_toCompacts, Set.biUnion_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ CompactSpace.{u_1} (NonemptyCompacts α) ↔ CompactSpace α

Tactic:
⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩

Premises used: inferInstance, CompactSpace.mk, Iff.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine : ∀ (h : CompactSpace.{u_1} (NonemptyCompacts α)), IsCompact.{u_1} (X := α) univ
⊢ CompactSpace.{u_1} (NonemptyCompacts α) ↔ CompactSpace α

Tactic:
refine ⟨fun h => ⟨?_⟩, fun _ => inferInstance⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
⊢ IsCompact.{u_1} (X := α)
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α))

Tactic:
isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ

Premises used: TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompact, isCompact_univ
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
h₁ :
  Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α))
⊢ IsCompact.{u_1} (X := α) univ

Tactic:
convert! isCompact_biUnion_coe_of_isCompact (α := α) isCompact_univ

Premises used: TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompact, isCompact_univ
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : CompactSpace.{u_1} (NonemptyCompacts α)
h₁ :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α)) univ
⊢ Eq.{u_1 + 1} (α := Set α) univ
    (⋃ (K : NonemptyCompacts α), ⋃ (_ : Membership.mem (γ := Set (NonemptyCompacts α)) univ K), (↑K : Set α))

Tactic:
symm