awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : IsEmpty α
⊢ IsEmpty.{u_1 + 1} (NonemptyCompacts α)

Tactic:
⟨fun K => not_isEmpty_iff.mpr K.nonempty.to_type ‹_›⟩

Premises used: Iff.mpr, Set.Nonempty.to_type, IsEmpty.mk, TopologicalSpace.NonemptyCompacts.nonempty, not_isEmpty_iff
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsEmpty.{u_1 + 1} (NonemptyCompacts α) ↔ IsEmpty α

Tactic:
⟨fun _ => Function.isEmpty ({·} : α → NonemptyCompacts α), fun _ => inferInstance⟩

Premises used: Function.isEmpty, inferInstance, Iff.intro, Singleton.singleton
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Nonempty α
⊢ Nonempty.{u_1 + 1} (NonemptyCompacts α)

Tactic:
.map ({·}) ‹_›

Premises used: Nonempty.map, Singleton.singleton
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw : ¬IsEmpty.{u_1 + 1} (NonemptyCompacts α) ↔ ¬IsEmpty α
⊢ Nonempty.{u_1 + 1} (NonemptyCompacts α) ↔ Nonempty α

Tactic:
simp_rw [← not_isEmpty_iff, isEmpty_iff]

Premises used: TopologicalSpace.NonemptyCompacts.isEmpty_iff, not_isEmpty_iff
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
⊢ Subsingleton.{u_1 + 1} (NonemptyCompacts α)

Tactic:
⟨fun K L => NonemptyCompacts.ext ?_⟩

Premises used: TopologicalSpace.NonemptyCompacts.ext, Subsingleton.intro
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
refine : ∀ (K L : NonemptyCompacts α), (↑K : Set α) = (↑L : Set α)
⊢ Subsingleton.{u_1 + 1} (NonemptyCompacts α)

Tactic:
refine ⟨fun K L => NonemptyCompacts.ext ?_⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Subsingleton α
K L : NonemptyCompacts α
rw : univ = (↑L : Set α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ (↑K : Set α) = (↑L : Set α)

Tactic:
rw [Subsingleton.eq_univ_of_nonempty K.nonempty, Subsingleton.eq_univ_of_nonempty L.nonempty]

Premises used: TopologicalSpace.NonemptyCompacts.nonempty, Subsingleton.eq_univ_of_nonempty
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Subsingleton.{u_1 + 1} (NonemptyCompacts α) ↔ Subsingleton α

Tactic:
⟨fun _ => singleton_injective.subsingleton, fun _ => inferInstance⟩

Premises used: Function.Injective.subsingleton, inferInstance, Iff.intro, TopologicalSpace.NonemptyCompacts.singleton_injective
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Nontrivial α
⊢ Nontrivial.{u_1} (NonemptyCompacts α)

Tactic:
singleton_injective.nontrivial

Premises used: Function.Injective.nontrivial, TopologicalSpace.NonemptyCompacts.singleton_injective
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw : ¬Subsingleton.{u_1 + 1} (NonemptyCompacts α) ↔ ¬Subsingleton α
⊢ Nontrivial.{u_1} (NonemptyCompacts α) ↔ Nontrivial α

Tactic:
simp_rw [← not_subsingleton_iff_nontrivial, subsingleton_iff]

Premises used: TopologicalSpace.NonemptyCompacts.subsingleton_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
s : NonemptyCompacts α
⊢ (↑(NonemptyCompacts.map f hf s) : Set β) = f '' (↑s : Set α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : NonemptyCompacts α
h : ∀ (x : α), x ∈ (↑(NonemptyCompacts.map id ⋯ K) : Set α) ↔ x ∈ (↑K : Set α)
⊢ NonemptyCompacts.map id ⋯ K = K

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : NonemptyCompacts α
x : α
⊢ x ∈ (↑(NonemptyCompacts.map id ⋯ K) : Set α) ↔ x ∈ (↑K : Set α)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
h :
  ∀ (x : γ),
    x ∈ (↑(NonemptyCompacts.map (f ∘ g) ⋯ K) : Set γ) ↔
      x ∈ (↑(NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)) : Set γ)
⊢ NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
x : γ
⊢ x ∈ (↑(NonemptyCompacts.map (f ∘ g) ⋯ K) : Set γ) ↔
    x ∈ (↑(NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)) : Set γ)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
h : ∀ (x_1 : β), x_1 ∈ (↑(NonemptyCompacts.map f hf {x}) : Set β) ↔ x_1 ∈ (↑{f x} : Set β)
⊢ NonemptyCompacts.map f hf {x} = {f x}

Tactic:
ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
x_1 : β
⊢ x_1 ∈ (↑(NonemptyCompacts.map f hf {x}) : Set β) ↔ x_1 ∈ (↑{f x} : Set β)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
hf' : Function.Injective f
⊢ Function.Injective (NonemptyCompacts.map f hf)

Tactic:
.of_comp (f := SetLike.coe) <| hf'.image_injective.comp SetLike.coe_injective

Premises used: SetLike.coe_injective, Function.Injective.comp, Function.Injective.image_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (NonemptyCompacts.map f hf)
x x_1 : α
h_1 : Eq (α := NonemptyCompacts β) (((fun (x : β) ↦ {x}) ∘ f) x) (((fun (x : β) ↦ {x}) ∘ f) x_1)
⊢ NonemptyCompacts.map f hf ((fun (x : α) ↦ ({x} : NonemptyCompacts α)) x) =
    NonemptyCompacts.map f hf ((fun (x : α) ↦ ({x} : NonemptyCompacts α)) x_1)

Tactic:
simp_all
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
⊢ range (NonemptyCompacts.map f ⋯) = {K : NonemptyCompacts β | (↑K : Set β) ⊆ range f}

Tactic:
subset_antisymm
    (range_subset_iff.mpr fun _ => image_subset_range _ _)
    (fun L hL => ⟨
      { carrier := f ⁻¹' L
        isCompact' := hf.isCompact_preimage' L.isCompact hL
        nonempty' := L.nonempty.preimage' hL },
      NonemptyCompacts.ext (image_preimage_eq_of_subset hL)⟩)

Premises used: Iff.mpr, TopologicalSpace.NonemptyCompacts.toCompacts, TopologicalSpace.NonemptyCompacts.ext, TopologicalSpace.NonemptyCompacts.mk, Set.Nonempty.preimage', Set.image_subset_range, subset_antisymm, TopologicalSpace.Compacts.carrier, TopologicalSpace.Compacts.mk, TopologicalSpace.NonemptyCompacts.nonempty, SetLike.coe, Set.preimage, Set.image_preimage_eq_of_subset, Topology.IsInducing.isCompact_preimage', Exists.intro, TopologicalSpace.NonemptyCompacts.isCompact, Set.range_subset_iff
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : NonemptyCompacts α
⊢ CompactSpace.{u_1} ↥s

Tactic:
isCompact_iff_compactSpace.1 s.isCompact

Premises used: isCompact_iff_compactSpace, Iff.mp, TopologicalSpace.NonemptyCompacts.isCompact
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : NonemptyCompacts α
⊢ Nonempty.{u_1 + 1} ↥s

Tactic:
s.nonempty.to_subtype

Premises used: Set.Nonempty.to_subtype, TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
K : NonemptyCompacts α
L : NonemptyCompacts β
⊢ (↑(K ×ˢ L) : Set (α × β)) = (↑K : Set α) ×ˢ (↑L : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
K : NonemptyCompacts α
L : NonemptyCompacts β
⊢ (K ×ˢ L).toCompacts = K.toCompacts ×ˢ L.toCompacts

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T2Space α
inst_3 : T2Space β
K : NonemptyCompacts α
L : NonemptyCompacts β
⊢ (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds

Tactic:
rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
x : α
y : β
⊢ SProd.sprod (α := NonemptyCompacts α) (β := NonemptyCompacts β) {x} {y} = {(x, y)}

Tactic:
NonemptyCompacts.ext Set.singleton_prod_singleton

Premises used: TopologicalSpace.NonemptyCompacts.ext, Set.singleton_prod_singleton
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : PositiveCompacts α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (s : PositiveCompacts α) ↦ s.carrier) s)
    ((fun (s : PositiveCompacts α) ↦ s.carrier) t)
obtain :
  ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
    (interior_nonempty' : (interior { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier).Nonempty)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : PositiveCompacts α) ↦ s.carrier)
          { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
        ((fun (s : PositiveCompacts α) ↦ s.carrier) t)),
    { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } = t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : PositiveCompacts α
carrier : Set α
isCompact' : IsCompact carrier
interior_nonempty' : (interior { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier).Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : PositiveCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
    ((fun (s : PositiveCompacts α) ↦ s.carrier) t)
obtain :
  ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
    (interior_nonempty'_1 :
      (interior { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier).Nonempty)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : PositiveCompacts α) ↦ s.carrier)
          { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
        ((fun (s : PositiveCompacts α) ↦ s.carrier)
          { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 })),
    { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } =
      { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 }
⊢ { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
carrier : Set α
isCompact' : IsCompact carrier
interior_nonempty' : (interior { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier).Nonempty
carrier_1 : Set α
isCompact'_1 : IsCompact carrier_1
interior_nonempty'_1 : (interior { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier).Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : PositiveCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' })
    ((fun (s : PositiveCompacts α) ↦ s.carrier)
      { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 })
⊢ { carrier := carrier, isCompact' := isCompact', interior_nonempty' := interior_nonempty' : PositiveCompacts α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, interior_nonempty' := interior_nonempty'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : PositiveCompacts α
⊢ IsCompact (↑s : Set α)

Tactic:
s.isCompact'

Premises used: TopologicalSpace.Compacts.isCompact', TopologicalSpace.PositiveCompacts.toCompacts
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : PositiveCompacts α
⊢ (interior (↑s : Set α)).Nonempty

Tactic:
s.interior_nonempty'

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : PositiveCompacts α
⊢ (↑s : Set α).Nonempty

Tactic:
s.interior_nonempty.mono interior_subset

Premises used: interior_subset, TopologicalSpace.PositiveCompacts.interior_nonempty, Set.Nonempty.mono
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : PositiveCompacts α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Compacts α
h : (interior s.carrier).Nonempty
⊢ (↑{ toCompacts := s, interior_nonempty' := h : PositiveCompacts α } : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : PositiveCompacts α
⊢ s.carrier = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : PositiveCompacts α
⊢ (↑s.toCompacts : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : PositiveCompacts α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
hf' : IsOpenMap f
s : PositiveCompacts α
⊢ (↑(PositiveCompacts.map f hf hf' s) : Set β) = f '' (↑s : Set α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : PositiveCompacts α
⊢ PositiveCompacts.map id ⋯ ⋯ K = K

Tactic:
PositiveCompacts.ext <| Set.image_id _

Premises used: Set.image_id, TopologicalSpace.PositiveCompacts.ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
hf' : IsOpenMap f
hg' : IsOpenMap g
K : PositiveCompacts α
⊢ PositiveCompacts.map (f ∘ g) ⋯ ⋯ K = PositiveCompacts.map f hf hf' (PositiveCompacts.map g hg hg' K)

Tactic:
PositiveCompacts.ext <| Set.image_comp _ _ _

Premises used: Set.image_comp, TopologicalSpace.PositiveCompacts.ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LocallyCompactSpace α
U : Set α
ho : IsOpen U
hn : U.Nonempty
⊢ ∃ (K : PositiveCompacts α), (↑K : Set α) ⊆ U

Tactic:
let ⟨x, hx⟩ := hn
  let ⟨K, hKc, hxK, hKU⟩ := exists_compact_subset ho hx
  ⟨⟨⟨K, hKc⟩, ⟨x, hxK⟩⟩, hKU⟩

Premises used: _private.0.exists_positiveCompacts_subset.match_1, Exists, HasSubset.Subset, TopologicalSpace.Compacts.mk, exists_compact_subset, SetLike.coe, Exists.intro, _private.0.exists_positiveCompacts_subset.match_2, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : R1Space α
inst_2 : LocallyCompactSpace α
U : Set α
ho : IsOpen U
hn : U.Nonempty
⊢ ∃ (K : PositiveCompacts α), closure (↑K : Set α) ⊆ U

Tactic:
let ⟨K, hKU⟩ := exists_positiveCompacts_subset ho hn
  ⟨K, K.isCompact.closure_subset_of_isOpen ho hKU⟩

Premises used: Exists, _private.0.IsOpen.exists_positiveCompacts_closure_subset.match_1, HasSubset.Subset, exists_positiveCompacts_subset, SetLike.coe, closure, IsCompact.closure_subset_of_isOpen, Exists.intro, TopologicalSpace.PositiveCompacts.isCompact
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
inhabit : ∀ (inhabited_h : Inhabited α), Nonempty.{u_1 + 1} (PositiveCompacts α)
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)

Tactic:
inhabit α
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
inhabited_h : Inhabited α
rcases :
  ∀ (K : Set α) (hKc : IsCompact K) (hK : Membership.mem (γ := Filter α) (nhds default) K),
    Nonempty.{u_1 + 1} (PositiveCompacts α)
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)

Tactic:
rcases exists_compact_mem_nhds (default : α) with ⟨K, hKc, hK⟩

Premises used: Inhabited.default, WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
inhabited_h : Inhabited α
K : Set α
hKc : IsCompact K
hK : Membership.mem (γ := Filter α) (nhds default) K
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)

Tactic:
⟨⟨K, hKc⟩, _, mem_interior_iff_mem_nhds.2 hK⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, TopologicalSpace.Compacts.mk, Nonempty.intro, Exists.intro, TopologicalSpace.PositiveCompacts.mk
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : WeaklyLocallyCompactSpace α
inst_4 : Nonempty α
inhabited_h : Inhabited α
K : Set α
hKc : IsCompact K
hK : Membership.mem (γ := Filter α) (nhds default) K
⊢ Nonempty.{u_1 + 1} (PositiveCompacts α)

Tactic:
exact ⟨⟨K, hKc⟩, _, mem_interior_iff_mem_nhds.2 hK⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
simp : (interior (↑K.toCompacts : Set α) ×ˢ interior (↑L.toCompacts : Set β)).Nonempty
⊢ (interior (K.toCompacts ×ˢ L.toCompacts).carrier).Nonempty

Tactic:
simp only [Compacts.carrier_eq_coe, Compacts.coe_prod, interior_prod_eq]

Premises used: TopologicalSpace.Compacts.carrier_eq_coe, interior_prod_eq, TopologicalSpace.Compacts.coe_prod
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (interior (↑K.toCompacts : Set α) ×ˢ interior (↑L.toCompacts : Set β)).Nonempty

Tactic:
K.interior_nonempty.prod L.interior_nonempty

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty, Set.Nonempty.prod
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (interior (↑K.toCompacts : Set α) ×ˢ interior (↑L.toCompacts : Set β)).Nonempty

Tactic:
exact K.interior_nonempty.prod L.interior_nonempty

Premises used: TopologicalSpace.PositiveCompacts.interior_nonempty, Set.Nonempty.prod
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (↑(K ×ˢ L) : Set (α × β)) = (↑K : Set α) ×ˢ (↑L : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s t : CompactOpens α
h : Eq.{u_1 + 1} (α := Set α) ((fun (s : CompactOpens α) ↦ s.carrier) s) ((fun (s : CompactOpens α) ↦ s.carrier) t)
obtain :
  ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
    (isOpen' : IsOpen { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
        ((fun (s : CompactOpens α) ↦ s.carrier) t)),
    { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } = t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
t : CompactOpens α
carrier : Set α
isCompact' : IsCompact carrier
isOpen' : IsOpen { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
    ((fun (s : CompactOpens α) ↦ s.carrier) t)
obtain :
  ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
    (isOpen'_1 : IsOpen { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
        ((fun (s : CompactOpens α) ↦ s.carrier)
          { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 })),
    { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } =
      { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 }
⊢ { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
carrier : Set α
isCompact' : IsCompact carrier
isOpen' : IsOpen { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier
carrier_1 : Set α
isCompact'_1 : IsCompact carrier_1
isOpen'_1 : IsOpen { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' })
    ((fun (s : CompactOpens α) ↦ s.carrier) { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 })
⊢ { carrier := carrier, isCompact' := isCompact', isOpen' := isOpen' : CompactOpens α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, isOpen' := isOpen'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : CompactOpens α
⊢ IsCompact (↑s : Set α)

Tactic:
s.isCompact'

Premises used: TopologicalSpace.CompactOpens.toCompacts, TopologicalSpace.Compacts.isCompact'