awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
inst_1 : HasProp P PUnit.{u + 1}
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Type (max u w)
S : CompHausLike P
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) X
this : Preregular.{u, u + 1} (CompHausLike P)
a :
  Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z :=
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
          (Functor.obj
              (functor.{u, w} P hs :
                Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
              X :
            Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))).obj
      (op (of P PUnit.{u + 1})))
    (⇑(map
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (unit P hs) X)) :
            (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj X)) →
              (fun (X : Type (max u w)) ↦ X)
                ((functor P hs ⋙
                      (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                        (op (of P PUnit.{u + 1}))).obj
                  X))
          f) :
      (a : (↑S.toTop : Type u)) → ((functor P hs).obj X).obj.obj (op (of P PUnit.{u + 1})))
x : (↑(↑a : Set (↑S.toTop : Type u)) : Type u)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
⊢ Preregular.{u, u + 1} (CompHausLike P)

Tactic:
have := CompHausLike.preregular hs
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
this_1 : Preregular.{u, u + 1} (CompHausLike P)
this : PreservesFiniteProducts (Functor.obj (sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))) X) :=
  ⋯
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app (InducedCategory.Hom.hom (NatTrans.app (counit P hs) X)) (op (of P PUnit.{u + 1}))) :
          TypeCat.Fun
            (LocallyConstant PUnit.{u + 1}
              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))))
            (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
        (a : LocallyConstant PUnit.{u + 1} (X.obj.obj (op (of P PUnit.{u + 1})))) → X.obj.obj (op (of P PUnit.{u + 1})))
      (LocallyConstant.const PUnit.{u + 1} x) =
    x

Tactic:
apply presheaf_ext ((unit P hs).app _ x)

Premises used: CategoryTheory.ConcreteCategory.hom, CompHausLike.LocallyConstant.unit, DFunLike.coe, CategoryTheory.NatTrans.app, CompHausLike.LocallyConstant.presheaf_ext
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X_1 : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
X : Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))
x : X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))
this_1 : Preregular.{u, u + 1} (CompHausLike P)
this : PreservesFiniteProducts (Functor.obj (sheafToPresheaf (coherentTopology (CompHausLike P)) (Type (max u w))) X) :=
  ⋯
a :
  Fiber (Y := (↑((of P PUnit.{u + 1}).toTop (P := P)) : Type u)) (Z :=
    X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))
    (⇑((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (unit P hs)
                  (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1})))) :
              (a : (fun (X : Type (max u w)) ↦ X) ((𝟭 (Type (max u w))).obj (X.obj.obj (op (of P PUnit.{u + 1}))))) →
                (fun (X : Type (max u w)) ↦ X)
                  ((functor P hs ⋙
                        (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w))).obj
                          (op (of P PUnit.{u + 1}))).obj
                    (X.obj.obj (op (of P PUnit.{u + 1})))))
            x :
          (fun (X : Type (max u w)) ↦ X)
            ((Functor.comp (D := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  (functor.{u, w} P hs :
                    Type (max u w) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)))
                  (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u w)))
                      (op (of P PUnit.{u + 1})) :
                    Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w)) ⥤
                      Type (max u w))).obj
              (X.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P))).obj (op (of P PUnit.{u + 1}))))) :
      (a : (↑(of P PUnit.{u + 1}).toTop : Type u)) → X.obj.obj (op (of P PUnit.{u + 1})))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
T : CompHausLike P
g : T ⟶ S
X : TopCat
inst_2 : HasExplicitFiniteCoproducts P
inst_3 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
inst_4 : HasExplicitFiniteCoproducts P
⊢ IsIso (Y :=
    Functor.comp (D := Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u u_1)))
      (functor.{u, u_1} P hs :
        Type (max u u_1) ⥤ Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u u_1)))
      (Functor.obj (sheafSections (coherentTopology (CompHausLike P)) (Type (max u u_1))) (op (of P PUnit.{u + 1})) :
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u u_1)) ⥤ Type (max u u_1)))
    (Adjunction.unit (adjunction P hs))

Tactic:
inferInstanceAs (IsIso (unitIso P hs).hom)

Premises used: _private.0.CompHausLike.LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction._proof_1
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ functor.Faithful

Tactic:
functorFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CondensedSet.LocallyConstant.functorFullyFaithful
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ functor.Full

Tactic:
functorFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CondensedSet.LocallyConstant.functorFullyFaithful
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ Functor.Faithful (discrete (Type (u_1 + 1)))

Tactic:
Functor.Faithful.of_iso iso

Premises used: CondensedSet.LocallyConstant.iso, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ Functor.Full (discrete (Type (u_1 + 1)))

Tactic:
Functor.Full.of_iso iso

Premises used: CondensedSet.LocallyConstant.iso, CategoryTheory.Functor.Full.of_iso
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
S : LightProfinite
p :
  (↑(S.toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u) →
    Prop
⊢ HasProp.{u}
    (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))
    (Subtype p)

Tactic:
⟨⟨(inferInstance : TotallyDisconnectedSpace (Subtype p)),
    (inferInstance : SecondCountableTopology {s | p s})⟩⟩

Premises used: inferInstance, And.intro, CompHausLike.HasProp.mk
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ functor.Faithful

Tactic:
functorFullyFaithful.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, LightCondSet.LocallyConstant.functorFullyFaithful
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ functor.Full

Tactic:
functorFullyFaithful.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, LightCondSet.LocallyConstant.functorFullyFaithful
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ Functor.Faithful (LightCondensed.discrete (Type u))

Tactic:
Functor.Faithful.of_iso iso.{u}

Premises used: LightCondSet.LocallyConstant.iso, CategoryTheory.Functor.Faithful.of_iso
-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
⊢ Functor.Full (LightCondensed.discrete (Type u))

Tactic:
Functor.Full.of_iso iso.{u}

Premises used: CategoryTheory.Functor.Full.of_iso, LightCondSet.LocallyConstant.iso
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
⊢ Preregular.{u, u + 1} (CompHausLike P)

Tactic:
have := CompHausLike.preregular hs
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
this : Preregular.{u, u + 1} (CompHausLike P)
hF :
  Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u w)) →ₗ[R] (↑x2 : Type (max u w)))
        (CC := ModuleCat.carrier))
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X)

Tactic:
apply Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp
      (s := CategoryTheory.forget (ModuleCat R))

Premises used: ModuleCat, CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp, CategoryTheory.forget
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u w)) →ₗ[R] (↑x2 : Type (max u w)))
        (CC := ModuleCat.carrier))

Tactic:
((CompHausLike.LocallyConstant.functor P hs).obj _).property

Premises used: LocallyConstant.comap, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, CompHausLike.LocallyConstant.functor, CategoryTheory.Functor.obj
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (max u w)
inst : Ring R
inst_1 : HasExplicitFiniteCoproducts P
inst_2 : HasExplicitPullbacks P
hs :
  ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
    EffectiveEpi f →
      Function.Surjective (α := (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) X) (β :=
        (fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) Y)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) f) :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) X) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) Y)
X : ModuleCat R
this : Preregular.{u, u + 1} (CompHausLike P)
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (obj (functorToPresheaves.{w, u} (P := P) R) X ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u w)) →ₗ[R] (↑x2 : Type (max u w)))
        (CC := ModuleCat.carrier))

Tactic:
exact ((CompHausLike.LocallyConstant.functor P hs).obj _).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CompHausLike.LocallyConstant.functor, CategoryTheory.Functor.obj
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
⊢ IsIso (C := CondensedSet) (X :=
    obj (C := CondensedMod R)
      (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 (presheafToSheaf (coherentTopology CompHaus) (ModuleCat R))
        (obj (Functor.const CompHausᵒᵖ)
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))))
    (Y :=
    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))
    (CategoryStruct.comp (Y :=
        obj
          (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
              (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
            constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
          ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))
        (NatTrans.app
          (Iso.hom
            (constantCommuteCompose (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).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))))
        (NatTrans.app
          (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
          (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))) :
      obj
          (constantSheaf (coherentTopology CompHaus) (ModuleCat R) ⋙
            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).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
            (op (CompHaus.of PUnit.{u + 1}))) ⟶
        obj (𝟭 (Sheaf (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)))

Tactic:
IsIso.comp_isIso' inferInstance ?_

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.Condensed.Discrete.Module
Goal:
P : TopCat.{u} → Prop
R : Type (u + 1)
inst : Ring R
M : ModuleCat R
⊢ Faithful (D := Sheaf (coherentTopology CompHaus) (Type (u + 1)))
    (constantSheaf (coherentTopology CompHaus) (Type (u + 1)))

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

Tactic:
have : (constantSheaf (coherentTopology CompHaus) (Type (u + 1))).Full :=
    inferInstanceAs (discrete _).Full
-- 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)))
rw :
  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))
⊢ IsIso (X :=
    obj
      (CategoryTheory.forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
          (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC := ModuleCat.carrier) ⋙
        constantSheaf (coherentTopology CompHaus) (Type (u + 1)))
      ((obj (functor R) M).obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj
        (op (CompHaus.of PUnit.{u + 1}))))
    (NatTrans.app
      (Adjunction.counit (constantSheafAdj (coherentTopology CompHaus) (Type (u + 1)) CompHaus.isTerminalPUnit))
      (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 [← Sheaf.isConstant_iff_isIso_counit_app]

Premises used: CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app