awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
h :
  ∀ [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous f →
      Continuous g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous h ∧ g ∘ h = f
⊢ ∀ [inst : TopologicalSpace A] [inst_1 : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous f →
      Continuous g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
h :
  ∀ [inst : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous f →
      Continuous[inst_1, _] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∀ [inst : TopologicalSpace B] [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous f →
      Continuous[inst_1, _] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
h :
  ∀ [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∀ [CompactSpace A] [T2Space A] [CompactSpace B] [T2Space B]
    {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
h :
  ∀ [T2Space A] [CompactSpace B] [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B}
    {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∀ [T2Space A] [CompactSpace B] [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B}
    {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
h :
  ∀ [CompactSpace B] [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∀ [CompactSpace B] [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
h :
  ∀ [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∀ [T2Space B] {f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B} {g : A → B},
    Continuous[_, inst_2] f →
      Continuous[inst_1, inst_2] g →
        Function.Surjective g →
          ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
_
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
rw :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) A')
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B')
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) g') :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A') →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
⊢ Epi g'

Tactic:
rw [CompHaus.epi_iff_surjective]

Premises used: CompHaus.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) A')
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B')
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) g') :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A') →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')

Tactic:
assumption
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
⊢ Epi g'

Tactic:
have : Epi g' := by
    rw [CompHaus.epi_iff_surjective]
    assumption
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h :
  ∀ (h : X ⟶ A') (hh : h ≫ g' = f'),
    ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
⊢ ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
obtain ⟨h, hh⟩ := Projective.factors f' g'

Premises used: CategoryTheory.Projective.factors
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
⊢ ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
⟨h, h.hom.hom.2, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, ContinuousMap.continuous_toFun, TopCat.Hom.hom, And.intro, Exists.intro, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
h₁ :
  g ∘
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) h) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A') =
    f
⊢ ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f

Tactic:
refine ⟨h, h.hom.hom.2, ?_⟩
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
h₁ :
  ∀ (t : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
    (g ∘
          (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) h) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A'))
        t =
      f t
⊢ g ∘
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) h) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A') =
    f

Tactic:
ext t
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
hh : h ≫ g' = f'
t : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
⊢ Eq (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (h ≫ g') :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f' :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')

Tactic:
apply_fun (fun e => e t) at hh
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
t : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hh :
  Eq (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (h ≫ g') :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f' :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')
⊢ (g ∘
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) h) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A'))
      t =
    f t

Tactic:
hh
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : CompHaus
inst : Projective X
A B : Type u
inst_1 : TopologicalSpace A
inst_2 : TopologicalSpace B
inst_3 : CompactSpace A
inst_4 : T2Space A
inst_5 : CompactSpace B
inst_6 : T2Space B
f : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → B
g : A → B
hf : Continuous[_, inst_2] f
hg : Continuous[inst_1, inst_2] g
hsurj : Function.Surjective g
A' : CompHaus := of A
B' : CompHaus := of B
f' : X ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := f, continuous_toFun := hf }
g' : A' ⟶ B' := CompHausLike.ofHom (fun (x : TopCat.{u}) ↦ True) { toFun := g, continuous_toFun := hg }
this : Epi g'
h : X ⟶ A'
t : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hh :
  Eq (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) (h ≫ g') :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f' :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B')
        t :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        B')
⊢ (g ∘
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) h) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) A'))
      t =
    f t

Tactic:
exact hh
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : ExtremallyDisconnected X
⊢ HasProp (fun (Y : TopCat.{u_1}) ↦ ExtremallyDisconnected.{u_1} (↑Y : Type u_1)) X

Tactic:
⟨(inferInstance : ExtremallyDisconnected X)⟩

Premises used: inferInstance, CompHausLike.HasProp.mk
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Stonean
⊢ ExtremallyDisconnected.{u}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)

Tactic:
X.prop

Premises used: CompHausLike.prop
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Type u_1
inst : Finite X
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
dsimp : ExtremallyDisconnected X
⊢ ExtremallyDisconnected.{u_1} (↑((CompHaus.of X).toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Type u_1
inst : Finite X
inst_1 : TopologicalSpace X
inst_2 : DiscreteTopology X
open_closure :
  ∀ (U : Set X),
    IsOpen[(CompHaus.of X).toTop.str] U → IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)
⊢ ExtremallyDisconnected X

Tactic:
constructor
-- 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
open_closure :
  IsOpen[(CompHaus.of X).toTop.str] U → IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)
⊢ IsOpen[(CompHaus.of X).toTop.str] U → IsOpen[(CompHaus.of X).toTop.str] (closure[(CompHaus.of X).toTop.str] U)

Tactic:
_