-- 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)
      ((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})))) →
        X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (sigmaComparison.{u, w} (P := P) X
                fun
                  (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})))) ↦
                (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)) :
            TypeCat.Fun
              (X.obj
                (op
                  (of P
                    ((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})))) ×
                      (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))))
              ((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})))) →
                X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))) :
          (a :
              (fun (X : Type (max u w)) ↦ X)
                (X.obj
                  (op
                    (of P
                      ((a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) ×
                        (↑(fiber f a).toTop : Type u)))))) →
            (fun (X : Type (max u w)) ↦ X)
              ((a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                X.obj (op (of P (↑(fiber f a).toTop : Type u)))))
        (((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))))) :
      (fun (X : Type (max u w)) ↦ X)
        ((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})))) →
          X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (sigmaComparison.{u, w} (P := P) X
                fun
                  (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})))) ↦
                (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)) :
            TypeCat.Fun
              (X.obj
                (op
                  (of P
                    ((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})))) ×
                      (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))))
              ((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})))) →
                X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))) :
          (a :
              (fun (X : Type (max u w)) ↦ X)
                (X.obj
                  (op
                    (of P
                      ((a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) ×
                        (↑(fiber f a).toTop : Type u)))))) →
            (fun (X : Type (max u w)) ↦ X)
              ((a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                X.obj (op (of P (↑(fiber f a).toTop : Type u)))))
        (((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))))) :
      (fun (X : Type (max u w)) ↦ X)
        ((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})))) →
          X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))))
⊢ 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 (sigmaComparison X (fun a ↦ (fiber f a).1))

Premises used: CompHausLike.sigmaComparison, CompHausLike.LocallyConstant.fiber, TopCat.carrier, CompHausLike.toTop, CategoryTheory.injective_of_mono