awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Type u_1
inst : Finite X
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
U : Set X
h : IsOpen[(CompHaus.of X).toTop.str] U
⊢ IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)

Tactic:
apply isOpen_discrete (closure U)

Premises used: closure, isOpen_discrete
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
⊢ Epi f ↔
    Function.Surjective (α :=
      (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))
        X)
      (β :=
      (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))
        Y)
      (⇑(ConcreteCategory.hom (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)) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)

Tactic:
⟨?_, fun h => ConcreteCategory.epi_of_surjective f h⟩

Premises used: CategoryTheory.ConcreteCategory.epi_of_surjective, Iff.intro
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
refine :
  Epi f →
    Function.Surjective (α :=
      (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))
        X)
      (β :=
      (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))
        Y)
      (⇑(ConcreteCategory.hom (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)) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)
⊢ Epi f ↔
    Function.Surjective (α :=
      (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))
        X)
      (β :=
      (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))
        Y)
      (⇑(ConcreteCategory.hom (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)) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
              X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)

Tactic:
refine ⟨?_, fun h => ConcreteCategory.epi_of_surjective f h⟩
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
by_contra! :
  ∀
    (hy :
      ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
        (ConcreteCategory.hom (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))
                f :
              (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
            a ≠
          y),
    False
⊢ ∃ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
    (ConcreteCategory.hom (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)) f :
          (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
        a =
      y

Tactic:
by_contra! hy
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hy :
  ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
    (ConcreteCategory.hom (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)) f :
          (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
        a ≠
      y
C : Set
  ((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))
    Y) :=
  Set.range (ι :=
    (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))
      X)
    (⇑(ConcreteCategory.hom (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)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)
⊢ IsClosed C

Tactic:
have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hy :
  ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
    (ConcreteCategory.hom (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)) f :
          (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
        a ≠
      y
C : Set
  ((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))
    Y) :=
  Set.range (ι :=
    (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))
      X)
    (⇑(ConcreteCategory.hom (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)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)
hC : IsClosed C
U : Set
  ((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))
    Y) :=
  Cᶜ
⊢ U ∈ 𝓝 y

Tactic:
simp only [U, C, Set.mem_range, hy, exists_false, not_false_eq_true, hC.compl_mem_nhds]

Premises used: Set.mem_range, IsClosed.compl_mem_nhds, exists_false, not_false_eq_true
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Stonean
f : X ⟶ Y
h : Epi f
y : (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hy :
  ∀ (a : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)),
    (ConcreteCategory.hom (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)) f :
          (a : (↑X.toTop : Type u_1)) → (↑Y.toTop : Type u_1))
        a ≠
      y
C : Set
  ((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))
    Y) :=
  Set.range (ι :=
    (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))
      X)
    (⇑(ConcreteCategory.hom (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)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) Y)
hC : IsClosed C
U : Set
  ((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))
    Y) :=
  Cᶜ
⊢ U ∈ 𝓝 y

Tactic:
have hUy : U ∈ 𝓝 y := by
    simp only [U, C, Set.mem_range, hy, exists_false, not_false_eq_true, hC.compl_mem_nhds]
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
_ : ∀ [Epi f], ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ
⊢ ∀ [Epi f], ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
⊢ ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
haveI : ExtremallyDisconnected (toCompHaus.obj X).toTop := X.prop
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this : ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
rwa rwa₁ rwa₂ rwa₃ : Epi f
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      C)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) B) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) C)

Tactic:
rwa [← CompHaus.epi_iff_surjective]

Premises used: CompHaus.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this : ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      C)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) B) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) C)

Tactic:
have hf : Function.Surjective f := by rwa [← CompHaus.epi_iff_surjective]
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this : ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
hf :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      C)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) B) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) C)
obtain :
  ∀
    (f' :
      (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
        (↑(B.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
    (h :
      Continuous f' ∧
        Eq (α :=
          (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
            (↑(C.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
          ((⇑(TopCat.Hom.hom f.hom) : (a : (↑B.toTop : Type u_1)) → (↑C.toTop : Type u_1)) ∘ f')
          (⇑(TopCat.Hom.hom φ.hom) : (a : (↑(toCompHaus.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))),
    ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ
⊢ ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ

Tactic:
obtain ⟨f', h⟩ := CompactT2.ExtremallyDisconnected.projective φ.hom.hom.continuous
      f.hom.hom.continuous
      hf

Premises used: ContinuousMap.continuous, TopCat.Hom.hom, CompactT2.ExtremallyDisconnected.projective, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : CompHaus
φ : toCompHaus.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this : ExtremallyDisconnected.{u_1} (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
hf :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      C)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) B) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) C)
f' :
  (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
    (↑(B.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)
h :
  Continuous f' ∧
    Eq (α :=
      (↑((toCompHaus.obj X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1) →
        (↑(C.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      ((⇑(TopCat.Hom.hom f.hom) : (a : (↑B.toTop : Type u_1)) → (↑C.toTop : Type u_1)) ∘ f')
      (⇑(TopCat.Hom.hom φ.hom) : (a : (↑(toCompHaus.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))
h₁ : ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := f', continuous_toFun := ⋯ } ≫ f = φ
⊢ ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ

Tactic:
use ofHom _ ⟨f', h.left⟩

Premises used: CompHausLike.ofHom, ContinuousMap.mk, And.left
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
_ : ∀ [Epi f], ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ
⊢ ∀ [Epi f], ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst : Epi f
⊢ ExtremallyDisconnected.{u_1}
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1)

Tactic:
haveI : ExtremallyDisconnected (toProfinite.obj X) := X.prop
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst : Epi f
this :
  ExtremallyDisconnected.{u_1}
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1)
rwa rwa₁ rwa₂ rwa₃ : Epi f
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
      B)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
      C)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)) f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            B) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) C)

Tactic:
rwa [← Profinite.epi_iff_surjective]

Premises used: Profinite.epi_iff_surjective