awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
⊢ Condensed.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 : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
⊢ Condensed.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' _ CompHaus.isTerminalPUnit adjunction _

Premises used: inferInstance, CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app', CondensedSet.LocallyConstant.adjunction, CompHaus.isTerminalPUnit, CompHaus, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ Condensed.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 : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ Sheaf.IsConstant (coherentTopology Profinite)
    (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)

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 : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)

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:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
⊢ Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)

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:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
⊢ ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ X.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:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
⊢ LocallyConstant.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 : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
⊢ ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X

Tactic:
7 → 4

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

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

Premises used: CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
tfae_7_to_4 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X
⊢ LocallyConstant.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 : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
tfae_7_to_4 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X
⊢ ∀ (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ X.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:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
tfae_7_to_4 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X
⊢ ∀ (a : LocallyConstant.functor.essImage X) (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))

Tactic:
4 → 7

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

Tactic:
tfae_have 4 → 7 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv (isoWhiskerLeft profiniteToCompHaus.op
      ((sheafToPresheaf _ _).mapIso i))
      (Condensed.isColimitLocallyConstantPresheafDiagram Y S)⟩
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
X : CondensedSet
tfae_1_iff_2 :
  Condensed.IsDiscrete X ↔
    IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
      (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X)
tfae_1_iff_3 : Condensed.IsDiscrete X ↔ essImage (discrete (Type (u + 1))) X
tfae_1_iff_4 : Condensed.IsDiscrete X ↔ LocallyConstant.functor.essImage X
tfae_1_iff_5 : Condensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_1_iff_6 :
  Condensed.IsDiscrete X ↔
    Sheaf.IsConstant (coherentTopology Profinite)
      (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X)
tfae_7_to_4 :
  ∀
    (a :
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))),
    LocallyConstant.functor.essImage X
tfae_4_to_7 :
  ∀ (a : LocallyConstant.functor.essImage X) (S : Profinite.{u}),
    Nonempty.{u + 3}
      (IsColimit
        ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
          S.asLimitCone.op))
⊢ [Condensed.IsDiscrete X,
      IsIso (X := obj (underlying (Type (u + 1)) ⋙ discrete (Type (u + 1))) X)
        (NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (Type (u + 1)))) X),
      essImage (discrete (Type (u + 1))) X, LocallyConstant.functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      Sheaf.IsConstant (coherentTopology Profinite)
        (obj (Equivalence.inverse (ProfiniteCompHaus.equivalence (Type (u + 1)))) X),
      ∀ (S : Profinite.{u}),
        Nonempty.{u + 3}
          (IsColimit
            ((profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone
              S.asLimitCone.op))].TFAE

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

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

Premises used: ModuleCat, CategoryTheory.Sheaf.isConstant_iff_forget, CategoryTheory.forget, CompHaus.isTerminalPUnit, CompHaus, CategoryTheory.coherentTopology
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
⊢ HasLimitsOfSize.{u, u + 1, u + 1, u + 2} (ModuleCat R)

Tactic:
hasLimitsOfSizeShrink.{u, u + 1, u + 1, u + 1} _

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink
-- Module: Mathlib.Condensed.Discrete.Characterization
Goal:
R : Type (u + 1)
inst : Ring R
M : CondensedMod R
⊢ 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
⊢ IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
    (NatTrans.app (Adjunction.counit (Condensed.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 + 1)
inst : Ring R
M : CondensedMod R
⊢ Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.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 + 1)
inst : Ring R
M : CondensedMod R
⊢ Condensed.IsDiscrete M ↔
    IsIso (X := obj (Condensed.underlying (ModuleCat R) ⋙ Condensed.discrete (ModuleCat R)) M)
      (NatTrans.app (Adjunction.counit (Condensed.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 + 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)
⊢ 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)
⊢ essImage (Condensed.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 + 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)
⊢ Condensed.IsDiscrete M ↔ essImage (Condensed.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 + 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)
⊢ Condensed.IsDiscrete M ↔ essImage (Condensed.discrete (ModuleCat R)) M

Tactic:
tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- 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
⊢ 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
⊢ 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 + 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
⊢ Condensed.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 + 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
⊢ Condensed.IsDiscrete M ↔ essImage (functor R) M

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

Premises used: CategoryTheory.Sheaf.isConstant_iff_mem_essImage, CondensedMod.LocallyConstant.adjunction, CompHaus.isTerminalPUnit
-- 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

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
⊢ 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