awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
    ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      (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) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (X a)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
          x =
        b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
        (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) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
erw :
  (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := toCompHaus.obj B) (fun (a : α) ↦ toCompHaus.obj (X a))
      fun (a : α) ↦ toCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
        (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) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ Stonean.toCompHaus.obj (X a)) (fun a ↦ Stonean.toCompHaus.map (π a))).out 2 0 :)]

Premises used: Stonean.toCompHaus, CategoryTheory.Functor.map, List.TFAE.out, OfNat.ofNat, CompHaus.effectiveEpiFamily_tfae, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := toCompHaus.obj B) (fun (a : α) ↦ toCompHaus.obj (X a))
      fun (a : α) ↦ toCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π

Tactic:
⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Functor.finite_effectiveEpiFamily_of_map, inferInstance, Stonean.toCompHaus, Iff.intro
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := toCompHaus.obj B) (fun (a : α) ↦ toCompHaus.obj (X a))
      fun (a : α) ↦ toCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
        (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) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
tfae_have 3 ↔ 1 := by
    erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ Stonean.toCompHaus.obj (X a)) (fun a ↦ Stonean.toCompHaus.map (π a))).out 2 0 :)]
    exact ⟨fun h ↦ Stonean.toCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
tfae_3_iff_1 :
  (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
        (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) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π
⊢ [EffectiveEpiFamily X π, Epi (X := ∐ X) (Sigma.desc π),
      ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
        ∃ (a : α) (x :
          (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
          (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) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦
                        (↑X.toTop : Type u))
                      (X a)) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                    B)
              x =
            b].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
surj :
  ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
    ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)),
      (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) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (X a)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
          x =
        b
⊢ EffectiveEpiFamily X π

Tactic:
((effectiveEpiFamily_tfae X π).out 2 0).mp surj

Premises used: Stonean.effectiveEpiFamily_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.Category.Stonean.Limits
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi_1 :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) :
              Type ?u.9361)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
              (↑X.toTop : Type ?u.9361))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
            (↑X.toTop : Type ?u.9361))
          Z)
X_1 Y_1 B : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)
f_1 : X_1 ⟶ B
g : Y_1 ⟶ B
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
        (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
      X_1)
    (Y :=
    (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
        (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
      B)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          C((↑(x1.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u),
            (↑(x2.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)) f_1) :
      (a : (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) X_1) →
        (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ HasExplicitPullback (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) f_1 g

Tactic:
⟨extremallyDisconnected_pullback _ hi⟩

Premises used: Stonean.extremallyDisconnected_pullback, CompHausLike.HasProp.mk
-- Module: Mathlib.Topology.Category.Stonean.Limits
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi_1 :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) :
              Type ?u.9361)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.9361}) ↦ ExtremallyDisconnected (↑X : Type ?u.9361))) : Type ?u.9361))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
              (↑X.toTop : Type ?u.9361))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.9361)) ↦
            (↑X.toTop : Type ?u.9361))
          Z)
X_1 Y_1 B : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)
f_1 : X_1 ⟶ B
g : Y_1 ⟶ B
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
        (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
      X_1)
    (Y :=
    (fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
        (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u))
      B)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          C((↑(x1.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u),
            (↑(x2.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) ↦
          (↑(X.toTop (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u))) : Type u)) f_1) :
      (a : (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) X_1) →
        (fun (X : CompHausLike fun (Y : TopCat) ↦ ExtremallyDisconnected (↑Y : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ HasExplicitPullback (P := fun (Y : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑Y : Type u)) f_1 g

Tactic:
exact ⟨extremallyDisconnected_pullback _ hi⟩
-- Module: Mathlib.Topology.Category.Stonean.Limits
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187))) : Type ?u.10187))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187))) : Type ?u.10187))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187))) :
              Type ?u.10187),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187))) :
              Type ?u.10187)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.10187}) ↦ ExtremallyDisconnected (↑X : Type ?u.10187))) : Type ?u.10187))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
              (↑X.toTop : Type ?u.10187))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.10187)) ↦
            (↑X.toTop : Type ?u.10187))
          Z)
⊢ FinitaryExtensive Stonean

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Stonean.Limits
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662))) : Type ?u.10662))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662))) : Type ?u.10662))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662))) :
              Type ?u.10662),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662))) :
              Type ?u.10662)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.10662}) ↦ ExtremallyDisconnected (↑X : Type ?u.10662))) : Type ?u.10662))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
              (↑X.toTop : Type ?u.10662))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.10662)) ↦
            (↑X.toTop : Type ?u.10662))
          Z)
⊢ PreservesFiniteCoproducts toCompHaus

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Stonean.Limits
Goal:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi :
  IsOpenEmbedding (X :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431))) : Type ?u.11431))
      X)
    (Y :=
    (fun (X : CompHausLike fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431))) : Type ?u.11431))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431))) :
              Type ?u.11431),
            (↑(x2.toTop (P := fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431))) :
              Type ?u.11431)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{?u.11431}) ↦ ExtremallyDisconnected (↑X : Type ?u.11431))) : Type ?u.11431))
          f) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
              (↑X.toTop : Type ?u.11431))
            X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type ?u.11431)) ↦
            (↑X.toTop : Type ?u.11431))
          Z)
⊢ PreservesFiniteCoproducts toProfinite

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.TopCat.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier))

Tactic:
⟨_, ⟨adj₁⟩⟩

Premises used: Nonempty.intro, Exists.intro, TopCat.adj₁, CategoryTheory.Functor.IsRightAdjoint.mk