awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
⊢ Function.Surjective (α := (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type (u_1 + 1)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1 + 1}) ↦ C((↑X : Type (u_1 + 1)), (↑Y : Type (u_1 + 1))))
          (CC := TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) →
        (↑((𝟭 TopCat).obj X) : Type (u_1 + 1)))

Tactic:
(topCatAdjunctionCounit_bijective _).2

Premises used: CondensedSet.topCatAdjunctionCounit_bijective, And.right
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
⊢ Function.Surjective (α := (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) (β :=
    (↑(Functor.obj (𝟭 TopCat) X) : Type (u_1 + 1)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1 + 1}) ↦ C((↑X : Type (u_1 + 1)), (↑Y : Type (u_1 + 1))))
          (CC := TopCat.carrier) (topCatAdjunction.counit.app X)) :
      (a : (↑((topCatToCondensedSet ⋙ condensedSetToTopCat).obj X) : Type (u_1 + 1))) →
        (↑((𝟭 TopCat).obj X) : Type (u_1 + 1)))

Tactic:
exact (topCatAdjunctionCounit_bijective _).2

Premises used: CondensedSet.topCatAdjunctionCounit_bijective, And.right
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : CondensedSet
⊢ topCatToCondensedSet.Faithful

Tactic:
topCatAdjunction.faithful_R_of_epi_counit_app

Premises used: CondensedSet.topCatAdjunction, CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
h :
  ∀ {Y : Type (u + 1)} [tY : TopologicalSpace Y] (f : (↑X.toTopCat : Type (u + 1)) → Y),
    (∀ (S : CompHaus.{u})
        (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
        Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))) →
      Continuous f
⊢ UCompactlyGeneratedSpace.{u, u + 1} (↑X.toTopCat : Type (u + 1))

Tactic:
apply uCompactlyGeneratedSpace_of_continuous_maps

Premises used: uCompactlyGeneratedSpace_of_continuous_maps
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
Y : Type (u + 1)
h :
  ∀ [tY : TopologicalSpace Y] (f : (↑X.toTopCat : Type (u + 1)) → Y),
    (∀ (S : CompHaus.{u})
        (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
        Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))) →
      Continuous f
⊢ ∀ [tY : TopologicalSpace Y] (f : (↑X.toTopCat : Type (u + 1)) → Y),
    (∀ (S : CompHaus.{u})
        (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
        Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))) →
      Continuous f

Tactic:
_
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
Y : Type (u + 1)
tY : TopologicalSpace Y
f : (↑X.toTopCat : Type (u + 1)) → Y
h :
  ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))
h₁ :
  ∀ (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)),
    Continuous (Y := Y)
      fun
        (a :
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      (f ∘ X.coinducingCoprod)
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)
⊢ Continuous f

Tactic:
rw [continuous_coinduced_dom, continuous_sigma_iff]

Premises used: continuous_coinduced_dom, continuous_sigma_iff
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
Y : Type (u + 1)
tY : TopologicalSpace Y
f : (↑X.toTopCat : Type (u + 1)) → Y
h :
  ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))
⊢ ∀ (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)),
    Continuous (Y := Y)
      fun
        (a :
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      (f ∘ X.coinducingCoprod)
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)

Tactic:
fun ⟨S, s⟩ ↦ h S ⟨_, continuous_coinducingCoprod X _⟩

Premises used: _private.0.CondensedSet.toTopCatMap.match_1, Continuous, ContinuousMap.mk, Function.comp, CondensedSet.continuous_coinducingCoprod, Sigma.mk, _private.0.CondensedSet.coinducingCoprod
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
Y : Type (u + 1)
tY : TopologicalSpace Y
f : (↑X.toTopCat : Type (u + 1)) → Y
h :
  ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X.toTopCat : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      (f ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X.toTopCat : Type (u + 1))))
⊢ ∀ (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)),
    Continuous (Y := Y)
      fun
        (a :
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      (f ∘ X.coinducingCoprod)
        (Sigma.mk (β :=
          fun (i : (S : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ↦
          (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u))
          i a)

Tactic:
exact fun ⟨S, s⟩ ↦ h S ⟨_, continuous_coinducingCoprod X _⟩
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 X : CondensedSet
⊢ UCompactlyGeneratedSpace.{u, u + 1} (↑(condensedSetToTopCat.obj X) : Type (u + 1))

Tactic:
inferInstanceAs (UCompactlyGeneratedSpace.{u, u + 1} X.toTopCat)

Premises used: _private.0.CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat._proof_1
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
inst : UCompactlyGeneratedSpace.{u, u + 1} (↑X : Type (u + 1))
h :
  ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      ((topCatAdjunctionCounitEquiv X).invFun ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X : Type (u + 1))))
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun

Tactic:
apply continuous_from_uCompactlyGeneratedSpace

Premises used: continuous_from_uCompactlyGeneratedSpace
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
inst : UCompactlyGeneratedSpace.{u, u + 1} (↑X : Type (u + 1))
⊢ ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      ((topCatAdjunctionCounitEquiv X).invFun ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X : Type (u + 1))))

Tactic:
fun _ _ ↦ continuous_coinducingCoprod X.toCondensedSet _

Premises used: ContinuousMap.comp, CondensedSet.continuous_coinducingCoprod, TopCat.toCondensedSet, ContinuousMap.const, _private.0.CondensedSet.coinducingCoprod
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : TopCat
inst : UCompactlyGeneratedSpace.{u, u + 1} (↑X : Type (u + 1))
⊢ ∀ (S : CompHaus.{u}) (g : C((↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u), (↑X : Type (u + 1)))),
    Continuous (X := (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
      ((topCatAdjunctionCounitEquiv X).invFun ∘ (⇑g : (a : (↑S.toTop : Type u)) → (↑X : Type (u + 1))))

Tactic:
exact fun _ _ ↦ continuous_coinducingCoprod X.toCondensedSet _

Premises used: CondensedSet.continuous_coinducingCoprod, TopCat.toCondensedSet
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X : CondensedSet
rw : ∀ (X : CompactlyGenerated.{u_1, u_1 + 1}), IsIso (compactlyGeneratedAdjunction.counit.app X)
⊢ IsIso compactlyGeneratedAdjunction.counit

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : CompactlyGenerated
⊢ IsIso (compactlyGeneratedAdjunction.counit.app X)

Tactic:
inferInstanceAs (IsIso (compactlyGeneratedAdjunctionCounitIso X).hom)

Premises used: _private.0.CondensedSet.instIsIsoFunctorCompactlyGeneratedCounitCompactlyGeneratedAdjunction._proof_1
-- Module: Mathlib.Condensed.TopCatAdjunction
Goal:
X_1 : CondensedSet
X : CompactlyGenerated
⊢ IsIso (compactlyGeneratedAdjunction.counit.app X)

Tactic:
exact inferInstanceAs (IsIso (compactlyGeneratedAdjunctionCounitIso X).hom)
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
hP :
  ∀ (X_1 B : C) (π : X_1 ⟶ B) [EffectiveEpi π] [inst_4 : HasPullback π π],
    Function.Bijective (α := (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) (β :=
      (fun (X : Type (max w w')) ↦ X)
        (↑{x : (yonedaPresheaf G X).obj (op X_1) |
              Eq (α := (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.fst π π))) :
                      (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op X_1))) →
                        (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                    x :
                  (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                        ((yonedaPresheaf G X).map (Quiver.Hom.op (pullback.snd π π))) :
                      (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op X_1))) →
                        (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                    x :
                  (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))} :
          Type (max w w')))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (mapToEqualizer (yonedaPresheaf G X) π (pullback.fst π π) (pullback.snd π π) ⋯)) :
        (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))) →
          (fun (X : Type (max w w')) ↦ X)
            (↑{x : (yonedaPresheaf G X).obj (op X_1) |
                  (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.fst π π).op) :
                        (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op X_1))) →
                          (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                      x =
                    (ConcreteCategory.hom ((yonedaPresheaf G X).map (pullback.snd π π).op) :
                        (a : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op X_1))) →
                          (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op (pullback π π))))
                      x} :
              Type (max w w')))
⊢ EqualizerCondition (yonedaPresheaf G X)

Tactic:
apply EqualizerCondition.mk

Premises used: CategoryTheory.regularTopology.EqualizerCondition.mk
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
hP : a = b
⊢ a = b

Tactic:
simp only [yonedaPresheaf, unop_op]

Premises used: Opposite.unop_op, ContinuousMap.yonedaPresheaf
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
hP :
  ∀ (x : (↑(G.obj (unop (op B))) : Type w)),
    Eq.{w' + 1} (α := X) ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
      ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
⊢ a = b

Tactic:
ext x
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
x : (↑(G.obj (unop (op B))) : Type w)
hP :
  ∀ (y : (↑(G.obj Z) : Type w))
    (hy :
      (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
              (G.map π) :
            (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
          y =
        x),
    Eq.{w' + 1} (α := X) ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
      ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
⊢ Eq.{w' + 1} (α := X) ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)

Tactic:
obtain ⟨y, hy⟩ := (hq Z B π).surjective x

Premises used: Topology.IsQuotientMap.surjective
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
x : (↑(G.obj (unop (op B))) : Type w)
y : (↑(G.obj Z) : Type w)
hy :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
          (G.map π) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
      y =
    x
hP :
  Eq.{w' + 1} (α := X)
    ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)
⊢ Eq.{w' + 1} (α := X) ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)

Tactic:
rw [← hy]
-- Module: Mathlib.Condensed.TopComparison
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X : Type w'
inst_1 : TopologicalSpace X
inst_2 : ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) G
hq :
  ∀ (Z B : C) (π : Z ⟶ B) [EffectiveEpi π],
    IsQuotientMap (X := (↑(G.obj Z) : Type w)) (Y := (↑(G.obj B) : Type w))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
            (G.map π)) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
Z B : C
π : Z ⟶ B
inst_3 : EffectiveEpi π
inst_4 : HasPullback π π
a b : (fun (X : Type (max w w')) ↦ X) ((yonedaPresheaf G X).obj (op B))
h :
  Eq (α := (↑(G.obj Z) : Type w) → X)
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑a : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
    (Function.comp (β := (↑(G.obj B) : Type w)) (⇑b : (a : (↑(G.obj B) : Type w)) → X)
      (⇑(TopCat.Hom.hom (G.map π)) : (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w)))
x : (↑(G.obj (unop (op B))) : Type w)
y : (↑(G.obj Z) : Type w)
hy :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
          (G.map π) :
        (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
      y =
    x
⊢ Eq.{w' + 1} (α := X)
    ((a : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{w}) ↦ C((↑X : Type w), (↑Y : Type w))) (CC := TopCat.carrier)
                (G.map π) :
              (a : (↑(G.obj Z) : Type w)) → (↑(G.obj B) : Type w))
            y :
          (↑(G.obj B) : Type w)) :
      X)

Tactic:
congr_fun h y

Premises used: congr_fun