awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
x : X.carrier
⊢ Eq (α :=
    (Functor.obj
        (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
          { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
          fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
        (completionFunctor.obj X)).carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) X.completionHom :
          (a : X.carrier) → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj (completionFunctor.obj X)).carrier)
        x :
      (Functor.obj
          (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
            fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
            carrier))
          (completionFunctor.obj X)).carrier)
    ((↑x : Completion X.carrier) : Completion X.carrier)

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f :
  X ⟶
    Functor.obj
      (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
        { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
        fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
      Y
x : (completionFunctor.obj X).α
⊢ Eq (α := Y.α)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
            (CC := α) (extensionHom f) :
          (a : (completionFunctor.obj X).α) → Y.α)
        x :
      Y.α)
    (Completion.extension
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
              { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f) :
          (a : X.carrier) → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier)
        x :
      (Functor.obj
          (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
            fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
            carrier))
          Y).carrier)

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
h :
  ∀ (x : (completionFunctor.obj X).toUniformSpace.carrier),
    Eq (α := Y.toUniformSpace.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
              { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier)
              (extensionHom (X.completionHom ≫ f)).hom :
            (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
          x :
        Y.toUniformSpace.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
              { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f :
            (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
          x :
        Y.toUniformSpace.carrier)
⊢ (extensionHom (X.completionHom ≫ f)).hom = f

Tactic:
ext x
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
x : (completionFunctor.obj X).toUniformSpace.carrier
⊢ Eq (α := Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier)
            (extensionHom (X.completionHom ≫ f)).hom :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)

Tactic:
congr_fun (Completion.extension_comp_coe f.hom.property) x

Premises used: UniformSpace.Completion.coe', UniformSpaceCat.Hom.hom, UniformSpace.Completion.extension_comp_coe, SeparationQuotient.mk, UniformSpace.Completion.extension, congr_fun, AbstractCompletion.extend, Subtype.property, ite
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
x : (completionFunctor.obj X).toUniformSpace.carrier
⊢ Eq (α := Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier)
            (extensionHom (X.completionHom ≫ f)).hom :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : UniformSpaceCat.{u_1}) ↦
            { f : x1.carrier → x2.carrier // UniformContinuous f }) (CC := carrier) f :
          (a : (completionFunctor.obj X).toUniformSpace.carrier) → Y.toUniformSpace.carrier)
        x :
      Y.toUniformSpace.carrier)

Tactic:
exact congr_fun (Completion.extension_comp_coe f.hom.property) x

Premises used: UniformSpaceCat.Hom.hom, UniformSpace.Completion.extension_comp_coe, congr_fun, Subtype.property
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : completionFunctor.obj X ⟶ Y
⊢ InducedCategory.Hom.hom
      ((fun
            (f :
              X ⟶
                Functor.obj
                  (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
                    { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
                    fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD :=
                    carrier))
                  Y) ↦
          extensionHom f)
        ((fun (f : completionFunctor.obj X ⟶ Y) ↦ X.completionHom ≫ f.hom) f)) =
    f.hom

Tactic:
simp
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
        { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
        fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
      Y
x : (completionFunctor.obj X').α
h :
  (↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
            (CC := α) (extensionHom (f ≫ g))) :
        (completionFunctor.obj X').α → Y.α)
      x =
    Completion.extension
      ((↑(Hom.hom g) : X.carrier → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier) ∘
        (↑(Hom.hom f) : X'.carrier → X.carrier))
      x
⊢ (↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
            (CC := α) (extensionHom (f ≫ g))) :
        (completionFunctor.obj X').α → Y.α)
      x =
    Function.comp (β := (completionFunctor.obj X).α)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) (extensionHom g)) :
        (a : (completionFunctor.obj X).α) → Y.α)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
            { f : x1.α → x2.α // UniformContinuous f }) (CC := α) (X := completionFunctor.obj X') (Y :=
            completionFunctor.obj X)
            (ConcreteCategory.ofHom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
              { f : x1.α → x2.α // UniformContinuous f }) (CC := α)
              (Subtype.mk (p := fun (f : Completion X'.carrier → Completion X.carrier) ↦ UniformContinuous f)
                (Completion.map (⇑f.hom' : (a : X'.carrier) → X.carrier)) ⋯))) :
        (a : (completionFunctor.obj X').α) → (completionFunctor.obj X).α)
      x

Tactic:
erw [Completion.extension_map (γ := Y) g.hom.2 f.hom.2]

Premises used: UniformSpaceCat.Hom.hom, UniformSpace.Completion.extension_map, Subtype.property
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
X' X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget₂ CpltSepUniformSpace (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦
        { f : x1.α → x2.α // UniformContinuous f }) (CC := α) UniformSpaceCat (FD :=
        fun (x1 x2 : UniformSpaceCat.{u_1}) ↦ { f : x1.carrier → x2.carrier // UniformContinuous f }) (CD := carrier))
      Y
x : (completionFunctor.obj X').α
⊢ (↑(ConcreteCategory.hom (FC := fun (x1 x2 : CpltSepUniformSpace.{u_1}) ↦ { f : x1.α → x2.α // UniformContinuous f })
            (CC := α) (extensionHom (f ≫ g))) :
        (completionFunctor.obj X').α → Y.α)
      x =
    Completion.extension
      ((↑(Hom.hom g) : X.carrier → ((forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y).carrier) ∘
        (↑(Hom.hom f) : X'.carrier → X.carrier))
      x

Tactic:
rfl
-- Module: Mathlib.Topology.Category.UniformSpace
Goal:
inst : HasLimits UniformSpaceCat
⊢ HasLimits CpltSepUniformSpace

Tactic:
hasLimits_of_reflective <| forget₂ CpltSepUniformSpace UniformSpaceCat.{u}

Premises used: CategoryTheory.hasLimits_of_reflective, CpltSepUniformSpace, CategoryTheory.forget₂, UniformSpaceCat
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClopen s
⊢ IsOpen[inst] s

Tactic:
hs.2

Premises used: And.right
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClopen s
⊢ IsClosed[inst] s

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure[inst] s = s ∧ interior s = s ↔ closure[inst] s ⊆ interior s
⊢ IsClopen s ↔ frontier s = ∅

Tactic:
rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]

Premises used: frontier, closure_eq_iff_isClosed, interior_eq_iff_isOpen, IsClopen, Set.diff_eq_empty
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s = s ∧ interior s = s ↔ closure[inst] s ⊆ interior s

Tactic:
⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩

Premises used: Eq.subset, And.right, And.left, Iff.intro, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine : ∀ (h : closure[inst] s ⊆ interior s), closure[inst] s = s ∧ interior s = s
⊢ closure[inst] s = s ∧ interior s = s ↔ closure[inst] s ⊆ interior s

Tactic:
refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure[inst] s ⊆ interior s
⊢ closure[inst] s = s ∧ interior s = s

Tactic:
⟨(h.trans interior_subset).antisymm subset_closure,
    interior_subset.antisymm (subset_closure.trans h)⟩

Premises used: interior_subset, subset_closure, HasSubset.Subset.trans, HasSubset.Subset.antisymm, And.intro
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure[inst] s ⊆ interior s
⊢ closure[inst] s = s ∧ interior s = s

Tactic:
exact ⟨(h.trans interior_subset).antisymm subset_closure,
    interior_subset.antisymm (subset_closure.trans h)⟩
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ∪ t)

Tactic:
⟨hs.1.union ht.1, hs.2.union ht.2⟩

Premises used: IsClosed.union, IsOpen.union, And.right, And.left, And.intro, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ∩ t)

Tactic:
⟨hs.1.inter ht.1, hs.2.inter ht.2⟩

Premises used: And.right, And.left, And.intro, IsOpen.inter, IsClosed.inter, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClopen.{u} (X := X) ∅

Tactic:
⟨isClosed_empty, isOpen_empty⟩

Premises used: isClosed_empty, And.intro, IsClopen, isOpen_empty
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
⊢ IsClopen.{u} (X := X) univ

Tactic:
⟨isClosed_univ, isOpen_univ⟩

Premises used: isClosed_univ, isOpen_univ, And.intro, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClopen s
⊢ IsClopen sᶜ

Tactic:
⟨hs.2.isClosed_compl, hs.1.isOpen_compl⟩

Premises used: IsClosed.isOpen_compl, IsOpen.isClosed_compl, And.right, And.intro, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClopen sᶜ ↔ IsClopen s

Tactic:
⟨fun h => compl_compl s ▸ IsClopen.compl h, IsClopen.compl⟩

Premises used: compl_compl, Eq.rec, IsClopen.compl, Iff.intro
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s \ t)

Tactic:
hs.inter ht.compl

Premises used: Set.Mem, IsClopen.inter, Set.diff, setOf, IsClopen.compl, Not
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ⇨ t)

Tactic:
simpa [himp_eq] using ht.union hs.compl

Premises used: himp_eq, IsClopen.compl, IsClopen.union
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ×ˢ t)

Tactic:
⟨hs.1.prod ht.1, hs.2.prod ht.2⟩

Premises used: IsClosed.prod, And.right, And.left, And.intro, IsClopen, IsOpen.prod
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Sort u_2
inst_1 : Finite Y
s : Y → Set X
h : ∀ (i : Y), IsClopen (s i)
⊢ IsClopen.{u} (X := X) (⋃ (i : Y), s i)

Tactic:
⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩

Premises used: isClosed_iUnion_of_finite, isOpen_iUnion, And.right, And.left, And.intro, Iff.mp, IsClopen, forall_and
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
s : Set Y
f : Y → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClopen (f i)
⊢ IsClopen.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩

Premises used: And.right, And.left, And.intro, isOpen_biUnion, IsClopen, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
s : Finset Y
f : Y → Set X
h : ∀ i ∈ s, IsClopen (f i)
⊢ IsClopen.{u} (X := X) (⋃ i ∈ s, f i)

Tactic:
s.finite_toSet.isClopen_biUnion h

Premises used: Set.Finite.isClopen_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Sort u_2
inst_1 : Finite Y
s : Y → Set X
h : ∀ (i : Y), IsClopen (s i)
⊢ IsClopen.{u} (X := X) (⋂ (i : Y), s i)

Tactic:
⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩

Premises used: isOpen_iInter_of_finite, And.right, And.left, And.intro, Iff.mp, IsClopen, isClosed_iInter, forall_and
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
s : Set Y
hs : s.Finite
f : Y → Set X
h : ∀ i ∈ s, IsClopen (f i)
⊢ IsClopen.{u} (X := X) (⋂ i ∈ s, f i)

Tactic:
⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩

Premises used: isClosed_biInter, And.right, And.left, And.intro, Set.Finite.isOpen_biInter, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
s : Finset Y
f : Y → Set X
h : ∀ i ∈ s, IsClopen (f i)
⊢ IsClopen.{u} (X := X) (⋂ i ∈ s, f i)

Tactic:
s.finite_toSet.isClopen_biInter h

Premises used: Finset.finite_toSet, Set.Finite.isClopen_biInter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set Y
h : IsClopen s
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsClopen (f ⁻¹' s)

Tactic:
⟨h.1.preimage hf, h.2.preimage hf⟩

Premises used: And.right, And.left, And.intro, IsClosed.preimage, IsClopen, IsOpen.preimage
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
hf : ContinuousOn f s
hs : IsClopen s
ht : IsClopen t
⊢ IsClopen (s ∩ f ⁻¹' t)

Tactic:
⟨ContinuousOn.preimage_isClosed_of_isClosed hf hs.1 ht.1,
    ContinuousOn.isOpen_inter_preimage hf hs.2 ht.2⟩

Premises used: ContinuousOn.preimage_isClosed_of_isClosed, ContinuousOn.isOpen_inter_preimage, And.right, And.left, And.intro, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
⊢ IsClopen (s ∩ a)

Tactic:
⟨?_, IsOpen.inter h.2 ha⟩

Premises used: And.right, And.intro, IsOpen.inter, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
refine : IsClosed[inst] (s ∩ a)
⊢ IsClopen (s ∩ a)

Tactic:
refine ⟨?_, IsOpen.inter h.2 ha⟩
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
⊢ IsClosed[inst] (s ∩ bᶜ)

Tactic:
have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
⊢ IsClosed[inst] (s ∩ bᶜ)

Tactic:
this
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
h₁ : s ∩ a = s ∩ bᶜ
⊢ IsClosed[inst] (s ∩ a)

Tactic:
convert! this using 1
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ

Tactic:
(inter_subset_inter_right s hab.subset_compl_right).antisymm ?_

Premises used: Set.inter_subset_inter_right, Disjoint.subset_compl_right, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
h₁ : s ∩ bᶜ ⊆ s ∩ a
⊢ s ∩ a = s ∩ bᶜ

Tactic:
refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_

Premises used: Set.inter_subset_inter_right, Disjoint.subset_compl_right, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ a

Tactic:
simpa [notMem_of_mem_compl hx₂] using cover hx₁

Premises used: Set.notMem_of_mem_compl
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
this : IsClosed[inst] (s ∩ bᶜ)
x : X
hx₁ : x ∈ s
hx₂ : x ∈ bᶜ
⊢ x ∈ s ∩ a

Tactic:
exact ⟨hx₁, by simpa [notMem_of_mem_compl hx₂] using cover hx₁⟩
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ s ∩ a = s ∩ (s ∩ a)

Tactic:
simp
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
rw : IsClopen (s ∩ (s ∩ a))
⊢ IsClopen (s ∩ a)

Tactic:
rw [show s ∩ a = s ∩ (s ∩ a) by simp]
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ IsClopen (s ∩ (s ∩ a))

Tactic:
isClopen_inter_of_disjoint_cover_clopen h ?_ (h.2.inter ha) (h.2.inter hb) ?_

Premises used: isClopen_inter_of_disjoint_cover_clopen, And.right, IsOpen.inter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_1 : s ⊆ s ∩ a ∪ s ∩ b
refine_2 : Disjoint (s ∩ a) (s ∩ b)
⊢ IsClopen (s ∩ (s ∩ a))

Tactic:
refine isClopen_inter_of_disjoint_cover_clopen h ?_ (h.2.inter ha) (h.2.inter hb) ?_

Premises used: isClopen_inter_of_disjoint_cover_clopen, And.right, IsOpen.inter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_1 : s ⊆ s ∩ (a ∪ b)
⊢ s ⊆ s ∩ a ∪ s ∩ b

Tactic:
rw [← inter_union_distrib_left]

Premises used: Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ (a ∪ b)

Tactic:
subset_inter .rfl cover

Premises used: Set.Subset.rfl, Set.subset_inter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
⊢ s ⊆ s ∩ (a ∪ b)

Tactic:
exact subset_inter .rfl cover

Premises used: Set.Subset.rfl, Set.subset_inter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : s ∩ a ∩ b = ∅
refine_2 : s ∩ a ∩ (s ∩ b) = ∅
refine_2₁ : s ∩ a ∩ (b ∩ s) = ∅
refine_2₂ : s ∩ a ∩ b ∩ s = ∅
refine_2₃ : ∅ ∩ s = ∅
refine_2₄ refine_2₅ : Eq.{u + 1} (α := Set X) ∅ ∅
⊢ Disjoint (s ∩ a) (s ∩ b)

Tactic:
rw [disjoint_iff_inter_eq_empty, inter_comm s b, ← inter_assoc, hab, empty_inter]

Premises used: Set.empty_inter, Set.disjoint_iff_inter_eq_empty, Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
a b : Set X
cover : univ ⊆ a ∪ b
ha : IsOpen[inst] a
hb : IsOpen[inst] b
hab : Disjoint a b
⊢ IsClopen a

Tactic:
univ_inter a ▸ isClopen_inter_of_disjoint_cover_clopen isClopen_univ cover ha hb hab

Premises used: isClopen_inter_of_disjoint_cover_clopen, isClopen_univ, Eq.rec, Set.univ_inter
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : DiscreteTopology X
s : Set X
⊢ IsClopen s

Tactic:
⟨isClosed_discrete _, isOpen_discrete _⟩

Premises used: isClosed_discrete, And.intro, isOpen_discrete, IsClopen
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClopen (X := X ⊕ Y) (range Sum.inl)

Tactic:
⟨isClosed_range_inl, isOpen_range_inl⟩

Premises used: isClosed_range_inl, And.intro, IsClopen, isOpen_range_inl
-- Module: Mathlib.Topology.Clopen
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsClopen (X := X ⊕ Y) (range Sum.inr)

Tactic:
⟨isClosed_range_inr, isOpen_range_inr⟩

Premises used: isOpen_range_inr, isClosed_range_inr, And.intro, IsClopen