awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
⊢ Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)

Tactic:
1 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
⊢ Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)

Tactic:
tfae_have 1 ↔ 5 :=
    have : (functor R).Faithful := inferInstance
    have : (functor R).Full := inferInstance
    -- These `have` statements above shouldn't be needed, but they are.
    Sheaf.isConstant_iff_isIso_counit_app' _ CompHaus.isTerminalPUnit (adjunction R) _

Premises used: inferInstance, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', CondensedMod.LocallyConstant.adjunction, CompHaus.isTerminalPUnit, CompHaus, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ Condensed.IsDiscrete M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ Sheaf.IsConstant (coherentTopology Profinite)
    (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)

Tactic:
1 ↔ 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)

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

Premises used: profiniteToCompHaus, Profinite, CategoryTheory.Sheaf.isConstant_iff_of_equivalence, Profinite.isTerminalPUnit, CompHaus.isTerminalPUnit, CompHaus, Iff.symm, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
⊢ ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
⊢ Condensed.IsDiscrete M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
⊢ ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M

Tactic:
7 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
h :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
rw :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙
              (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
⊢ Condensed.IsDiscrete M

Tactic:
rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)]

Premises used: CondensedMod.isDiscrete_iff_isDiscrete_forget, List.TFAE.out, CondensedSet.isDiscrete_tfae, OfNat.ofNat
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
h :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
S : Profinite
this : PreservesFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙
            (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
        S.asLimitCone.op))

Tactic:
⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩

Premises used: ModuleCat, Nonempty.some, Nonempty.intro, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
h :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
S : Profinite
this : PreservesFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙
            (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
        S.asLimitCone.op))

Tactic:
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
⊢ ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M

Tactic:
tfae_have 7 → 1 := by
    intro h
    rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)]
    intro S
    letI : PreservesFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
      preservesFilteredColimitsOfSize_shrink.{u, u + 1, u, u + 1} _
    exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
⊢ Condensed.IsDiscrete M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
⊢ ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
⊢ ∀ (a : Condensed.IsDiscrete M) (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))

Tactic:
1 → 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
h : Condensed.IsDiscrete M
S : Profinite
rw :
  ∀
    (h :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙
                  (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op)))
    (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op))

Tactic:
rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)] at h

Premises used: CondensedMod.isDiscrete_iff_isDiscrete_forget, List.TFAE.out, CondensedSet.isDiscrete_tfae, OfNat.ofNat
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙
              (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
S : Profinite
this : ReflectsFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op))

Tactic:
⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩

Premises used: ModuleCat, Nonempty.some, Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects, CategoryTheory.forget
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
tfae_1_iff_2 :
  Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : Condensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : Condensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_1_iff_6 :
  Condensed.IsDiscrete M ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (Condensed.ProfiniteCompHaus.equivalence (ModuleCat R))) M)
tfae_7_to_1 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    Condensed.IsDiscrete M
h :
  ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙
              (obj (Condensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
S : Profinite
this : ReflectsFilteredColimitsOfSize.{u, u, u + 1, u + 1, u + 2, u + 2}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op))

Tactic:
exact ⟨isColimitOfReflects (forget (ModuleCat R)) (h S).some⟩