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)
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
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)
⊢ (f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      ((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)) g :
          (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
        (preimage (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          a)) =
    Fiber.image (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a

Tactic:
map_preimage_eq_image_map _ _ a

Premises used: Function.Fiber.map_preimage_eq_image_map
-- 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
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)
⊢ (f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      ((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)) g :
          (a : (↑T.toTop : Type u)) → (↑S.toTop : Type u))
        (preimage (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          a)) =
    Fiber.image (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a

Tactic:
exact map_preimage_eq_image_map _ _ a

Premises used: Function.Fiber.map_preimage_eq_image_map
-- 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
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Continuous (Y := (↑(S.toTop (P := P)) : Type u))
    fun (x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)) ↦
    (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)) g :
        (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
      (↑x : (↑T.toTop : Type u))

Tactic:
fun_prop
-- 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
a :
  Fiber (Y := (↑(T.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Continuous (Y :=
    (↑((fiber.{u, w} (P := P) f
              (Fiber.mk (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                ((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)) g :
                    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
                  (preimage
                    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                    a)))).toTop
          (P := P)) :
      Type u))
    fun (x : (↑((fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.hom) f) a).toTop (P := P)) : Type u)) ↦
    Subtype.mk (p := fun (x : (↑(S.toTop (P := P)) : Type u)) ↦
      Membership.mem (γ := Set (↑(S.toTop (P := P)) : Type u))
        ((↑(Fiber.mk (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                ((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)) g :
                    (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) →
                      (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
                  (preimage
                    (⇑(comap (TopCat.Hom.hom g.hom) f) : (a : (↑T.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                    a))) :
            Set (↑(S.toTop (P := P)) : Type u)) :
          Set (↑(S.toTop (P := P)) : Type u))
        x)
      ((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)) g :
          (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) T) → (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) S)
        (↑x : (↑T.toTop : Type u)))
      ⋯

Tactic:
exact Continuous.subtype_mk (by fun_prop) _

Premises used: Continuous.subtype_mk
-- 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)
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
S T : (CompHausLike P)ᵒᵖ
f : LocallyConstant (↑((unop S).toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
g : S ⟶ T
a :
  Fiber (Y := (↑((unop T).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Eq (α := S ⟶ op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a))
    (g ≫ Quiver.Hom.op (sigmaIncl (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a))
    (Quiver.Hom.op
        (sigmaIncl (P := P) f
          (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
            ((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)) g.unop :
                (a : (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop T)) →
                  (fun (X : CompHausLike P) ↦ (↑X.toTop : Type u)) (unop S))
              (preimage
                (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                  (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                a)))) ≫
      Quiver.Hom.op (componentHom (P := P) f g.unop a))

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, CategoryTheory.InducedCategory.homMk, ContinuousMap.comp, Quiver.Hom.unop, CompHausLike.LocallyConstant.componentHom, CompHausLike.LocallyConstant.sigmaIncl, rfl, TopologicalSpace.Fiber.sigmaIncl
-- 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_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S_1.toTop (P := P)) : Type u) (Y_1.obj (op (of P PUnit.{u + 1})))
T_1 : CompHausLike P
g_1 : T_1 ⟶ S_1
inst_2 : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_3 : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
h :
  ∀ (f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S),
    Eq (α := Y.obj T)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
              (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) g ≫
            match (motive :=
              (x : (CompHausLike P)ᵒᵖ) →
                Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶
                  Y.obj x)
              T with
            | op S => counitAppApp.{u, w} (P := P) S Y))
        f)
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((match (motive :=
              (x : (CompHausLike P)ᵒᵖ) →
                Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶
                  Y.obj x)
              S with
            | op S => counitAppApp.{u, w} (P := P) S Y) ≫
            Y.map g))
        f)
⊢ Eq (α :=
    Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S ⟶ Y.obj T)
    (CategoryTheory.Functor.map (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1}))))
        g ≫
      match (motive :=
        (x : (CompHausLike P)ᵒᵖ) →
          Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶ Y.obj x)
        T with
      | op S => counitAppApp.{u, w} (P := P) S Y)
    ((match (motive :=
        (x : (CompHausLike P)ᵒᵖ) →
          Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) x ⟶ Y.obj x)
        S with
      | op S => counitAppApp.{u, w} (P := P) S Y) ≫
      Y.map g)

Tactic:
ext f
-- 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_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f_1 : LocallyConstant (↑(S_1.toTop (P := P)) : Type u) (Y_1.obj (op (of P PUnit.{u + 1})))
T_1 : CompHausLike P
g_1 : T_1 ⟶ S_1
inst_2 : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_3 : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S
a :
  Fiber (Y := (↑((unop T).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Fiber.image
      (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a =
    Fiber.image (Y := (↑((unop S).toTop (P := P)) : Type u))
      ((⇑f : (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) :
        (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          ((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)) g.unop :
              (a : (↑(unop T).toTop : Type u)) → (↑(unop S).toTop : Type u))
            (preimage
              (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
              a)) :
        Fiber (Y := (↑((unop S).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
          (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))))

Tactic:
image_eq_image_mk (g := g.unop) (a := a)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.unop, DFunLike.coe, Function.Fiber.image_eq_image_mk
-- 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_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f_1 : LocallyConstant (↑(S_1.toTop (P := P)) : Type u) (Y_1.obj (op (of P PUnit.{u + 1})))
T_1 : CompHausLike P
g_1 : T_1 ⟶ S_1
inst_2 : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_3 : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S
a :
  Fiber (Y := (↑((unop T).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Fiber.image
      (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a =
    Fiber.image (Y := (↑((unop S).toTop (P := P)) : Type u))
      ((⇑f : (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) :
        (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
      (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          ((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)) g.unop :
              (a : (↑(unop T).toTop : Type u)) → (↑(unop S).toTop : Type u))
            (preimage
              (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
              a)) :
        Fiber (Y := (↑((unop S).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
          (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))))

Tactic:
exact image_eq_image_mk (g := g.unop) (a := a)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.unop, DFunLike.coe, Function.Fiber.image_eq_image_mk
-- 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)
X : Type (max u w)
rw :
  Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
      (TopCat.toSheafCompHausLike.{w, u} P (TopCat.discrete.obj X) hs :
        have this := ⋯;
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))
⊢ Presheaf.IsSheaf (C := CompHausLike P) (coherentTopology (CompHausLike P))
    (Functor.obj (functorToPresheaves.{u, w} (P := P)) X)

Tactic:
rw [Presheaf.isSheaf_of_iso_iff (functorToPresheavesIso P hs X)]

Premises used: CategoryTheory.Presheaf.isSheaf_of_iso_iff, CompHausLike.LocallyConstant.functorToPresheavesIso
-- 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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
      (TopCat.toSheafCompHausLike.{w, u} P (TopCat.discrete.obj X) hs :
        have this := ⋯;
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))

Tactic:
((TopCat.discrete.obj X).toSheafCompHausLike P hs).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, TopCat.discrete, TopCat.toSheafCompHausLike, CategoryTheory.Functor.obj
-- 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)
X : Type (max u w)
⊢ Presheaf.IsSheaf (coherentTopology (CompHausLike P))
    (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
      (TopCat.toSheafCompHausLike.{w, u} P (TopCat.discrete.obj X) hs :
        have this := ⋯;
        Sheaf (C := CompHausLike P) (coherentTopology (CompHausLike P)) (Type (max u w))))

Tactic:
exact ((TopCat.discrete.obj X).toSheafCompHausLike P hs).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, TopCat.discrete, TopCat.toSheafCompHausLike, CategoryTheory.Functor.obj
-- 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
⊢ 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)
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)
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom
                (ObjectProperty.homMk (P := Presheaf.IsSheaf (coherentTopology (CompHausLike P)))
                  (counitApp (P := P)
                    (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)))))))
              (op S)) :
          TypeCat.Fun (LocallyConstant (↑(S.toTop (P := P)) : Type u) (LocallyConstant PUnit.{u + 1} X))
            (LocallyConstant (↑(S.toTop (P := P)) : Type u) X)) :
        (a : LocallyConstant (↑S.toTop : Type u) (LocallyConstant PUnit.{u + 1} X)) →
          LocallyConstant (↑S.toTop : Type u) X)
      (map (fun (x : X) ↦ LocallyConstant.const PUnit.{u + 1} x) f) =
    f

Tactic:
apply presheaf_ext
    (X := ((functor P hs).obj X).obj) (Y := ((functor.{u, w} P hs).obj X).obj)
      (f.map ((unit P hs).app X))