-- 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)
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))
⊢ ∀ (S : Profinite),
    Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj M).val).mapCocone S.asLimitCone.op))

Tactic:
intro S

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))
S : Profinite
⊢ Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ ((Condensed.forget R).obj 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)
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
tfae_1_to_7 :
  Condensed.IsDiscrete M →
    ∀ (S : Profinite), Nonempty (IsColimit ((profiniteToCompHaus.op ⋙ M.val).mapCocone S.asLimitCone.op))
⊢ [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_finish

Result:
no goals

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