awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
s t : Compacts α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

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

Tactic:
SetLike.coe_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SetLike.coe_injective, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Compacts α
⊢ (↑s : Set α).Nonempty ↔ s ≠ ⊥

Tactic:
nonempty_iff_ne_empty.trans coe_eq_empty.not

Premises used: Iff.not, TopologicalSpace.Compacts.coe_eq_empty, Set.nonempty_iff_ne_empty, Iff.trans
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)

Tactic:
Finset.cons_induction_on s rfl fun a s _ h => ?_

Premises used: Finset.cons_induction_on
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
refine :
  ∀ (a : ι) (s : Finset ι) (x : a ∉ s) (h : (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)),
    (↑((Finset.cons a s x).sup f) : Set α) = (Finset.cons a s x).sup fun (i : ι) ↦ (↑(f i) : Set α)
⊢ (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)

Tactic:
refine Finset.cons_induction_on s rfl fun a s _ h => ?_
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s_1 : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
h_1 : a ∉ s
h : (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)
simp_rw : (↑(f a) : Set α) ∪ (↑(s.sup f) : Set α) = (↑(f a) : Set α) ∪ s.sup fun (i : ι) ↦ (↑(f i) : Set α)
⊢ (↑((Finset.cons a s h_1).sup f) : Set α) = (Finset.cons a s h_1).sup fun (i : ι) ↦ (↑(f i) : Set α)

Tactic:
simp_rw [Finset.sup_cons, coe_sup, sup_eq_union]

Premises used: Set.sup_eq_union, TopologicalSpace.Compacts.coe_sup, Finset.sup_cons
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_4
s_1 : Finset ι
f : ι → Compacts α
a : ι
s : Finset ι
h_1 : a ∉ s
h : (↑(s.sup f) : Set α) = s.sup fun (i : ι) ↦ (↑(f i) : Set α)
⊢ (↑(f a) : Set α) ∪ (↑(s.sup f) : Set α) = (↑(f a) : Set α) ∪ s.sup fun (i : ι) ↦ (↑(f i) : Set α)

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
⊢ Membership.mem (γ := Compacts α) {y} x ↔ x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
x : α
⊢ Eq (α := Closeds α) (toCloseds {x}) {x}

Tactic:
rfl

Premises used: TopologicalSpace.Compacts.toCloseds, setOf, Set.singleton, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Function.Injective (β := Compacts α) fun (x : α) ↦ {x}

Tactic:
.of_comp (f := SetLike.coe) Set.singleton_injective

Premises used: Set.singleton_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
⊢ Eq (α := Compacts α) {x} {y} ↔ x = y

Tactic:
singleton_injective.eq_iff

Premises used: TopologicalSpace.Compacts.singleton_injective, Function.Injective.eq_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 : Nonempty α
exists_pair_ne : ∃ (x : Compacts α) (y : Compacts α), x ≠ y
⊢ Nontrivial.{u_1} (Compacts α)

Tactic:
constructor
-- 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 α
exists_pair_ne : ∀ (x : α), ∃ (x : Compacts α) (y : Compacts α), x ≠ y
⊢ ∃ (x : Compacts α) (y : Compacts α), x ≠ y

Tactic:
obtain ⟨x⟩ := ‹Nonempty α›

Premises used: Nonempty
-- 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 α
x : α
⊢ ∃ (x : Compacts α) (y : Compacts α), x ≠ y

Tactic:
⟨⊥, {x}, ne_of_apply_ne SetLike.coe (Set.empty_ne_singleton x)⟩

Premises used: Bot.bot, ne_of_apply_ne, Set.empty_ne_singleton, SetLike.coe, Exists.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 α
x : α
⊢ ∃ (x : Compacts α) (y : Compacts α), x ≠ y

Tactic:
exact ⟨⊥, {x}, ne_of_apply_ne SetLike.coe (Set.empty_ne_singleton x)⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Subsingleton.{u_1 + 1} (Compacts α) ↔ IsEmpty α

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

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
refine : ∀ (h : Subsingleton.{u_1 + 1} (Compacts α)), IsEmpty α
⊢ Subsingleton.{u_1 + 1} (Compacts α) ↔ IsEmpty α

Tactic:
refine ⟨fun h => ?_, fun _ => inferInstance⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Subsingleton.{u_1 + 1} (Compacts α)
contrapose! : ∀ (h : Nonempty α), Nontrivial.{u_1} (Compacts α)
⊢ IsEmpty α

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Nonempty α
⊢ Nontrivial.{u_1} (Compacts α)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : ¬Subsingleton.{u_1 + 1} (Compacts α) ↔ Nonempty α
rw₁ : ¬IsEmpty α ↔ Nonempty α
rw₂ rw₃ : Nonempty α ↔ Nonempty α
⊢ Nontrivial.{u_1} (Compacts α) ↔ Nonempty α

Tactic:
rw [← not_subsingleton_iff_nontrivial, subsingleton_iff, not_isEmpty_iff]

Premises used: not_isEmpty_iff, not_subsingleton_iff_nontrivial, TopologicalSpace.Compacts.subsingleton_iff
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
s : Compacts α
⊢ (↑(Compacts.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 : Compacts α
⊢ Compacts.map id ⋯ K = K

Tactic:
Compacts.ext <| Set.image_id _

Premises used: TopologicalSpace.Compacts.ext, Set.image_id
-- 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 : Compacts α
⊢ Compacts.map (f ∘ g) ⋯ K = Compacts.map f hf (Compacts.map g hg K)

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

Premises used: TopologicalSpace.Compacts.ext, Set.image_comp
-- 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 (Compacts.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
x : α
⊢ Compacts.map f hf {x} = {f x}

Tactic:
Compacts.ext Set.image_singleton

Premises used: Set.image_singleton, TopologicalSpace.Compacts.ext
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective f

Tactic:
⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩

Premises used: TopologicalSpace.Compacts.map_injective, Iff.intro, 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
refine : ∀ (h : Function.Injective (Compacts.map f hf)), Function.Injective (β := Compacts β) ((fun (x : β) ↦ {x}) ∘ f)
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective f

Tactic:
refine ⟨fun h => .of_comp (f := ({·} : β → Compacts β)) ?_, map_injective hf⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
simp_rw : Function.Injective.{u_1 + 1, u_2 + 1} (β := Compacts β) fun (x : α) ↦ Compacts.map f hf {x}
⊢ Function.Injective (β := Compacts β) ((fun (x : β) ↦ {x}) ∘ f)

Tactic:
simp_rw [Function.comp_def, ← map_singleton hf]

Premises used: TopologicalSpace.Compacts.map_singleton, Function.comp_def
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β := Compacts β) fun (x : α) ↦ Compacts.map f hf {x}

Tactic:
h.comp singleton_injective

Premises used: TopologicalSpace.Compacts.singleton_injective, Function.Injective.comp, TopologicalSpace.Compacts.map
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (β := Compacts β) fun (x : α) ↦ Compacts.map f hf {x}

Tactic:
exact h.comp singleton_injective

Premises used: TopologicalSpace.Compacts.singleton_injective, Function.Injective.comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
⊢ range (Compacts.map f ⋯) = {K : Compacts β | (↑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 },
      Compacts.ext (image_preimage_eq_of_subset hL)⟩)

Premises used: Iff.mpr, TopologicalSpace.Compacts.ext, Set.image_subset_range, subset_antisymm, TopologicalSpace.Compacts.carrier, TopologicalSpace.Compacts.mk, SetLike.coe, Set.preimage, TopologicalSpace.Compacts.isCompact, Set.image_preimage_eq_of_subset, Topology.IsInducing.isCompact_preimage', Exists.intro, 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 γ
f : α ≃ₜ β
s : Compacts α
h : (↑(Compacts.map (⇑f.symm : (a : β) → α) ⋯ (Compacts.map (⇑f : (a : α) → β) ⋯ s)) : Set α) = (↑s : Set α)
⊢ Compacts.map (⇑f.symm : (a : β) → α) ⋯ (Compacts.map (⇑f : (a : α) → β) ⋯ s) = s

Tactic:
ext1
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts α
⊢ (↑(Compacts.map (⇑f.symm : (a : β) → α) ⋯ (Compacts.map (⇑f : (a : α) → β) ⋯ s)) : Set α) = (↑s : Set α)

Tactic:
simp only [coe_map, ← image_comp, f.symm_comp_self, image_id]

Premises used: TopologicalSpace.Compacts.coe_map, Set.image_comp, Set.image_id, Homeomorph.symm_comp_self
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
h : (↑(Compacts.map (⇑f : (a : α) → β) ⋯ (Compacts.map (⇑f.symm : (a : β) → α) ⋯ s)) : Set β) = (↑s : Set β)
⊢ Compacts.map (⇑f : (a : α) → β) ⋯ (Compacts.map (⇑f.symm : (a : β) → α) ⋯ s) = s

Tactic:
ext1
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
s : Compacts β
⊢ (↑(Compacts.map (⇑f : (a : α) → β) ⋯ (Compacts.map (⇑f.symm : (a : β) → α) ⋯ s)) : Set β) = (↑s : Set β)

Tactic:
simp only [coe_map, ← image_comp, f.self_comp_symm, image_id]

Premises used: TopologicalSpace.Compacts.coe_map, Homeomorph.self_comp_symm, Set.image_comp, Set.image_id
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := Compacts α ≃ Compacts α) (Compacts.equiv (Homeomorph.refl α)) (Equiv.refl (Compacts α))

Tactic:
Equiv.ext map_id

Premises used: Equiv.ext, TopologicalSpace.Compacts.map_id
-- 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 : β ≃ₜ γ
⊢ Compacts.equiv (f.trans g) = (Compacts.equiv f).trans (Compacts.equiv g)

Tactic:
Equiv.ext <| map_comp g f g.continuous f.continuous

Premises used: TopologicalSpace.Compacts.map_comp, Homeomorph.continuous, Equiv.ext, DFunLike.coe
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ Compacts.equiv f.symm = (Compacts.equiv f).symm

Tactic:
rfl

Premises used: TopologicalSpace.Compacts.equiv, TopologicalSpace.Compacts.map, Equiv.symm, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Compacts α
⊢ (↑((Compacts.equiv f : (a : Compacts α) → Compacts β) K : Compacts β) : Set β) =
    (⇑f.symm : (a : β) → α) ⁻¹' (↑K : Set α)

Tactic:
f.toEquiv.image_eq_preimage_symm K

Premises used: Set.Mem, Homeomorph.toEquiv, setOf, Equiv.image_eq_preimage_symm, SetLike.coe, Set.image
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
K : Compacts α
L : Compacts β
⊢ (↑(K ×ˢ L) : Set (α × β)) = (↑K : Set α) ×ˢ (↑L : Set β)

Tactic:
rfl

Premises used: setOf, Set.prod, 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 : Compacts α
L : Compacts β
⊢ (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 (α := Compacts α) (β := Compacts β) {x} {y} = {(x, y)}

Tactic:
Compacts.ext Set.singleton_prod_singleton

Premises used: TopologicalSpace.Compacts.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 : NonemptyCompacts α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (s : NonemptyCompacts α) ↦ s.carrier) s)
    ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)
obtain :
  ∀ (carrier : Set α) (isCompact' : IsCompact carrier)
    (nonempty' : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier.Nonempty)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : NonemptyCompacts α) ↦ s.carrier)
          { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
        ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)),
    { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } = 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 : NonemptyCompacts α
carrier : Set α
isCompact' : IsCompact carrier
nonempty' : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier.Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : NonemptyCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
    ((fun (s : NonemptyCompacts α) ↦ s.carrier) t)
obtain :
  ∀ (carrier_1 : Set α) (isCompact'_1 : IsCompact carrier_1)
    (nonempty'_1 : { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier.Nonempty)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : NonemptyCompacts α) ↦ s.carrier)
          { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
        ((fun (s : NonemptyCompacts α) ↦ s.carrier)
          { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 })),
    { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } =
      { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }
⊢ { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } = 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
nonempty' : { carrier := carrier, isCompact' := isCompact' : Compacts α }.carrier.Nonempty
carrier_1 : Set α
isCompact'_1 : IsCompact carrier_1
nonempty'_1 : { carrier := carrier_1, isCompact' := isCompact'_1 : Compacts α }.carrier.Nonempty
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : NonemptyCompacts α) ↦ s.carrier)
      { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' })
    ((fun (s : NonemptyCompacts α) ↦ s.carrier)
      { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 })
⊢ { carrier := carrier, isCompact' := isCompact', nonempty' := nonempty' : NonemptyCompacts α } =
    { carrier := carrier_1, isCompact' := isCompact'_1, nonempty' := nonempty'_1 }

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

Tactic:
s.isCompact'

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

Tactic:
s.nonempty'

Premises used: TopologicalSpace.NonemptyCompacts.nonempty'
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
s : NonemptyCompacts α
⊢ s.toCloseds = s.toCloseds

Tactic:
rfl

Premises used: TopologicalSpace.NonemptyCompacts.toCloseds, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
x : α
s : NonemptyCompacts α
⊢ x ∈ s.toCloseds ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := NonemptyCompacts α) toCloseds

Tactic:
.of_comp (f := SetLike.coe) SetLike.coe_injective

Premises used: SetLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : NonemptyCompacts α
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 : s.carrier.Nonempty
⊢ (↑{ toCompacts := s, nonempty' := h : NonemptyCompacts α } : Set α) = (↑s : Set α)

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s : NonemptyCompacts α
⊢ x ∈ s.toCompacts ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := NonemptyCompacts α) toCompacts

Tactic:
.of_comp (f := SetLike.coe) SetLike.coe_injective

Premises used: SetLike.coe_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
h :
  ∀ (K : Compacts α),
    Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ Membership.mem (γ := Set (Compacts α)) {⊥}ᶜ K
⊢ Eq (α := Set (Compacts α)) (range toCompacts) {⊥}ᶜ

Tactic:
ext K
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Compacts α
h : Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ (↑K : Set α).Nonempty
⊢ Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ Membership.mem (γ := Set (Compacts α)) {⊥}ᶜ K

Tactic:
rw [mem_compl_singleton_iff, ← Compacts.coe_nonempty]

Premises used: Set.mem_compl_singleton_iff, TopologicalSpace.Compacts.coe_nonempty
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Compacts α
⊢ Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ (↑K : Set α).Nonempty

Tactic:
⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩

Premises used: TopologicalSpace.NonemptyCompacts.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Compacts α
h : Membership.mem (γ := Set (Compacts α)) (range toCompacts) K → (↑K : Set α).Nonempty
⊢ Membership.mem (γ := Set (Compacts α)) (range toCompacts) K ↔ (↑K : Set α).Nonempty

Tactic:
refine ⟨?_, fun h => ⟨⟨K, h⟩, rfl⟩⟩
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : NonemptyCompacts α
⊢ (↑K.toCompacts : Set α).Nonempty

Tactic:
K.nonempty

Premises used: TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
K : NonemptyCompacts α
⊢ (↑K.toCompacts : Set α).Nonempty

Tactic:
exact K.nonempty

Premises used: TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : NonemptyCompacts α
⊢ (↑(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
inst : TopologicalSpace α
s t : NonemptyCompacts α
⊢ (s ⊔ t).toCompacts = s.toCompacts ⊔ t.toCompacts

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : Nonempty α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
⊢ Membership.mem (γ := NonemptyCompacts α) {y} x ↔ x = y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.singleton
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
x : α
⊢ Eq (α := Closeds α) (toCloseds {x}) {x}

Tactic:
rfl

Premises used: TopologicalSpace.NonemptyCompacts.toCloseds, setOf, Set.singleton, rfl
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Function.Injective (β := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
.of_comp (f := SetLike.coe) Set.singleton_injective

Premises used: Set.singleton_injective, Function.Injective.of_comp
-- Module: Mathlib.Topology.Sets.Compacts
Goal:
α : Type u_1
inst : TopologicalSpace α
x y : α
⊢ Eq (α := NonemptyCompacts α) {x} {y} ↔ x = y

Tactic:
singleton_injective.eq_iff

Premises used: Function.Injective.eq_iff, TopologicalSpace.NonemptyCompacts.singleton_injective