awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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
have tfae_1_iff_6 : 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
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (goal)
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))
⊢ Condensed.IsDiscrete M
have 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))
Tactic: rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)]
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (goal)
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
⊢ Nonempty.{u + 3}
    (IsColimit
      ((profiniteToCompHaus.op ⋙ M.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))).mapCocone S.asLimitCone.op))
have 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))
Tactic: rw [isDiscrete_iff_isDiscrete_forget, ((CondensedSet.isDiscrete_tfae _).out 0 6 :)] at h
Cleared hypotheses: h, S
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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
have 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))
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⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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),
      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
have 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)
Tactic: tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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
have tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ essImage (LightCondensed.discrete (Type u)) X
Tactic: tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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
have tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
Tactic: tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _ LightProfinite.isTerminalPUnit adjunction X
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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 (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
have tfae_1_iff_5 : 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
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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)
⊢ [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
have tfae_6_to_4 : ∀
  (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)
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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
⊢ [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
have tfae_4_to_6 : ∀ (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)⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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),
      essImage (LightCondensed.discrete (ModuleCat R)) M, essImage (functor R) 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)))].TFAE
have 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)
Tactic: tfae_have 1 ↔ 2 := Sheaf.isConstant_iff_isIso_counit_app _ _ _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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, essImage (functor R) 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)))].TFAE
have tfae_1_iff_3 : LightCondensed.IsDiscrete M ↔ essImage (LightCondensed.discrete (ModuleCat R)) M
Tactic: tfae_have 1 ↔ 3 := ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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,
      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, essImage (functor R) 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)))].TFAE
have tfae_1_iff_4 : LightCondensed.IsDiscrete M ↔ essImage (functor R) M
Tactic: tfae_have 1 ↔ 4 := Sheaf.isConstant_iff_mem_essImage _
    LightProfinite.isTerminalPUnit (adjunction R) _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (hypothesis)
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 (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, essImage (functor R) 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)))].TFAE
have tfae_1_iff_5 : 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) _
-- Lean 4 proof step from Mathlib.Condensed.Discrete.Characterization (goal)
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)))
⊢ LightCondensed.IsDiscrete M
have rw : ∀ (S : LightProfinite.{u}),
  Nonempty.{u + 2}
    (IsColimit
      ((obj (LightCondensed.forget R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).mapCocone
        (coconeRightOpOfCone S.asLimitCone)))
Tactic: rw [isDiscrete_iff_isDiscrete_forget, ((LightCondSet.isDiscrete_tfae _).out 0 5 :)]