Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
b :
  Fiber
    ⇑(comap (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
        f)
⊢ (ConcreteCategory.hom
        (g.hom.app
          (op
            (fiber
              (comap
                (TopCat.Hom.hom
                  (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                f)
              b))))
      ((ConcreteCategory.hom
          (X.obj.map
            (isTerminalPUnit.from
                (fiber
                  (comap
                    (TopCat.Hom.hom
                      (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                    f)
                  b)).op))
        (f (preimage (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))) ∘ ⇑f) a))) =
    (ConcreteCategory.hom
        (g.hom.app
          (op
            (fiber
              (comap
                (TopCat.Hom.hom
                  (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                f)
              b))))
      ((ConcreteCategory.hom
          (X.obj.map
            (ofHom P (sigmaInclIncl (⇑f) (ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 a b)).op))
        (counitAppAppImage f
          (Fiber.mk ⇑f
            ↑(preimage
                (⇑f ∘
                  ⇑(TopologicalSpace.Fiber.sigmaIncl
                      ((ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 ∘ ⇑f) a))
                b))))

Tactic:
simp only [counitAppAppImage, ← Functor.map_comp_apply, ← op_comp]

Goal state after:
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S✝ : CompHausLike P
Y✝ : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝³ : HasProp P PUnit.{u + 1}
f✝ : LocallyConstant (↑S✝.toTop) (Y✝.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g✝ : T ⟶ S✝
X✝ : TopCat
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))
g : X ⟶ Y
this : Preregular (CompHausLike P)
S : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑(unop S).toTop) (X.obj.obj (op (of P PUnit.{u + 1})))
a : Fiber ⇑(map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f)
b :
  Fiber
    ⇑(comap (TopCat.Hom.hom (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
        f)
⊢ (ConcreteCategory.hom
        (g.hom.app
          (op
            (fiber
              (comap
                (TopCat.Hom.hom
                  (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                f)
              b))))
      ((ConcreteCategory.hom
          (X.obj.map
            (isTerminalPUnit.from
                (fiber
                  (comap
                    (TopCat.Hom.hom
                      (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                    f)
                  b)).op))
        (f (preimage (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))) ∘ ⇑f) a))) =
    (ConcreteCategory.hom
        (g.hom.app
          (op
            (fiber
              (comap
                (TopCat.Hom.hom
                  (sigmaIncl (map (⇑(ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1}))))) f) a).hom)
                f)
              b))))
      ((ConcreteCategory.hom
          (X.obj.map
            (ofHom P (sigmaInclIncl (⇑f) (ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 a b) ≫
                isTerminalPUnit.from
                  (fiber f
                    (Fiber.mk ⇑f
                      ↑(preimage
                          (⇑f ∘
                            ⇑(TopologicalSpace.Fiber.sigmaIncl
                                ((ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 ∘ ⇑f) a))
                          b)))).op))
        (Fiber.image (⇑f)
          (Fiber.mk ⇑f
            ↑(preimage
                (⇑f ∘
                  ⇑(TopologicalSpace.Fiber.sigmaIncl
                      ((ConcreteCategory.hom (g.hom.app (op (of P PUnit.{u + 1})))).1 ∘ ⇑f) a))
                b))))