awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)
⊢ Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op (of PUnit.{u + 1}))) :
        (a : X.obj.obj (Opposite.op (of PUnit.{u + 1}))) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
              (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
          (a : X.obj.obj (Opposite.op S)) → X.obj.obj (Opposite.op (of PUnit.{u + 1})))
        x)
have hf : Continuous (Y := Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
  fun (a : (↑(S.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) ↦
  (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
          (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) a).op) :
      (a : Y.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op (of PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (Opposite.op S)) :
        (a : X.obj.obj (Opposite.op S)) → Y.obj.obj (Opposite.op S))
      x)
Tactic: rw [show (fun (a : S) ↦
          f.hom.app ⟨of PUnit⟩ (X.obj.map ((of PUnit.{u + 1}).const a).op x)) = _
        from funext fun a ↦ NatTrans.naturality_apply f.hom ((of PUnit.{u + 1}).const a).op x]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 : CondensedSet
X : TopCat
⊢ Continuous (Y := (↑X : Type (u + 1)))
    fun
      (x :
        X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1}))) ↦
    x.toFun PUnit.unit
have rw : Continuous.{u + 1, u + 1} (X :=
  (i :
    (S : CompHaus.{u}) × X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)) ×
    (↑(i.fst (β := fun (S : CompHaus.{u}) ↦
              X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op S)).toTop
          (P := fun (x : TopCat.{u}) ↦ True)) :
      Type u))
  (Y := (↑X : Type (u + 1)))
  ((fun
        (x :
          X.toCondensedSet.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (Opposite.op (of PUnit.{u + 1}))) ↦
      x.toFun PUnit.unit) ∘
    X.toCondensedSet.coinducingCoprod)
Tactic: rw [continuous_coinduced_dom]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 X : CondensedSet
S : CompHausᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
⊢ Continuous (Y := (↑X.toTopCat : Type (u + 1)))
    fun (s : (↑(Functor.obj (CompHausLike.compHausLikeToTop fun (x : TopCat.{u}) ↦ True) (Opposite.unop S)) : Type u)) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (CompHausLike.const (P := fun (x : TopCat.{u}) ↦ True) (of PUnit.{u + 1}) s).op) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (Opposite.unop S)))) →
          (fun (X : Type (u + 1)) ↦ X) (X.obj.obj (Opposite.op (of PUnit.{u + 1}))))
      x
have suffices : ∀ (i : (T : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)),
  Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
    fun
      (a :
        (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                  X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)).toTop
              (P := fun (x : TopCat.{u}) ↦ True)) :
          Type u)) ↦
    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: suffices ∀ (i : (T : CompHaus.{u}) × X.obj.obj ⟨T⟩),
          Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 X : CondensedSet
S : CompHausᵒᵖ
x : X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj S
⊢ ∀ (i : (T : CompHaus.{u}) × X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)),
    Continuous (Y := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op (of PUnit.{u + 1})))
      fun
        (a :
          (↑(i.fst (β := fun (T : CompHaus.{u}) ↦
                    X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (Opposite.op T)).toTop
                (P := fun (x : TopCat.{u}) ↦ True)) :
            Type u)) ↦
      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)
have rw : Continuous X.coinducingCoprod
Tactic: rw [← continuous_sigma_iff]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X Y : CondensedSet
⊢ Eq (α := condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)
    (CategoryStruct.comp (Y := condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
        (condensedSetToTopCat.map
          (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
        (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
          (condensedSetToTopCat.obj Y)) :
      condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)
    (𝟙 (condensedSetToTopCat.obj Y) : condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y)
have w : ∀ (x : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))),
  Eq (α := (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
              TopCat.carrier) (X := condensedSetToTopCat.obj Y) (Y := condensedSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
                  (condensedSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (condensedSetToTopCat.obj Y)) :
                condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y) :
            C((↑(condensedSetToTopCat.obj Y) : Type (u + 1)), (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
            TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X Y : CondensedSet
x : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))
⊢ Eq (α := (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
              TopCat.carrier) (X := condensedSetToTopCat.obj Y) (Y := condensedSetToTopCat.obj Y)
              (CategoryStruct.comp (Y :=
                  condensedSetToTopCat.obj (topCatToCondensedSet.obj (condensedSetToTopCat.obj Y)))
                  (condensedSetToTopCat.map
                    (NatTrans.app { app := topCatAdjunctionUnit, naturality := topCatAdjunction._proof_2 } Y))
                  (NatTrans.app { app := topCatAdjunctionCounit, naturality := topCatAdjunction._proof_3 }
                    (condensedSetToTopCat.obj Y)) :
                condensedSetToTopCat.obj Y ⟶ condensedSetToTopCat.obj Y) :
            C((↑(condensedSetToTopCat.obj Y) : Type (u + 1)), (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
            TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
          (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
        x :
      (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
have w : Eq (α :=
  (fun (X : Type (u + 1)) ↦ X)
    (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
      (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map
            (𝟙 (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) :
        (a : (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1})))))) →
          (fun (X : Type (u + 1)) ↦ X) (Y.obj.obj (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
      x :
    (fun (X : Type (u + 1)) ↦ X)
      (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (Opposite.op (Opposite.unop (Opposite.op (of PUnit.{u + 1}))))))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u + 1}) ↦ C((↑X : Type (u + 1)), (↑Y : Type (u + 1)))) (CC :=
          TopCat.carrier) (𝟙 (condensedSetToTopCat.obj Y)) :
        (a : (↑(condensedSetToTopCat.obj Y) : Type (u + 1))) → (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
      x :
    (↑(condensedSetToTopCat.obj Y) : Type (u + 1)))
Tactic: change Y.obj.map (𝟙 _) _ = _
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 : CondensedSet
X : TopCat
⊢ Epi (topCatAdjunction.counit.app X)
have rw : 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: rw [TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 X : CondensedSet
⊢ UCompactlyGeneratedSpace.{u, u + 1} (↑X.toTopCat : Type (u + 1))
have 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
Tactic: apply uCompactlyGeneratedSpace_of_continuous_maps
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
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))))
⊢ Continuous f
have 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)
Tactic: rw [continuous_coinduced_dom, continuous_sigma_iff]
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X_1 : CondensedSet
X : TopCat
inst : UCompactlyGeneratedSpace.{u, u + 1} (↑X : Type (u + 1))
⊢ Continuous (topCatAdjunctionCounitEquiv X).invFun
have 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))))
Tactic: apply continuous_from_uCompactlyGeneratedSpace
-- Lean 4 proof step from Mathlib.Condensed.TopCatAdjunction (goal)
Goal:
X : CondensedSet
⊢ IsIso compactlyGeneratedAdjunction.counit
have rw : ∀ (X : CompactlyGenerated.{u_1, u_1 + 1}), IsIso (compactlyGeneratedAdjunction.counit.app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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))
⊢ EqualizerCondition (yonedaPresheaf G X)
have 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 π π) sorry)) :
      (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')))
Tactic: apply EqualizerCondition.mk
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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)))
⊢ a = b
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨y, hy⟩ := (hq Z B π).surjective x
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (goal)
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) x : X)
    ((b : (a : (↑(G.obj (unop (op B))) : Type w)) → X) x : X)
have 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)
Tactic: rw [← hy]
-- Lean 4 proof step from Mathlib.Condensed.TopComparison (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
G : CategoryTheory.Functor.{v, w, u, w + 1} C TopCat
X_1 : Type w'
inst_1 : TopologicalSpace X_1
P : TopCat.{u} → Prop
X : TopCat
inst_2 : CompHausLike.HasExplicitFiniteCoproducts P
inst_3 : CompHausLike.HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (yonedaPresheaf (CompHausLike.compHausLikeToTop P) (↑X : Type (max u w)))
have this : Preregular.{u, u + 1} (CompHausLike P)
Tactic: have := CompHausLike.preregular hs