awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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))
⊢ ∃ (f' : toCompHaus.obj X ⟶ B), f' ≫ f = φ
have h₁ : ofHom (fun (x : TopCat.{u_1}) ↦ True) { toFun := f', continuous_toFun := sorry } ≫ f = φ
Tactic: use ofHom _ ⟨f', h.left⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
Goal:
X : Stonean
B C : Profinite
φ : toProfinite.obj X ⟶ C
f : B ⟶ C
inst : Epi f
⊢ ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
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)
⊢ ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ
have 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)
Tactic: have hf : Function.Surjective f := by rwa [← Profinite.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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 ⟶ B), f' ≫ f = φ
have 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 = φ
Tactic: obtain ⟨f', h⟩ := CompactT2.ExtremallyDisconnected.projective φ.hom.hom.continuous
      f.hom.hom.continuous
      hf
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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))
⊢ ∃ (f' : toProfinite.obj X ⟶ B), f' ≫ f = φ
have h₁ : ofHom (fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) { toFun := f', continuous_toFun := sorry } ≫
    f =
  φ
Tactic: use ofHom _ ⟨f', h.left⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
Goal:
X B C : Stonean
φ : X ⟶ C
f : B ⟶ C
inst : Epi f
⊢ ∃ (f' : X ⟶ B), f' ≫ f = φ
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
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)
⊢ ∃ (f' : X ⟶ B), f' ≫ f = φ
have 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)
Tactic: have hf : Function.Surjective f := by rwa [← Stonean.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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 ⟶ B), f' ≫ f = φ
have 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 = φ
Tactic: obtain ⟨f', h⟩ := CompactT2.ExtremallyDisconnected.projective φ.hom.hom.continuous
      f.hom.hom.continuous
      hf
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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))
⊢ ∃ (f' : X ⟶ B), f' ≫ f = φ
have h₁ : ofHom (fun (X : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑X : Type u_1)) { toFun := f', continuous_toFun := sorry } ≫
    f =
  φ
Tactic: use ofHom _ ⟨f', h.left⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
Goal:
X : CompHaus
⊢ Projective X ↔ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
have mp : Projective X → ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
Goal:
X : CompHaus
mp : Projective X → ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
⊢ Projective X ↔ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
have mpr : ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → Projective X
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
Goal:
X : CompHaus
h : Projective X
⊢ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
have mp : ExtremallyDisconnected.{u}
  (↑(X.toStonean.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)
Tactic: change ExtremallyDisconnected X.toStonean
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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
have mpr : Projective X'.compHaus
Tactic: change Projective X'.compHaus
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
Goal:
X : Profinite
⊢ Epi (π X)
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
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)
⊢ Epi (π X)
have 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))
Tactic: rw [CompHaus.epi_iff_surjective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
Goal:
X : Profinite
hX :
  ExtremallyDisconnected.{u}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Projective X
have change : Projective
  (Stonean.toProfinite.obj
    (CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
      (X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) sorry))
Tactic: change Projective (Stonean.toProfinite.obj ⟨X.toTop, inferInstance⟩)
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (hypothesis)
Goal:
B X : Stonean
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π,
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          X)
        (β :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          B)
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
              B)].TFAE
have tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance