-- Mathlib/Condensed/Discrete/Characterization.lean
theorem isDiscrete_tfae  (X : CondensedSet.{u}) :
    TFAE
    [ X.IsDiscrete
    , IsIso ((Condensed.discreteUnderlyingAdj _).counit.app X)
    , (Condensed.discrete _).essImage X
    , CondensedSet.LocallyConstant.functor.essImage X
    , IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X)
    , Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence _).inverse.obj X)
    , ∀ S : Profinite.{u}, Nonempty
        (IsColimit <| (profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
    ]

Proof state:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE

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

Result:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
tfae_7_to_4 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))) →
    LocallyConstant.functor.essImage X
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE

Proof state:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Result:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE

Proof state:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE

Tactic:
tfae_have 1 ↔ 6 :=
  (Sheaf.isConstant_iff_of_equivalence (coherentTopology Profinite)
    (coherentTopology CompHaus) profiniteToCompHaus Profinite.isTerminalPUnit
    CompHaus.isTerminalPUnit _).symm

Result:
X : CondensedSet
tfae_1_iff_2 : Condensed.IsDiscrete X ↔ IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ (discrete (Type (u + 1))).essImage X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X)
⊢ [Condensed.IsDiscrete X, IsIso ((discreteUnderlyingAdj (Type (u + 1))).counit.app X),
      (discrete (Type (u + 1))).essImage X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite) ((ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op))].TFAE