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

Proof state:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
⊢ [Condensed.IsDiscrete M, IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.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:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
⊢ [Condensed.IsDiscrete M, IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      Sheaf.IsConstant (coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))].TFAE

Proof state:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
⊢ (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M

Tactic:
intro h

Result:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
h : ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))
⊢ Condensed.IsDiscrete M

Proof state:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).val).mapCocone S.asLimitCone.op))
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))

Tactic:
letI : ReflectsFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
  reflectsFilteredColimitsOfSize_shrink.{u, u+1, u, u+1} _

Result:
R : Type (u + 1)
inst✝ : Ring R
M : CondensedMod R
tfae_1_iff_2 : Condensed.IsDiscrete M ↔ IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ (Condensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M)
tfae_7_to_1 :
  (∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))) →
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).val).mapCocone S.asLimitCone.op))
S : Profinite
this : ReflectsFilteredColimitsOfSize.{u, u, u + 1, u + 2, u + 2} (forget (ModuleCat R)) :=
  reflectsFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))