-- Mathlib/Condensed/Discrete/LocallyConstant.lean
lemma adjunction_left_triangle [HasExplicitFiniteCoproducts.{u} P]
    (X : Type max u w) : functorToPresheaves.{u, w}.map ((unit P hs).app X) ≫
      ((counit P hs).app ((functor P hs).obj X)).val = 𝟙 (functorToPresheaves.obj X)

Proof state:
case w.h.op.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map ((unit P hs).app X) f)
⊢ comap (TopCat.Hom.hom (isTerminalPUnit.from (fiber (map ((unit P hs).app X) f) a)))
      (Fiber.image ((unit P hs).app X ∘ ⇑f) a) =
    comap (TopCat.Hom.hom (sigmaIncl (map ((unit P hs).app X) f) a)) f

Tactic:
ext x

Result:
case w.h.op.h.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map ((unit P hs).app X) f)
x : ↑(fiber (map ((unit P hs).app X) f) a).toTop
⊢ (comap (TopCat.Hom.hom (isTerminalPUnit.from (fiber (map ((unit P hs).app X) f) a)))
        (Fiber.image ((unit P hs).app X ∘ ⇑f) a))
      x =
    (comap (TopCat.Hom.hom (sigmaIncl (map ((unit P hs).app X) f) a)) f) x

Proof state:
case w.h.op.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
⊢ (functorToPresheaves.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).val).app (op S) f =
    (𝟙 (functorToPresheaves.obj X)).app (op S) f

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, FunctorToTypes.comp, NatTrans.id_app,
  functorToPresheaves_obj_obj, types_id_apply]

Result:
case w.h.op.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
⊢ ((counit P hs).app ((functor P hs).obj X)).val.app (op S)
      ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f) =
    f

Proof state:
case w.h.op.h.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map ((unit P hs).app X) f)
x : ↑(fiber (map ((unit P hs).app X) f) a).toTop
⊢ (comap (TopCat.Hom.hom (isTerminalPUnit.from (fiber (map ((unit P hs).app X) f) a))) ((map ((unit P hs).app X) f) ↑x))
      x =
    (comap (TopCat.Hom.hom (sigmaIncl (map ((unit P hs).app X) f) a)) f) x

Tactic:
rfl

Result:
no goals

Proof state:
case w.h.op.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
⊢ counitAppApp S ((functor P hs).obj X).val ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f) = f

Tactic:
apply presheaf_ext
  (X := ((functor P hs).obj X).val) (Y := ((functor.{u, w} P hs).obj X).val)
    (f.map ((unit P hs).app X))

Result:
case w.h.op.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
⊢ ∀ (a : Fiber ⇑(map ((unit P hs).app X) f)),
    ((functor P hs).obj X).val.map (sigmaIncl (map ((unit P hs).app X) f) a).op
        (counitAppApp S ((functor P hs).obj X).val ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f)) =
      ((functor P hs).obj X).val.map (sigmaIncl (map ((unit P hs).app X) f) a).op f

Proof state:
case w.h.op.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map ((unit P hs).app X) f)
⊢ ((functor P hs).obj X).val.map (sigmaIncl (map ((unit P hs).app X) f) a).op
      (counitAppApp S ((functor P hs).obj X).val ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f)) =
    ((functor P hs).obj X).val.map (sigmaIncl (map ((unit P hs).app X) f) a).op f

Tactic:
erw [incl_of_counitAppApp]

Result:
case w.h.op.h.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
this : Preregular (CompHausLike P)
a : Fiber ⇑(map ((unit P hs).app X) f)
⊢ counitAppAppImage (map ((unit P hs).app X) f) a =
    ((functor P hs).obj X).val.map (sigmaIncl (map ((unit P hs).app X) f) a).op f

Proof state:
case w.h.op.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
⊢ ((counit P hs).app ((functor P hs).obj X)).val.app (op S)
      ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f) =
    f

Tactic:
simp only [counit, counitApp_app]

Result:
case w.h.op.h
P : TopCat → Prop
inst✝⁴ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
inst✝³ : HasProp P PUnit.{u + 1}
inst✝² : HasExplicitFiniteCoproducts P
inst✝¹ : HasExplicitPullbacks P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Surjective ⇑(ConcreteCategory.hom f)
inst✝ : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑S.toTop) X
⊢ counitAppApp S ((functor P hs).obj X).val ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f) = f