awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
mem_essImage :
  essImage (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))
⊢ Sheaf.IsConstant (coherentTopology CompHaus)
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
constructor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
mem_essImage :
  CondensedSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))
⊢ essImage (discrete (Type (u + 1)))
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
rw [essImage_eq_of_natIso CondensedSet.LocallyConstant.iso.symm]

Premises used: CondensedSet.LocallyConstant.iso, CategoryTheory.Functor.essImage_eq_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ CondensedSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
obj_mem_essImage CondensedSet.LocallyConstant.functor M

Premises used: LocallyConstant.comap, CategoryTheory.Functor.obj_mem_essImage, CategoryTheory.Functor.comp, CondensedSet.LocallyConstant.functor, ModuleCat.carrier
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
this :
  Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
⊢ CondensedSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology CompHaus)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
exact obj_mem_essImage CondensedSet.LocallyConstant.functor M

Premises used: CategoryTheory.Functor.obj_mem_essImage, CondensedSet.LocallyConstant.functor, ModuleCat.carrier
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
rw :
  (functorIsoDiscreteComponents R X).hom ≫ CategoryTheory.Functor.map (functor R) f =
    CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f) ≫
      (functorIsoDiscreteComponents R Y).hom
⊢ CategoryTheory.Functor.map (functor R) f ≫ (functorIsoDiscreteComponents R Y).inv =
    (functorIsoDiscreteComponents R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)

Tactic:
rw [Iso.eq_inv_comp, ← Category.assoc, Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
rw :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f) ≫
        (functorIsoDiscreteAux₂ R Y).hom ≫
          NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)
⊢ ((functorIsoDiscreteAux₂ R X).hom ≫
        NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) X)) ≫
      CategoryTheory.Functor.map (functor R) f =
    CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f) ≫
      (functorIsoDiscreteAux₂ R Y).hom ≫
        NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
rw [assoc, ← Iso.eq_inv_comp,
      ← (discreteUnderlyingAdj (ModuleCat R)).counit_naturality]

Premises used: CategoryTheory.Category.assoc, ModuleCat, CategoryTheory.Adjunction.counit_naturality, Condensed.discreteUnderlyingAdj, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
simp :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (((functorIsoDiscreteAux₂ R X).inv ≫
          CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
            (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)) ≫
        (functorIsoDiscreteAux₂ R Y).hom) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f) ≫
        (functorIsoDiscreteAux₂ R Y).hom ≫
          NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
simp only [← assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
      (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)) ≫
      (functorIsoDiscreteAux₂ R Y).hom
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y) =
    (((functorIsoDiscreteAux₂ R X).inv ≫
          CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
            (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)) ≫
        (functorIsoDiscreteAux₂ R Y).hom) ≫
      NatTrans.app (Adjunction.counit (discreteUnderlyingAdj (ModuleCat R))) (obj (functor R) Y)

Tactic:
congr 1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      (functorIsoDiscreteAux₂ R Y).inv =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
      (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)) ≫
      (functorIsoDiscreteAux₂ R Y).hom

Tactic:
rw [← Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  (CategoryTheory.Functor.map (discrete (ModuleCat R))
          (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
        (functorIsoDiscreteAux₂ R Y).inv).hom =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)).hom
⊢ CategoryTheory.Functor.map (discrete (ModuleCat R))
        (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
      (functorIsoDiscreteAux₂ R Y).inv =
    (functorIsoDiscreteAux₂ R X).inv ≫
      CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)

Tactic:
apply Sheaf.hom_ext

Premises used: CategoryTheory.Sheaf.hom_ext
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
e_a :
  Eq (α :=
    Quiver.Hom (V := CompHausᵒᵖ ⥤ ModuleCat R)
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
        (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (obj (Functor.const CompHausᵒᵖ)
            ((obj (functor R) X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
              (op (CompHaus.of PUnit.{u + 1}))))))
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
        (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)) (obj (Functor.const CompHausᵒᵖ) Y))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ)
          (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (functor R) f))
              (op (CompHaus.of PUnit.{u + 1})) ≫
            (functorIsoDiscreteAux₁ R Y).inv))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) ((functorIsoDiscreteAux₁ R X).inv ≫ f))))
⊢ (CategoryTheory.Functor.map (discrete (ModuleCat R))
          (CategoryTheory.Functor.map (underlying (ModuleCat R)) (CategoryTheory.Functor.map (functor R) f)) ≫
        (functorIsoDiscreteAux₂ R Y).inv).hom =
    ((functorIsoDiscreteAux₂ R X).inv ≫
        CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) f)).hom

Tactic:
simp [functorIsoDiscreteAux₂, ← Functor.map_comp]

Premises used: CondensedMod.LocallyConstant.functorIsoDiscreteAux₂, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := CompHausᵒᵖ ⥤ ModuleCat R)
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
        (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
          (obj (Functor.const CompHausᵒᵖ)
            ((obj (functor R) X).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
              (op (CompHaus.of PUnit.{u + 1}))))))
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus))
        (obj (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R)) (obj (Functor.const CompHausᵒᵖ) Y))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ)
          (NatTrans.app (InducedCategory.Hom.hom (CategoryTheory.Functor.map (functor R) f))
              (op (CompHaus.of PUnit.{u + 1})) ≫
            (functorIsoDiscreteAux₁ R Y).inv))))
    (InducedCategory.Hom.hom
      (CategoryTheory.Functor.map (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (CategoryTheory.Functor.map (Functor.const CompHausᵒᵖ) ((functorIsoDiscreteAux₁ R X).inv ≫ f))))

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Faithful (C := ModuleCat R) (functor R)

Tactic:
(fullyFaithfulFunctor R).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CondensedMod.LocallyConstant.fullyFaithfulFunctor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Full (C := ModuleCat R) (functor R)

Tactic:
(fullyFaithfulFunctor R).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CondensedMod.LocallyConstant.fullyFaithfulFunctor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Faithful.{u + 1, u + 1, u + 2, u + 2} (C := ModuleCat R) (discrete (ModuleCat R))

Tactic:
Functor.Faithful.of_iso (functorIsoDiscrete R)

Premises used: CondensedMod.LocallyConstant.functorIsoDiscrete, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Faithful (C := ModuleCat R) (D := Sheaf (coherentTopology CompHaus) (ModuleCat R))
    (constantSheaf (coherentTopology CompHaus) (ModuleCat R))

Tactic:
inferInstanceAs (discrete (ModuleCat R)).Faithful

Premises used: _private.0.CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Full (C := ModuleCat R) (D := Sheaf (coherentTopology CompHaus) (ModuleCat R))
    (constantSheaf (coherentTopology CompHaus) (ModuleCat R))

Tactic:
inferInstanceAs (discrete (ModuleCat R)).Full

Premises used: _private.0.CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))

Tactic:
inferInstanceAs (discrete (Type (u + 1))).Faithful

Premises used: _private.0.CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor._proof_1
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
⊢ Full (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))

Tactic:
inferInstanceAs (discrete (Type (u + 1))).Full

Premises used: _private.0.CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor._proof_2
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
⊢ HasSheafify (coherentTopology LightProfinite) (ModuleCat R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
⊢ Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))

Tactic:
have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Faithful :=
    inferInstanceAs (discrete _).Faithful
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))

Tactic:
have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Full :=
    inferInstanceAs (discrete (Type u)).Full
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
rw :
  Sheaf.IsConstant (coherentTopology LightProfinite)
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology LightProfinite) (Type u))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj
        (op (LightProfinite.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit
        (constantSheafAdj (coherentTopology LightProfinite) (Type u)
          (isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)))))
      (obj
        (sheafCompose (coherentTopology LightProfinite)
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
            (CC := ModuleCat.carrier)))
        (obj (functor R) M)))

Tactic:
rw [← Sheaf.isConstant_iff_isIso_counit_app]

Premises used: CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
mem_essImage :
  essImage (constantSheaf (coherentTopology LightProfinite) (Type u))
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
⊢ Sheaf.IsConstant (coherentTopology LightProfinite)
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
constructor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
mem_essImage :
  LightCondSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))
⊢ essImage (discrete (Type u))
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
rw [essImage_eq_of_natIso LightCondSet.LocallyConstant.iso.symm]

Premises used: CategoryTheory.Functor.essImage_eq_of_natIso, CategoryTheory.Iso.symm, LightCondSet.LocallyConstant.iso
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ LightCondSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
obj_mem_essImage LightCondSet.LocallyConstant.functor M

Premises used: LocallyConstant.comap, CategoryTheory.Functor.obj_mem_essImage, CategoryTheory.Functor.comp, ModuleCat.carrier, LightCondSet.LocallyConstant.functor
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type u
inst : Ring R
M : ModuleCat R
this_1 :
  Faithful (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
this :
  Full (D := Sheaf (coherentTopology LightProfinite) (Type u))
    (constantSheaf (coherentTopology LightProfinite) (Type u))
⊢ LightCondSet.LocallyConstant.functor.essImage
    (obj
      (sheafCompose (coherentTopology LightProfinite)
        (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
          (CC := ModuleCat.carrier)))
      (obj (functor R) M))

Tactic:
exact obj_mem_essImage LightCondSet.LocallyConstant.functor M

Premises used: CategoryTheory.Functor.obj_mem_essImage, ModuleCat.carrier, LightCondSet.LocallyConstant.functor