awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
⊢ IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
    (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)

Tactic:
2

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
inst : Ring R
M : LightCondMod R
⊢ LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)

Tactic:
1 ↔ 2

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
inst : Ring R
M : LightCondMod R
⊢ LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)

Tactic:
tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _

Premises used: CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
⊢ essImage (LightCondensed.discrete (ModuleCat R)) M

Tactic:
3

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
⊢ LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M

Tactic:
1 ↔ 3

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
⊢ LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M

Tactic:
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
⊢ LightCondensed.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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
⊢ essImage (functor R) M

Tactic:
4

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
⊢ LightCondensed.IsDiscrete M ↔ essImage (functor R) M

Tactic:
1 ↔ 4

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
⊢ LightCondensed.IsDiscrete M ↔ essImage (functor R) M

Tactic:
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _
    LightProfinite.isTerminalPUnit (adjunction R) _

Premises used: CategoryTheory.Sheaf.isConstant_iff_mem_essImage, LightProfinite.isTerminalPUnit, LightCondMod.LocallyConstant.adjunction
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
⊢ LightCondensed.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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
⊢ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)

Tactic:
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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
⊢ LightCondensed.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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
⊢ LightCondensed.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' _ LightProfinite.isTerminalPUnit (adjunction R) _

Premises used: inferInstance, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', LightProfinite.isTerminalPUnit, LightCondMod.LocallyConstant.adjunction, LightProfinite, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ LightCondensed.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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M

Tactic:
6 → 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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
h :
  ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
rw :
  ∀ (S : LightProfinite.{u}),
    Nonempty.{u + 2}
      (IsColimit
        ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
          (coconeRightOpOfCone S.asLimitCone)))
⊢ LightCondensed.IsDiscrete M

Tactic:
rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]

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

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
h :
  ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : PreservesFilteredColimitsOfSize.{0, 0, u, u, u + 1, u + 1}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty.{u + 2}
    (IsColimit
      ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
        (coconeRightOpOfCone S.asLimitCone)))

Tactic:
exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
⊢ ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M

Tactic:
tfae_have 6 → 1 := by
    intro h
    rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]
    intro S
    letI : PreservesFilteredColimitsOfSize.{0, 0} (forget (ModuleCat R)) :=
      preservesFilteredColimitsOfSize_shrink.{0, u, 0, u} _
    exact ⟨isColimitOfPreserves (forget (ModuleCat R)) (h S).some⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
⊢ LightCondensed.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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
⊢ ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
⊢ ∀ (a : LightCondensed.IsDiscrete M) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

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
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
h : LightCondensed.IsDiscrete M
S : LightProfinite
rw :
  ∀
    (h :
      ∀ (S : LightProfinite.{u}),
        Nonempty.{u + 2}
          (IsColimit
            ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone))))
    (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ Nonempty
    (IsColimit
      (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

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

Premises used: List.TFAE.out, LightCondSet.isDiscrete_tfae, OfNat.ofNat, LightCondMod.isDiscrete_iff_isDiscrete_forget
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
tfae_1_iff_2 :
  LightCondensed.IsDiscrete M ↔
    IsIso (X := obj (LightCondensed.underlying (ModuleCat R) ⋙ LightCondensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (ModuleCat R))) M)
tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
tfae_1_iff_5 : LightCondensed.IsDiscrete M ↔ IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) M)
tfae_6_to_1 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    LightCondensed.IsDiscrete M
h :
  ∀ (S : LightProfinite.{u}),
    Nonempty.{u + 2}
      (IsColimit
        ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
          (coconeRightOpOfCone S.asLimitCone)))
S : LightProfinite
this : ReflectsFilteredColimitsOfSize.{0, 0, u, u, u + 1, u + 1}
  (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC :=
    ModuleCat.carrier)) :=
  ⋯
⊢ Nonempty
    (IsColimit
      (M.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

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

Premises used: ModuleCat, Nonempty.some, Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects, CategoryTheory.forget