-- 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)
⊢ [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 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

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
⊢ [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)
tfae_6_to_4 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    functor.essImage X
tfae_4_to_6 :
  functor.essImage X →
    ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [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_finish

Result:
no goals

Proof state:
X : LightCondSet
⊢ [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 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _

Result:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).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
⊢ [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 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ 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
⊢ [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)
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

Tactic:
tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
  ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
    (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩

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
tfae_4_to_6 :
  functor.essImage X →
    ∀ (S : LightProfinite), Nonempty (IsColimit (X.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [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