awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ Eq (α :=
    (CostructuredArrow.proj toLightProfinite.op S ⋙
            toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))).obj
        { left := Y, right := right, hom := g : Comma toLightProfinite.op (fromPUnit S) } ⟶
      X.obj S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      ((lanPresheafExt (isoFinYoneda X ≪≫ (locallyConstantIsoFinYoneda X).symm)).inv ≫ (lanPresheafNatIso hX).hom).app
        S)
    (colimit.ι
        (CostructuredArrow.proj toLightProfinite.op S ⋙
          toLightProfinite.op ⋙ locallyConstantPresheaf (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
        { left := Y, right := right, hom := g } ≫
      NatTrans.app
        (Iso.hom
            (lanPresheafNatIso fun (x : LightProfinite.{u}) ↦
              isColimitLocallyConstantPresheafDiagram (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) x) ≫
          counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        S)
have w : (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
      (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
    Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g =
  (locallyConstantPresheaf
          (X.obj
            (Opposite.op
              (CompHausLike.of
                (fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                PUnit.{u + 1})))).map
      g ≫
    counitAppApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (Opposite.unop S) X
Tactic: suffices _ ≫ (isoFinYonedaComponents _ _).inv ≫ X.map g =
    (locallyConstantPresheaf _).map g ≫ counitAppApp (Opposite.unop S) X by
      simpa [locallyConstantIsoFinYoneda, isoFinYoneda, counitApp]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ (↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g =
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).map
        g ≫
      counitAppApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) (Opposite.unop S) X
have w : Eq (α :=
  (locallyConstantPresheaf
          (X.obj
            (Opposite.op
              (CompHausLike.of
                (fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                PUnit.{u + 1})))).obj
      (toLightProfinite.op.obj Y) ⟶
    X.obj (obj (fromPUnit S) right))
  ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
      (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
    Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g)
  (NatTrans.app
      (counitApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
      (toLightProfinite.op.obj Y) ≫
    X.map g)
Tactic: erw [(counitApp.{u, u} X).naturality]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ Eq (α :=
    (locallyConstantPresheaf
            (X.obj
              (Opposite.op
                (CompHausLike.of
                  (fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
                  PUnit.{u + 1})))).obj
        (toLightProfinite.op.obj Y) ⟶
      X.obj (obj (fromPUnit S) right))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))) ≫ X.map g)
    (NatTrans.app
        (counitApp (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        (toLightProfinite.op.obj Y) ≫
      X.map g)
have w : Eq (α :=
  LocallyConstant
      (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)
      (X.obj
        (Opposite.op
          (CompHausLike.of
            (fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
            PUnit.{u + 1}))) ⟶
    X.obj (obj (fromPUnit S) right))
  (((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y)))) ≫
    X.map g)
  (NatTrans.app
      (counitApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
      (Opposite.op (toLightProfinite.obj (Opposite.unop Y))) ≫
    X.map g)
Tactic: simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ Eq (α :=
    LocallyConstant
        (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of
              (fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              PUnit.{u + 1}))) ⟶
      X.obj (obj (fromPUnit S) right))
    (((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
          (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
        Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y)))) ≫
      X.map g)
    (NatTrans.app
        (counitApp (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
        (Opposite.op (toLightProfinite.obj (Opposite.unop Y))) ≫
      X.map g)
have w : Eq (α :=
  LocallyConstant
      (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)
      (X.obj
        (Opposite.op
          (CompHausLike.of
            (fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
            PUnit.{u + 1}))) ⟶
    X.obj (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))
  ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
      (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
    Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))))
  (NatTrans.app
    (counitApp (P := fun (X : TopCat.{u}) ↦
      TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
    (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))
Tactic: congr
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : LightProfiniteᵒᵖ ⥤ Type u
inst : PreservesFiniteProducts X
hX : (S : LightProfinite.{u}) → IsColimit (X.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toLightProfinite.op.obj Y ⟶ obj (fromPUnit S) right
⊢ Eq (α :=
    LocallyConstant
        (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)
        (X.obj
          (Opposite.op
            (CompHausLike.of
              (fun (X : TopCat.{u}) ↦
                TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
              PUnit.{u + 1}))) ⟶
      X.obj (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))
    ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
        (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
      Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y))))
    (NatTrans.app
      (counitApp (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
      (Opposite.op (toLightProfinite.obj (Opposite.unop Y))))
have w : ∀
  (f :
    LocallyConstant
      (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)
      (X.obj
        (Opposite.op
          (CompHausLike.of
            (fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
            PUnit.{u + 1})))),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : LocallyConstant (Opposite.unop Y).obj (X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ↦
            (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (LightProfinite.of PUnit.{u + 1})))) ≫
          Iso.inv (isoFinYonedaComponents X (toLightProfinite.obj (Opposite.unop Y)))))
      f =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (counitApp (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) X)
          (Opposite.op (toLightProfinite.obj (Opposite.unop Y)))))
      f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_2 : PreservesFiniteProducts X
x y : X.obj (op S)
inst_3 : HasExplicitFiniteCoproducts P
h :
  ∀
    (a :
      Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
        (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))),
    Eq (α := (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) f a))) :
            (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
              (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
          x :
        (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) f a))) :
            (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
              (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
          y :
        (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
⊢ x = y
have a : Eq (α := (fun (X : Type (max u w)) ↦ X) (X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f)))))
  (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) f)))) :
          TypeCat.Fun (X.obj (op S)) (X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))) :
        (a : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
          (fun (X : Type (max u w)) ↦ X) (X.obj (op (finiteCoproduct (fiber f)))))
      x :
    (fun (X : Type (max u w)) ↦ X) (X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f)))))
  (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) f)))) :
          TypeCat.Fun (X.obj (op S)) (X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))) :
        (a : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
          (fun (X : Type (max u w)) ↦ X) (X.obj (op (finiteCoproduct (fiber f)))))
      y :
    (fun (X : Type (max u w)) ↦ X) (X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f)))))
Tactic: apply injective_of_mono (X.mapIso (sigmaIso f).op).hom
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)
⊢ Membership.mem (α := (↑(S.toTop (P := P)) : Type u)) (γ := Set (↑(S.toTop (P := P)) : Type u))
    ((↑(Fiber.mk (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
            ((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)) g :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
              (preimage
                (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a))) :
        Set (↑(S.toTop (P := P)) : Type u)) :
      Set (↑(S.toTop (P := P)) : Type u))
    ((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)) g :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
        (↑x : (↑T.toTop : Type u)) :
      (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) S)
have simp : Eq (α := Y.obj (op (of P PUnit.{u + 1})))
  ((f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      ((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)) g :
          (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
        (↑x : (↑T.toTop : Type u))) :
    Y.obj (op (of P PUnit.{u + 1})))
  ((f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      ((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)) g :
          (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
        (preimage (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          a)) :
    Y.obj (op (of P PUnit.{u + 1})))
Tactic: simp only [Fiber.mk, Set.mem_preimage, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)
⊢ Eq (α := Y.obj (op (of P PUnit.{u + 1})))
    ((f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
        ((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)) g :
            (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
          (↑x : (↑T.toTop : Type u))) :
      Y.obj (op (of P PUnit.{u + 1})))
    ((f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
        ((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)) g :
            (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
          (preimage (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
            a)) :
      Y.obj (op (of P PUnit.{u + 1})))
have h : (f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
    ((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)) g :
        (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
      (preimage (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a)) =
  Fiber.image (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a
Tactic: convert! map_eq_image _ _ x
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S_1.toTop (P := P)) : Type u) (Y_1.obj (op (of P PUnit.{u + 1})))
T_1 : CompHausLike P
g_1 : T_1 ⟶ S_1
inst_2 : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_3 : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
⊢ Eq (α :=
    Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S ⟶ Y.obj T)
    (CategoryTheory.Functor.map (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1}))))
        g ≫
      match (motive :=
        (x : (CompHausLike P)ᵒᵖ) →
          Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶ Y.obj x)
        T with
      | op S => counitAppApp.{u, w} (P := P) S Y)
    ((match (motive :=
        (x : (CompHausLike P)ᵒᵖ) →
          Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶ Y.obj x)
        S with
      | op S => counitAppApp.{u, w} (P := P) S Y) ≫
      Y.map g)
have h : ∀ (f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S),
  Eq (α := Y.obj T)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map
            (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) g ≫
          match (motive :=
            (x : (CompHausLike P)ᵒᵖ) →
              Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶
                Y.obj x)
            T with
          | op S => counitAppApp.{u, w} (P := P) S Y))
      f)
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((match (motive :=
            (x : (CompHausLike P)ᵒᵖ) →
              Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶
                Y.obj x)
            S with
          | op S => counitAppApp.{u, w} (P := P) S Y) ≫
          Y.map g))
      f)
Tactic: ext f
-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (Functor.obj (functorToPresheaves.{u, w} (P := P)) X)
have rw : Presheaf.IsSheaf (coherentTopology (CompHausLike P))
  (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
    (TopCat.toSheafCompHausLike.{w, u} P (TopCat.discrete.obj X) hs :
      have this := sorry;
      Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
Tactic: rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIso P hs X)]