-- 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
h :
  ∀
    (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})))),
    Eq (α :=
      (fun (X : Type (max u w)) ↦ X) (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 : (fun (X : Type (max u w)) ↦ X) (Y.obj (op (unop T)))) →
            (fun (X : Type (max u w)) ↦ X) (Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a))))
        (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))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.map (Quiver.Hom.op (sigmaIncl (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (Y.obj (op (unop T)))) →
            (fun (X : Type (max u w)) ↦ X) (Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a))))
        (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))
⊢ 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:
apply presheaf_ext (f.comap g.unop.hom.hom)

Premises used: LocallyConstant.comap, Quiver.Hom.unop, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom, CompHausLike.LocallyConstant.presheaf_ext