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
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:
tfae_have 1 → 7 := by
    intro h S
    rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)] at h
    letI : ReflectsFilteredColimitsOfSize.{u, u} (forget (ModuleCat R)) :=
      reflectsFilteredColimitsOfSize_shrink.{u, u + 1, u, u + 1} _
    exact ⟨isColimitOfReflects (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
tfae_1_to_7 :
  ∀ (a : Condensed.IsDiscrete M) (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
⊢ [Condensed.IsDiscrete M,
      IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
        (NatTrans.app (Adjunction.counit (Condensed.discreteUnderlyingAdj (ModuleCat R))) M),
      essImage (Condensed.discrete (ModuleCat R)) M, essImage (functor R) M,
      IsIso (NatTrans.app (Adjunction.counit (LocallyConstant.adjunction R)) 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))].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
h :
  (S : LightProfinite.{u}) →
    IsColimit
      (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)) ≅
  (LocallyConstant.functor.obj
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).obj
    (P := Presheaf.IsSheaf (coherentTopology LightProfinite)) :=
  LightCondensed.isoLocallyConstantOfIsColimit (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))) h
⊢ LocallyConstant.functor.essImage X

Tactic:
⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Functor.preimageIso, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
h :
  (S : LightProfinite.{u}) →
    IsColimit
      (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone))
i : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)) ≅
  (LocallyConstant.functor.obj
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
          (toLightProfinite.op.obj (Opposite.op (of PUnit.{u + 1}))))).obj
    (P := Presheaf.IsSheaf (coherentTopology LightProfinite)) :=
  LightCondensed.isoLocallyConstantOfIsColimit (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite))) h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
⊢ LightCondensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
⊢ IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
    (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
⊢ LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)

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:
X : LightCondSet
⊢ LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)

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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
⊢ LightCondensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
⊢ essImage (LightCondensed.discrete (Type u)) X

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
⊢ LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X

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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
⊢ LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X

Tactic:
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
⊢ LightCondensed.IsDiscrete X

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
⊢ functor.essImage X

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
⊢ LightCondensed.IsDiscrete X ↔ functor.essImage X

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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
⊢ LightCondensed.IsDiscrete X ↔ functor.essImage X

Tactic:
tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ LightProfinite.isTerminalPUnit adjunction X

Premises used: CategoryTheory.Sheaf.isConstant_iff_mem_essImage, LightProfinite.isTerminalPUnit, LightCondSet.LocallyConstant.adjunction
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
⊢ LightCondensed.IsDiscrete X

Tactic:
1

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

Tactic:
5

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

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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
⊢ LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)

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

Premises used: inferInstance, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', LightProfinite.isTerminalPUnit, LightCondSet.LocallyConstant.adjunction, LightProfinite, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (X.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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ functor.essImage X

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X

Tactic:
6 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X

Tactic:
tfae_have 6 → 4 := fun h ↦
    mem_locallyConstant_essImage_of_isColimit_mapCocone X (fun S ↦ (h S).some)

Premises used: LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X
⊢ functor.essImage X

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X
⊢ ∀ (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (X.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:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X
⊢ ∀ (a : functor.essImage X) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
4 → 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X
⊢ ∀ (a : functor.essImage X) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))

Tactic:
tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
      (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : LightCondSet
tfae_1_iff_2 :
  LightCondensed.IsDiscrete X ↔
    IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
      (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  ∀
    (a :
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))),
    functor.essImage X
tfae_4_to_6 :
  ∀ (a : functor.essImage X) (S : LightProfinite.{u}),
    Nonempty
      (IsColimit
        (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [LightCondensed.IsDiscrete X,
      IsIso (X := obj (LightCondensed.underlying (Type u) ⋙ LightCondensed.discrete (Type u)) X)
        (NatTrans.app (Adjunction.counit (LightCondensed.discreteUnderlyingAdj (Type u))) X),
      essImage (LightCondensed.discrete (Type u)) X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite.{u}),
        Nonempty
          (IsColimit
            (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
              (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
⊢ LightCondensed.IsDiscrete M ↔ LightCondensed.IsDiscrete (obj (LightCondensed.forget R) M)

Tactic:
Sheaf.isConstant_iff_forget (coherentTopology LightProfinite)
    (forget (ModuleCat R)) M LightProfinite.isTerminalPUnit

Premises used: ModuleCat, CategoryTheory.Sheaf.isConstant_iff_forget, LightProfinite.isTerminalPUnit, CategoryTheory.forget, LightProfinite, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type u
inst : Ring R
M : LightCondMod R
⊢ LightCondensed.IsDiscrete M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false