-- 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
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

Tactic:
have := CompHausLike.preregular hs

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
this : Preregular (CompHausLike P)
⊢ counitAppApp S ((functor P hs).obj X).val ((functorToPresheaves.map ((unit P hs).app X)).app (op S) f) = 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:
intro a

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.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

Tactic:
erw [← map_eq_image _ a 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))) ((map ((unit P hs).app X) f) ↑x))
      x =
    (comap (TopCat.Hom.hom (sigmaIncl (map ((unit P hs).app X) f) a)) f) x

Proof state:
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)
⊢ functorToPresheaves.map ((unit P hs).app X) ≫ ((counit P hs).app ((functor P hs).obj X)).val =
    𝟙 (functorToPresheaves.obj X)

Tactic:
ext ⟨S⟩ (f : LocallyConstant _ X)

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
⊢ (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

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)
⊢ 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

Tactic:
simp only [functor_obj_val, functorToPresheaves_obj_obj, coe_of, Functor.id_obj,
  counitAppAppImage, LocallyConstant.map_apply, functorToPresheaves_obj_map, Quiver.Hom.unop_op]

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)
⊢ 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