awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (hypothesis)
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ [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_2_iff_3 : 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)
Tactic: tfae_have 2 ↔ 3 := epi_iff_surjective π
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (hypothesis)
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
⊢ [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
have tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
Tactic: tfae_have 2 → 1
  | _ => by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (hypothesis)
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), 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
have tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (goal)
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 π
have 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 π
Tactic: erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ Stonean.toCompHaus.obj (X a)) (fun a ↦ Stonean.toCompHaus.map (π a))).out 2 0 :)]
-- Lean 4 proof step from Mathlib.Topology.Category.Stonean.EffectiveEpi (hypothesis)
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 π, 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
have 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 π
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⟩
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Basic (goal)
Goal:
X Y : TopCat
f : (↑X : Type u) ≃ₜ (↑Y : Type u)
⊢ homeoOfIso (isoOfHomeo f) = f
have H : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u)) ((homeoOfIso (isoOfHomeo f) : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
    ((f : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Basic (goal)
Goal:
X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f
have w : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (isoOfHomeo (homeoOfIso f)).hom :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f.hom :
          (a : (↑X : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Basic (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
have mp : IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u)) →
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Basic (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
mp :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) →
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (f ≫ g)) :
        (a : (↑X : Type u)) → (↑Z : Type u)) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
have mpr : IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u)) →
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Basic (goal)
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
h :
  IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
⊢ IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
have h₁ : Eq (α := (↑Y : Type u) → (↑Z : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
    (a : (↑Y : Type u)) → (↑Z : Type u))
  (Function.comp (β := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f ≫ g)) :
      (a : (↑X : Type u)) → (↑Z : Type u))
    (⇑(homeoOfIso (asIso f).symm) : (a : (↑Y : Type u)) → (↑X : Type u)))
Tactic: convert! h.comp (TopCat.homeoOfIso (asIso f).symm).isOpenEmbedding
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
⊢ Eq (α := of (↑X : Type u) ⟶ B) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)
have w : ∀ (x : (↑(of (↑X : Type u)) : Type u)),
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
⊢ Eq (α := of (↑X : Type u) ⟶ B) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)
have w : ∀ (x : (↑(of (↑X : Type u)) : Type u)),
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := sorry } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)
have suffices : g =
  ofHom
    ((hπ.liftEquiv :
        (a :
            { g : C((↑X : Type u), (↑W : Type u)) //
              Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
          C((↑B : Type u), (↑W : Type u)))
      (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
        Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
          (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
            (a : (↑X : Type u)) → (↑B : Type u)))
        (Hom.hom e) sorry))
Tactic: suffices g = ofHom (hπ.liftEquiv ⟨e.hom,
      fun a b hab ↦ CategoryTheory.congr_fun (h
          (ofHom ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.EffectiveEpi (goal)
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
⊢ g =
    ofHom
      ((hπ.liftEquiv :
          (a :
              { g : C((↑X : Type u), (↑W : Type u)) //
                Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
            C((↑B : Type u), (↑W : Type u)))
        (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
          Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
            (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  π) :
              (a : (↑X : Type u)) → (↑B : Type u)))
          (Hom.hom e) ⋯))
have hf : Hom.hom g =
  Hom.hom
    (ofHom
      ((hπ.liftEquiv :
          (a :
              { g : C((↑X : Type u), (↑W : Type u)) //
                Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
            C((↑B : Type u), (↑W : Type u)))
        (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
          Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
            (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  π) :
              (a : (↑X : Type u)) → (↑B : Type u)))
          (Hom.hom e) sorry)))
Tactic: apply hom_ext