-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
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 (α := (fun (X : Type (max u w)) ↦ X) (Y.obj (op (fiber.{u, w} (P := P) f a))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y :=
                (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 (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))
                (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})))) ↦
                  (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))
                (↾fun
                    (g :
                      (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 (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))) ↦
                  g a)) :
            TypeCat.Fun (Y.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              (Y.obj (op (fiber.{u, w} (P := P) f a)))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (Y.obj (op (finiteCoproduct (fiber f))))) →
            (fun (X : Type (max u w)) ↦ X) (Y.obj (op (fiber f a))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op (Iso.hom (sigmaIso (P := P) f)))) :
              TypeCat.Fun (Y.obj (op S)) (Y.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))) :
            (a : (fun (X : Type (max u w)) ↦ X) (Y.obj (op S))) →
              (fun (X : Type (max u w)) ↦ X) (Y.obj (op (finiteCoproduct (fiber f)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (counitAppApp.{u, w} (P := P) S Y) :
              (a :
                  (fun (X : Type (max u w)) ↦ X)
                    (LocallyConstant (↑S.toTop : Type u) (Y.obj (op (of P PUnit.{u + 1}))))) →
                (fun (X : Type (max u w)) ↦ X) (Y.obj (op S)))
            f)) :
      (fun (X : Type (max u w)) ↦ X) (Y.obj (op (fiber.{u, w} (P := P) f a))))
    (counitAppAppImage (P := P) f a : Y.obj (op (fiber.{u, w} (P := P) f a)))
have simp : 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: simp only [counitAppApp, Functor.mapIso_inv, ← Iso.op_hom, CategoryTheory.comp_apply,
    ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← Functor.map_comp_apply, Iso.inv_hom_id,
    Functor.map_id_apply]