-- 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_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f_1 : 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
f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S
a :
  Fiber (Y := (↑((unop T).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
h :
  Eq (α := Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
    (counitAppAppImage (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (componentHom (P := P) f g.unop a))) :
        (a_1 :
            Y.obj
              (op
                (fiber f
                  (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                    ((ConcreteCategory.hom g.unop :
                        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop T)) →
                          (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop S))
                      (preimage
                        (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                          (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                        a)))))) →
          Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)))
      (counitAppAppImage (P := P) f
        (Fiber.mk (⇑f : (a : (↑(unop 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.unop :
              (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop T)) →
                (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop S))
            (preimage
              (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
              a)))))
⊢ Eq (α := Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.map (Quiver.Hom.op (sigmaIncl (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a))) :
          (a_1 : Y.obj T) → Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (counitAppApp.{u, w} (P := P) (unop T) Y) :
            (a : LocallyConstant (↑(unop T).toTop : Type u) (Y.obj (op (of P PUnit.{u + 1})))) → Y.obj T)
          (comap (TopCat.Hom.hom g.unop.hom) f)) :
      Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.map (Quiver.Hom.op (sigmaIncl (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a))) :
          (a_1 : Y.obj T) → Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map g) : (a : Y.obj S) → Y.obj T)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (counitAppApp.{u, w} (P := P) (unop S) Y) :
              (a : LocallyConstant (↑(unop S).toTop : Type u) (Y.obj (op (of P PUnit.{u + 1})))) → Y.obj S)
            f)) :
      Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))

Tactic:
rw [incl_of_counitAppApp, ← Functor.map_comp_apply, incl_comap,
      Functor.map_comp_apply, incl_of_counitAppApp]

Premises used: CompHausLike.LocallyConstant.incl_of_counitAppApp, CategoryTheory.Functor.map_comp_apply, CompHausLike.LocallyConstant.incl_comap