awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Colimit
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
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)
⊢ 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:
simp only [← Category.assoc, op_obj, functorToPresheaves_obj_obj]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.op_obj, CompHausLike.LocallyConstant.functorToPresheaves_obj_obj
-- Module: Mathlib.Condensed.Discrete.Colimit
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
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))))
⊢ 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:
congr
-- Module: Mathlib.Condensed.Discrete.Colimit
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
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
⊢ 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:
ext f
-- Module: Mathlib.Condensed.Discrete.Colimit
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
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})))
x :
  Function.Fiber (Y :=
    (↑((toLightProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u))
    (Z :=
    X.obj
      (Opposite.op
        (CompHausLike.of
          (fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
          PUnit.{u + 1})))
    (⇑f :
      (a : (↑(toLightProfinite.obj (Opposite.unop Y)).toTop : Type u)) →
        X.obj
          (Opposite.op
            (CompHausLike.of
              (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u))
              PUnit.{u + 1})))
⊢ Finite.{u + 1}
    (↑((fiber (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) f x).toTop
          (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)

Tactic:
have : Finite (fiber.{u, u} f x) :=
    Finite.of_injective (sigmaIncl.{u, u} f x).1 Subtype.val_injective
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑(Q.toTop (P := P)) : Type u) Z
a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)
inst_1 : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
x : X.obj (op Q)
⊢ Eq (α := X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (CategoryStruct.comp (Y :=
                  op
                    (of P
                      ((a : Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ×
                        (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
                  (Quiver.Hom.op (Iso.hom (sigmaIso (P := P) r)) :
                    op Q ⟶ op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) r)))
                  (Quiver.Hom.op
                      (ofHom P
                        {
                          toFun :=
                            Sigma.mk (β :=
                              fun
                                (a :
                                  Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z)
                                    (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ↦
                              (↑(↑a : Set (↑Q.toTop : Type u)) : Type u)) a,
                          continuous_toFun := ⋯ }) :
                    op
                        (of P
                          ((a :
                            Fiber (Y := (↑(Q.toTop (P := P)) : Type u)) (Z := Z) (⇑r : (a : (↑Q.toTop : Type u)) → Z)) ×
                            (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))) ⟶
                      op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
            TypeCat.Fun (X.obj (op Q)) (X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
          (a_1 : X.obj (op Q)) → X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
        x :
      X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) r a))) :
            TypeCat.Fun (X.obj (op Q)) (X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))) :
          (a_1 : X.obj (op Q)) → X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))
        x :
      X.obj (op (of P (↑(↑a : Set (↑Q.toTop : Type u)) : Type u))))

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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))))
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)))))
⊢ x = y

Tactic:
apply injective_of_mono (X.mapIso (sigmaIso f).op).hom

Premises used: CategoryTheory.Iso.op, CompHausLike.LocallyConstant.sigmaIso, CategoryTheory.injective_of_mono, CategoryTheory.Iso.hom, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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))))
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))))

Tactic:
specialize h a
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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)
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})))
⊢ 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)

Tactic:
simp only [Fiber.mk, Set.mem_preimage, Set.mem_singleton_iff]

Premises used: Function.Fiber.mk, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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)
⊢ (comap (TopCat.Hom.hom g.hom) f : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      (↑x : (↑T.toTop : Type u)) =
    Fiber.image (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a

Tactic:
map_eq_image _ _ x

Premises used: Function.Fiber.map_eq_image
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
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)
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
⊢ 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:
convert! map_eq_image _ _ x

Premises used: Function.Fiber.map_eq_image