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

Proof state:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
⊢ Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))

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

Result:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : ReflectsFilteredColimitsOfSize.{0, 0, u, u + 1, u + 1} (forget (ModuleCat R)) :=
  reflectsFilteredColimitsOfSize_shrink (forget (ModuleCat R))
⊢ Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Proof state:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
⊢ (∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M

Tactic:
intro h

Result:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ LightCondensed.IsDiscrete M

Proof state:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ ∀ (S : LightProfinite),
    Nonempty (IsColimit (((LightCondensed.forget R).obj M).val.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
intro S

Result:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
h : ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
⊢ Nonempty (IsColimit (((LightCondensed.forget R).obj M).val.mapCocone (coconeRightOpOfCone S.asLimitCone)))

Proof state:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 1 → 6 := by
  intro h S
  rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5:)] at h
  letI : ReflectsFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
    reflectsFilteredColimitsOfSize_shrink.{0, u, 0, u} _
  exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩

Result:
R : Type u
inst✝ : Ring R
M : LightCondMod R
tfae_1_iff_2 : LightCondensed.IsDiscrete M ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ (LightCondensed.discrete (ModuleCat R)).essImage M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ (functor R).essImage M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso ((LocallyConstant.adjunction R).counit.app M)
tfae_6_to_1 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    LightCondensed.IsDiscrete M
tfae_1_to_6 :
  LightCondensed.IsDiscrete M →
    ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [LightCondensed.IsDiscrete M, IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (functor R).essImage M,
      IsIso ((LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite), Nonempty (IsColimit (M.val.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE