awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
have hc : ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
  IsClosed (X := (↑C : Type u))
    (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
Tactic: have hc : ∀ (J : Finset ι) s, IsClosed ((π_app C (· ∈ J)) ⁻¹' {s}) := by
          intro J s
          refine IsClosed.preimage (π_app C (· ∈ J)).continuous ?_
          exact T1Space.t1 s
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K_1 : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
J K : Finset ι
h : J ≤ K
x : (↑C : Type u)
hx :
  Membership.mem (γ := Set (↑C : Type u))
    (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
      (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ K) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u))
      {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
          (op K)})
    x
⊢ Membership.mem (γ := Set (↑C : Type u))
    (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
      (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
      {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
          (op J)})
    x
have hx₁ : Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u)) (γ :=
  Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
  {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op K)}
  ((π_app (X := X) C fun (x : ι) ↦ x ∈ K : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u)) x :
    (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
Tactic: simp only [Set.mem_preimage] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J_1 K_1 : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
J K : Finset ι
h : J ≤ K
x : (↑C : Type u)
hx :
  Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
    {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op K)}
    ((π_app (X := X) C fun (x : ι) ↦ x ∈ K : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ K) : Type u)) x :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ K) : Type u))
⊢ Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) (γ :=
    Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
    {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)}
    ((π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x :
      (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
have rw : Membership.mem (α := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)) (γ :=
  Set (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
  (singleton (α := (↑(((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).map (homOfLE h).op) :
          (a : (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op K)) : Type u)) →
            (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u))
        ((↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
          (op K)) :
      (↑(((indexFunctor (X := X) (C := C) hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj (op J)) : Type u)))
  ((map (X := X) C (J := Membership.mem J) (K := Membership.mem K) h :
        (a : (↑(obj C (Membership.mem K)) : Type u)) → (↑(obj C (Membership.mem J)) : Type u))
      ((↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
        (op K)) :
    (↑(obj (X := X) C (Membership.mem J)) : Type u))
Tactic: rw [← map_comp_π_app C h, Function.comp_apply,
            hx, ← a.prop (homOfLE h).op]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (hypothesis)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
have H₁ : ∀ (Q₁ Q₂ : Finset ι),
  Q₁ ≤ Q₂ →
    Superset (α := Set (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
        {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op Q₁)})
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
        {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
            (op Q₂)})
Tactic: have H₁ : ∀ (Q₁ Q₂ : Finset ι), Q₁ ≤ Q₂ →
            π_app C (· ∈ Q₁) ⁻¹' {a.val (op Q₁)} ⊇
            π_app C (· ∈ Q₂) ⁻¹' {a.val (op Q₂)} := by
          intro J K h x hx
          simp only [Set.mem_preimage] at hx ⊢
          rw [← map_comp_π_app C h, Function.comp_apply,
            hx, ← a.prop (homOfLE h).op]
          rfl
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Product (goal)
Goal:
ι : Type u
X : ι → Type
inst : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J K : ι → Prop
inst_1 : ∀ (i : ι), T2Space (X i)
inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace.{u} (↑C : Type u)
a :
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (limitCone (indexFunctor (X := X) (C := C) hC)).pt
hc :
  ∀ (J : Finset ι) (s : (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u)),
    IsClosed (X := (↑C : Type u))
      (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
        (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) {s})
H₁ :
  ∀ (Q₁ Q₂ : Finset ι),
    Q₁ ≤ Q₂ →
      Superset (α := Set (↑C : Type u))
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₁) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₁) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₁)})
        (Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ Q₂) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ Q₂) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op Q₂)})
⊢ ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
have obtain : ∀ (x : (↑C : Type u))
  (hx :
    Membership.mem (γ := Set (↑C : Type u))
      (⋂ (J : Finset ι),
        Set.preimage (β := (↑(obj (X := X) C fun (x : ι) ↦ x ∈ J) : Type u))
          (⇑(π_app (X := X) C fun (x : ι) ↦ x ∈ J) : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u))
          {(↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u))
              (op J)})
      x),
  ∃ (x : (↑C : Type u)),
    ∀ (J : Finset ι),
      (π_app (X := X) C fun (x : ι) ↦ x ∈ J : (a : (↑C : Type u)) → (↑(obj C fun (x : ι) ↦ x ∈ J) : Type u)) x =
        (↑a : (j : (Finset ι)ᵒᵖ) → (↑(((indexFunctor hC ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j) : Type u)) (op J)
Tactic: obtain ⟨x, hx⟩ :
            Set.Nonempty (⋂ (J : Finset ι), π_app C (· ∈ J) ⁻¹' {a.val (op J)}) :=
          IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
            (fun J : Finset ι => π_app C (· ∈ J) ⁻¹' {a.val (op J)}) (directed_of_isDirected_le H₁)
            (fun J => (Set.singleton_nonempty _).preimage (surjective_π_app _))
            (fun J => (hc J (a.val (op J))).isCompact) fun J => hc J (a.val (op J))
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Projective (hypothesis)
Goal:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Epi g
⊢ ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f
have hg₁ : Surjective (α :=
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    Y)
  (β :=
  (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
      (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    Z)
  (⇑(ConcreteCategory.hom (FC :=
        fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
          (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
        (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
    (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
      (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Z)
Tactic: rw [epi_iff_surjective] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Projective (goal)
Goal:
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg :
  Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Y)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Z)
⊢ ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f
have obtain : ∀
  (g' :
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Z →
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Y)
  (hg' :
    RightInverse g'
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) g) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              Y) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Z)),
  ∃ (f' : of (Ultrafilter X) ⟶ Y), f' ≫ g = f
Tactic: obtain ⟨g', hg'⟩ := hg.hasRightInverse
-- Lean 4 proof step from Mathlib.Topology.Category.Sequential (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
⊢ CategoryStruct.comp (Y := Y)
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ }))
      (InducedCategory.homMk
        (TopCat.ofHom
          { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ })) =
    𝟙 X
have h : ∀ (x : (↑X.toTop : Type u)),
  Eq (α := (↑X.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ X X
            (CategoryStruct.comp (Y := Y)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := sorry }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := sorry }))) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 X) :
          (a : (↑X.toTop : Type u)) → (↑X.toTop : Type u))
        x :
      (↑X.toTop : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Sequential (goal)
Goal:
X_1 : Type u
inst : TopologicalSpace X_1
inst_1 : SequentialSpace X_1
X Y : Sequential
f : (↑X.toTop : Type u) ≃ₜ (↑Y.toTop : Type u)
⊢ CategoryStruct.comp (Y := X)
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := ⋯ }))
      (InducedCategory.homMk
        (TopCat.ofHom { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := ⋯ })) =
    𝟙 Y
have h : ∀ (x : (↑Y.toTop : Type u)),
  Eq (α := (↑Y.toTop : Type u))
    ((@ConcreteCategory.hom Sequential instCategory
            (fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u)))
            (fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) _ _ Y Y
            (CategoryStruct.comp (Y := X)
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f.symm : (a : (↑Y.toTop : Type u)) → (↑X.toTop : Type u)), continuous_toFun := sorry }))
              (InducedCategory.homMk
                (TopCat.ofHom
                  { toFun := (⇑f : (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)), continuous_toFun := sorry }))) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : Sequential.{u}) ↦ C((↑x1.toTop : Type u), (↑x2.toTop : Type u))) (CC :=
            fun (X : Sequential.{u}) ↦ (↑X.toTop : Type u)) (𝟙 Y) :
          (a : (↑Y.toTop : Type u)) → (↑Y.toTop : Type u))
        x :
      (↑Y.toTop : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Adjunctions (hypothesis)
Goal:
X : Type u
Y : Stonean
this : TopologicalSpace X := ⊥
⊢ (stoneCechObj X ⟶ Y) ≃
    (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
have this₁ : DiscreteTopology X
Tactic: haveI : DiscreteTopology X := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Adjunctions (goal)
Goal:
X : Type u
Y : Stonean
this_1 : TopologicalSpace X := ⊥
this : DiscreteTopology X
⊢ (stoneCechObj X ⟶ Y) ≃
    (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
have refine : (toCompHaus.obj (stoneCechObj X) ⟶ toCompHaus.obj Y) ≃
  (X ⟶ (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
Tactic: refine fullyFaithfulToCompHaus.homEquiv.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
Goal:
X : CompHaus
inst : Projective X
⊢ ExtremallyDisconnected.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
have h : CompactT2.Projective.{u} (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
Tactic: apply CompactT2.Projective.extremallyDisconnected
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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'
have 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')
Tactic: rw [CompHaus.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (hypothesis)
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 }
⊢ ∃ (h : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
have this : Epi g'
Tactic: have : Epi g' := by
    rw [CompHaus.epi_iff_surjective]
    assumption
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.Basic (goal)
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.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) → A), Continuous[_, inst_1] h ∧ g ∘ h = f
have 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
Tactic: obtain ⟨h, hh⟩ := Projective.factors f' g'