awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
H₁ :
  ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ≤ Q₂ →
      Superset (α := Set (↑C : Type u))
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₁)})
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₂)})
⊢ Set.Nonempty.{u} (α := (↑C : Type u))
    (⋂ (J : Finset ι),
      Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
        {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op J)})

Tactic:
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
            (fun J : Finset ι => π_app C (· ∈ J) ⁻¹' {a.val (op J)}) (directed_of_isDirected_le H₁)
            (fun J => (Set.singleton_nonempty _).preimage (surjective_π_app _))
            (fun J => (hc J (a.val (op J))).isCompact) fun J => hc J (a.val (op J))

Premises used: Set.singleton_nonempty, Membership.mem, Profinite.IndexFunctor.surjective_π_app, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, directed_of_isDirected_le, Set.preimage, Opposite.op, IsClosed.isCompact, Set.Nonempty.preimage, Singleton.singleton, Subtype.val, DFunLike.coe, Profinite.IndexFunctor.π_app
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
H₁ :
  ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ≤ Q₂ →
      Superset (α := Set (↑C : Type u))
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₁)})
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₂)})
x : (↑C : Type u)
hx :
  Membership.mem (γ := Set (↑C : Type u))
    (⋂ (J : Finset ι),
      Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
        {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op J)})
    x
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)

Tactic:
⟨x, Set.mem_iInter.1 hx⟩

Premises used: Set.mem_iInter, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Category.Profinite.Product
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
H₁ :
  ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ≤ Q₂ →
      Superset (α := Set (↑C : Type u))
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₁)})
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₂)})
x : (↑C : Type u)
hx :
  Membership.mem (γ := Set (↑C : Type u))
    (⋂ (J : Finset ι),
      Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
        {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op J)})
    x
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)

Tactic:
exact ⟨x, Set.mem_iInter.1 hx⟩
-- Module: Mathlib.Topology.Category.Profinite.Projective
Goal:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Z)

Tactic:
rw [epi_iff_surjective] at hg

Premises used: Profinite.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Profinite.Projective
Goal:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Z)
obtain :
  ∀
    (g' :
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          Z →
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          Y)
    (hg' :
      RightInverse g'
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                Y) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              Z)),
    ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f
⊢ ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f

Tactic:
obtain ⟨g', hg'⟩ := hg.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : SequentialSpace X
⊢ sequentialToTop.Full

Tactic:
inferInstanceAs (inducedFunctor _).Full

Premises used: _private.0.Sequential.instFullTopCatSequentialToTop._proof_1
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : SequentialSpace X
⊢ sequentialToTop.Faithful

Tactic:
inferInstanceAs (inducedFunctor _).Faithful

Premises used: _private.0.Sequential.instFaithfulTopCatSequentialToTop._proof_1
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
h :
  ∀ (x : (↑X.toTop : Type u)),
    Eq (α := (↑X.toTop : Type u))
      ((@ConcreteCategory.hom Sequential instCategory
              (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
              (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ X X
              (CategoryStruct.comp (Y := Y)
                (InducedCategory.homMk
                  (TopCat.ofHom
                    { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))
                (InducedCategory.homMk
                  (TopCat.ofHom
                    { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))) :
            (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
          x :
        (↑X.toTop : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
              fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 X) :
            (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
          x :
        (↑X.toTop : Type u))
⊢ CategoryStruct.comp (Y := Y)
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))
      (InducedCategory.homMk
        (TopCat.ofHom
          { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ })) =
    𝟙 X

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
x : (↑X.toTop : Type u)
⊢ Eq (α := (↑X.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ X X
            (CategoryStruct.comp (Y := Y)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 X) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))

Tactic:
f.symm_apply_apply x

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
x : (↑X.toTop : Type u)
⊢ Eq (α := (↑X.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ X X
            (CategoryStruct.comp (Y := Y)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 X) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))

Tactic:
exact f.symm_apply_apply x

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
h :
  ∀ (x : (↑Y.toTop : Type u)),
    Eq (α := (↑Y.toTop : Type u))
      ((@ConcreteCategory.hom Sequential instCategory
              (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
              (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ Y Y
              (CategoryStruct.comp (Y := X)
                (InducedCategory.homMk
                  (TopCat.ofHom
                    { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))
                (InducedCategory.homMk
                  (TopCat.ofHom
                    { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))) :
            (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
          x :
        (↑Y.toTop : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
              fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 Y) :
            (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
          x :
        (↑Y.toTop : Type u))
⊢ CategoryStruct.comp (Y := X)
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ })) =
    𝟙 Y

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
x : (↑Y.toTop : Type u)
⊢ Eq (α := (↑Y.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ Y Y
            (CategoryStruct.comp (Y := X)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 Y) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))

Tactic:
f.apply_symm_apply x

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Category.Sequential
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
x : (↑Y.toTop : Type u)
⊢ Eq (α := (↑Y.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ Y Y
            (CategoryStruct.comp (Y := X)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 Y) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))

Tactic:
exact f.apply_symm_apply x

Premises used: Homeomorph.apply_symm_apply
-- Module: Mathlib.Topology.Category.Stonean.Adjunctions
Goal:
X : Type u
Y : Stonean
this : TopologicalSpace X := ⊥
⊢ DiscreteTopology X

Tactic:
haveI : DiscreteTopology X := ⟨rfl⟩
-- Module: Mathlib.Topology.Category.Stonean.Adjunctions
Goal:
X : Type u
Y : Stonean
this_1 : TopologicalSpace X := ⊥
this : DiscreteTopology X
refine :
  (toCompHaus.obj (stoneCechObj X) ⟶ toCompHaus.obj Y) ≃
    (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
⊢ (stoneCechObj X ⟶ Y) ≃
    (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))

Tactic:
refine fullyFaithfulToCompHaus.homEquiv.trans ?_

Premises used: Equiv.trans, CategoryTheory.Functor.FullyFaithful.homEquiv, Stonean.fullyFaithfulToCompHaus
-- Module: Mathlib.Topology.Category.Stonean.Adjunctions
Goal:
X : Type u
Y : Stonean
this_1 : TopologicalSpace X := ⊥
this : DiscreteTopology X
⊢ (toCompHaus.obj (stoneCechObj X) ⟶ toCompHaus.obj Y) ≃
    (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))

Tactic:
exact (_root_.stoneCechEquivalence (TopCat.of X) (toCompHaus.obj Y)).trans
    (TopCat.adj₁.homEquiv _ _)

Premises used: Equiv.trans, stoneCechEquivalence, Stonean.toCompHaus, TopCat.adj₁, CategoryTheory.Adjunction.homEquiv, TopCat.of, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.Stonean.Adjunctions
Goal:
⊢ Limits.PreservesLimits
    (forget Stonean (FC :=
      fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
      C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1),
        (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))
      (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)))

Tactic:
rightAdjoint_preservesLimits stoneCechAdjunction

Premises used: CategoryTheory.Adjunction.rightAdjoint_preservesLimits, Stonean.stoneCechAdjunction
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
h : CompactT2.Projective.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
⊢ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)

Tactic:
apply CompactT2.Projective.extremallyDisconnected

Premises used: CompactT2.Projective.extremallyDisconnected