-- 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})))
inst_2 : PreservesFiniteProducts Y
inst_3 : HasExplicitFiniteCoproducts 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})))
⊢ Eq (α := Y.obj (op (fiber.{u, w} (P := P) f a)))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (sigmaComparison.{u, w} (P := P) Y
                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})))) ↦
                (↑(↑a : Set (↑S.toTop : Type u)) : Type u)) :
            TypeCat.Fun (Y.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              ((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})))) →
                Y.obj (op (of P (↑(↑a : Set (↑S.toTop : Type u)) : Type u))))) :
          (a : Y.obj (op (finiteCoproduct (fiber f)))) →
            (a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
              Y.obj (op (of P (↑(↑a : Set (↑S.toTop : Type u)) : Type u))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (inv
                    (sigmaComparison.{u, w} (P := P) Y
                      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})))) ↦
                      (↑(↑a : Set (↑S.toTop : Type u)) : Type u))) :
                TypeCat.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})))) →
                    Y.obj (op (of P (↑(↑a : Set (↑S.toTop : Type u)) : Type u))))
                  (Y.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})))) ×
                          (↑(↑a : Set (↑S.toTop : Type u)) : Type u)))))) :
              (a :
                  (a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                    Y.obj (op (of P (↑(↑a : Set (↑S.toTop : Type u)) : Type u)))) →
                Y.obj
                  (op
                    (of P
                      ((a : Fiber (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) ×
                        (↑(↑a : Set (↑S.toTop : Type u)) : Type u)))))
            (counitAppAppImage (P := P) f) :
          Y.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})))) ×
                  (↑(↑a : Set (↑S.toTop : Type u)) : Type u)))))
        a :
      Y.obj (op (of P (↑(↑a : Set (↑S.toTop : Type u)) : Type u))))
    (counitAppAppImage (P := P) f a : Y.obj (op (fiber.{u, w} (P := P) f a)))

Tactic:
congrFun (Iso.inv_hom_id_apply (asIso (sigmaComparison Y (fun a ↦ (fiber f a).1)))
    (counitAppAppImage f)) _

Premises used: Set.Mem, CompHausLike.sigmaComparison, CompHausLike.LocallyConstant.fiber, TopCat.carrier, congrFun, CompHausLike.toTop, CategoryTheory.Iso.inv_hom_id_apply, CategoryTheory.asIso