awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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:
have hf : Function.Surjective f := by rwa [← Profinite.epi_iff_surjective]
-- 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)
hf :
  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)
obtain :
  ∀
    (f' :
      (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1) →
        (↑(B.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
    (h :
      Continuous f' ∧
        Eq (α :=
          (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
              Type u_1) →
            (↑(C.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : 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 : (↑(toProfinite.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))),
    ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ
⊢ ∃ (f' : toProfinite.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 : 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)
hf :
  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)
f' :
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
      Type u_1) →
    (↑(B.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)
h :
  Continuous f' ∧
    Eq (α :=
      (↑((toProfinite.obj X).toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
          Type u_1) →
        (↑(C.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : 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 : (↑(toProfinite.obj X).toTop : Type u_1)) → (↑C.toTop : Type u_1))
h₁ :
  ofHom (fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))
        { toFun := f', continuous_toFun := ⋯ } ≫
      f =
    φ
⊢ ∃ (f' : toProfinite.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 B C : Stonean
φ : X ⟶ C
f : B ⟶ C
_ : ∀ [Epi f], ∃ (f' : X ⟶ B), f' ≫ f = φ
⊢ ∀ [Epi f], ∃ (f' : X ⟶ B), f' ≫ f = φ

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

Tactic:
haveI : ExtremallyDisconnected X.toTop := X.prop
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst : Epi f
this :
  ExtremallyDisconnected.{u_1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{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}) ↦ 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))
      B)
    (β :=
    (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))
      C)
    (⇑(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))
            B) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) C)

Tactic:
rwa [← Stonean.epi_iff_surjective]

Premises used: Stonean.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst : Epi f
this :
  ExtremallyDisconnected.{u_1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
⊢ 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))
      B)
    (β :=
    (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))
      C)
    (⇑(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))
            B) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) C)

Tactic:
have hf : Function.Surjective f := by rwa [← Stonean.epi_iff_surjective]
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst : Epi f
this :
  ExtremallyDisconnected.{u_1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hf :
  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))
      B)
    (β :=
    (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))
      C)
    (⇑(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))
            B) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) C)
obtain :
  ∀
    (f' :
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1) →
        (↑(B.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1))
    (h :
      Continuous f' ∧
        Eq (α :=
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1) →
            (↑(C.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : 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 : (↑X.toTop : Type u_1)) → (↑C.toTop : Type u_1))),
    ∃ (f' : X ⟶ B), f' ≫ f = φ
⊢ ∃ (f' : 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 B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst : Epi f
this :
  ExtremallyDisconnected.{u_1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
hf :
  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))
      B)
    (β :=
    (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))
      C)
    (⇑(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))
            B) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) C)
f' :
  (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1) →
    (↑(B.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1)
h :
  Continuous f' ∧
    Eq (α :=
      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : Type u_1) →
        (↑(C.toTop (P := fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1))) : 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 : (↑X.toTop : Type u_1)) → (↑C.toTop : Type u_1))
h₁ :
  ofHom (fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) { toFun := f', continuous_toFun := ⋯ } ≫
      f =
    φ
⊢ ∃ (f' : 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 : CompHaus
⊢ Epi (π X)

Tactic:
(projectivePresentation X).epi

Premises used: CompHaus.presentation.π, CompHaus.projectivePresentation, CategoryTheory.ProjectivePresentation.epi
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : CompHaus
Z : Stonean
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Premises used: CompHaus.lift
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
mp : Projective X → ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
mpr : ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → Projective X
⊢ Projective X ↔ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
h : Projective X
mp :
  ExtremallyDisconnected.{u}
    (↑(X.toStonean.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)
⊢ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)

Tactic:
change ExtremallyDisconnected X.toStonean

Premises used: TopCat.carrier, CompHausLike.toTop, CompHaus.toStonean, ExtremallyDisconnected
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected.{u}
    (↑(X.toStonean.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
h : ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
X' : Stonean :=
  CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
    (X.toTop (P := fun (x : TopCat.{u}) ↦ True)) ⋯
mpr : Projective X'.compHaus
⊢ Projective X

Tactic:
change Projective X'.compHaus

Premises used: Stonean.compHaus, CategoryTheory.Projective
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
h : ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
X' : Stonean :=
  CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
    (X.toTop (P := fun (x : TopCat.{u}) ↦ True)) ⋯
⊢ Projective X'.compHaus

Tactic:
apply Stonean.instProjectiveCompHausCompHaus

Premises used: Stonean.instProjectiveCompHausCompHaus
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
⊢ Epi.{u_1, u_1 + 1} (X :=
    ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation)
    (ProjectivePresentation.f (profiniteToCompHaus.obj X).projectivePresentation)

Tactic:
have := (profiniteToCompHaus.obj X).projectivePresentation.epi
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
this :
  Epi.{u_1, u_1 + 1} (X :=
    ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation)
    (ProjectivePresentation.f (profiniteToCompHaus.obj X).projectivePresentation)
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation))
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (profiniteToCompHaus.obj X))
    (⇑(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)) (X :=
          ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation)
          (ProjectivePresentation.f (profiniteToCompHaus.obj X).projectivePresentation)) :
      (a :
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1))
            (profiniteToCompHaus.obj X).projectivePresentation.p) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (profiniteToCompHaus.obj X))

Tactic:
rw [CompHaus.epi_iff_surjective] at this

Premises used: CompHaus.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
this :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation))
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (profiniteToCompHaus.obj X))
    (⇑(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)) (X :=
          ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation)
          (ProjectivePresentation.f (profiniteToCompHaus.obj X).projectivePresentation)) :
      (a :
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1))
            (profiniteToCompHaus.obj X).projectivePresentation.p) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (profiniteToCompHaus.obj X))
⊢ 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))
      (Stonean.toProfinite.obj X.presentation))
    (β :=
    (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))
      X)
    (⇑(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))
          (π X)) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            (Stonean.toProfinite.obj X.presentation)) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) X)

Tactic:
this