-- Mathlib/Condensed/Discrete/Characterization.lean
theorem isDiscrete_tfae  (X : LightCondSet.{u}) :
    TFAE
    [ X.IsDiscrete
    , IsIso ((LightCondensed.discreteUnderlyingAdj _).counit.app X)
    , (LightCondensed.discrete _).essImage X
    , LightCondSet.LocallyConstant.functor.essImage X
    , IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X)
    , ∀ S : LightProfinite.{u}, Nonempty
        (IsColimit <| X.val.mapCocone (coconeRightOpOfCone S.asLimitCone))
    ]

Proof state:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 ↔ 5 :=
  have : functor.Faithful := inferInstance
  have : functor.Full := inferInstance
  Sheaf.isConstant_iff_isIso_counit_app' _ LightProfinite.isTerminalPUnit adjunction X

Result:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Proof state:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 6 → 4 := fun h ↦
  mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)

Result:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    functor.essImage X
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE