awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Epi
Goal:
R : Type (u + 1)
inst : Ring R
X Y : CondensedMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : CompHaus.{u}) (y : (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S)) : Type (u + 1))),
      ∃ (S' : CompHaus.{u}) (φ : S' ⟶ S) (_ :
        Function.Surjective (α :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S')
          (β :=
          (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
            S)
          (⇑(hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                  (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
                (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) φ) :
            (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S') →
              (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) S))
        (x : (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')) : Type (u + 1))),
        Eq (α := (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')) : Type (u + 1)))
          ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
                  ModuleCat.carrier) (X := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S'))
                  (f.hom.app (op S')) :
                (a : (↑(X.obj.obj (op S')) : Type (u + 1))) → (↑(Y.obj.obj (op S')) : Type (u + 1)))
              x :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')) : Type (u + 1)))
          ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
                  ModuleCat.carrier) (Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).map (op φ)) :
                (a : (↑(Y.obj.obj (op S)) : Type (u + 1))) → (↑(Y.obj.obj (op S')) : Type (u + 1)))
              y :
            (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S')) : Type (u + 1)))

Tactic:
Condensed.epi_iff_locallySurjective_on_compHaus _ f

Premises used: Condensed.epi_iff_locallySurjective_on_compHaus
-- Module: Mathlib.Condensed.Epi
Goal:
R : Type (u + 1)
inst : Ring R
X Y : CondensedMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : Stonean.{u}),
      Function.Surjective (α :=
        (↑(X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)) : Type (u + 1))) (β :=
        (↑(Y.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus)) : Type (u + 1)))
        (⇑(hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (u + 1)) →ₗ[R] (↑x2 : Type (u + 1))) (CC :=
              ModuleCat.carrier) (X := X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)).obj (op S.compHaus))
              (f.hom.app (op S.compHaus))) :
          (a : (↑(X.obj.obj (op S.compHaus)) : Type (u + 1))) → (↑(Y.obj.obj (op S.compHaus)) : Type (u + 1)))

Tactic:
have : HasLimitsOfSize.{u, u + 1} (ModuleCat R) :=
    hasLimitsOfSizeShrink.{u, u + 1, u + 1, u + 1} _
  Condensed.epi_iff_surjective_on_stonean _ f

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink, ModuleCat, Condensed.epi_iff_surjective_on_stonean
-- Module: Mathlib.Condensed.Equivalence
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Condensed.{u, v_1, u_1} A
inst_1 : ∀ (Y : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow Y profiniteToCompHaus.op) A
⊢ Presheaf.IsSheaf (coherentTopology Profinite)
    (profiniteToCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)))

Tactic:
((ProfiniteCompHaus.equivalence A).inverse.obj X).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, Condensed.ProfiniteCompHaus.equivalence, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Condensed.Equivalence
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Condensed.{u, v_1, u_1} A
inst_1 : ∀ (Y : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow Y Stonean.toCompHaus.op) A
⊢ Presheaf.IsSheaf (coherentTopology Stonean)
    (Stonean.toCompHaus.op ⋙ X.obj (P := Presheaf.IsSheaf (coherentTopology CompHaus)))

Tactic:
((StoneanCompHaus.equivalence A).inverse.obj X).property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.comp, Condensed.StoneanCompHaus.equivalence, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_2 rw : PreservesFiniteProducts F
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective F]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_2 : PreservesFiniteProducts F
⊢ PreservesFiniteProducts F

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_2 : PreservesFiniteProducts F
⊢ PreservesFiniteProducts F

Tactic:
exact ⟨fun _ ↦ inferInstance⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteProducts.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
apply : IsSheaf (coherentTopology Stonean) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Stonean) F

Tactic:
apply isSheaf_coherent_of_projective_of_comp F (CategoryTheory.forget A)

Premises used: CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp, CategoryTheory.forget
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteProducts.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_5 rw : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Stonean) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteProducts.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X Stonean.toCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteProducts.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Stoneanᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
exact ⟨fun _ ↦ inferInstance⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_2 : PreservesFiniteProducts F
hF : EqualizerCondition F
rw : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_2 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Premises used: inferInstance, And.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_2 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
apply : IsSheaf (coherentTopology Profinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Profinite) F

Tactic:
apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)

Premises used: CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp, CategoryTheory.forget
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
rw :
  PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology Profinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Premises used: inferInstance, And.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape.{u, u + 1, v_1, u_1} (StructuredArrow X profiniteToCompHaus.op) A
FA : A → A → Type u_2
CA : A → Type u_3
inst_2 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_4 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} Profiniteᵒᵖ A
inst_5 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
rw : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ IsSheaf (coherentTopology CompHaus) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Premises used: inferInstance, And.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
apply : IsSheaf (coherentTopology CompHaus) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology CompHaus) F

Tactic:
apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)

Premises used: CategoryTheory.Presheaf.isSheaf_coherent_of_hasPullbacks_of_comp, CategoryTheory.forget
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
rw :
  PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology CompHaus) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
⟨⟨fun _ ↦ inferInstance⟩, hF⟩

Premises used: inferInstance, And.intro, CategoryTheory.Limits.PreservesFiniteProducts.mk
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
FA : A → A → Type u_2
CA : A → Type u_3
inst_1 : (X Y : A) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FA X Y) (CA X) (CA Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} A FA (CC := CA)
inst_3 : ReflectsFiniteLimits.{v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget A (FC := FA) (CC := CA))
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} CompHausᵒᵖ A
inst_4 : PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
hF : EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ PreservesFiniteProducts (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA)) ∧
    EqualizerCondition (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Condensed.{u_2, v_1, u_1} A
⊢ EqualizerCondition (X.obj (P := IsSheaf (coherentTopology CompHaus)))

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.obj |>.mp X.property |>.2

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.right, Iff.mp
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Condensed.{u_2, v_1, u_1} A
⊢ PreservesFiniteProducts (X.obj (P := IsSheaf (coherentTopology CompHaus)))

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.obj |>.mp
    X.property |>.1

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.left, Iff.mp
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Sheaf.{u, v_1, u + 1, u_1} (coherentTopology Profinite) A
⊢ PreservesFiniteProducts (X.obj (P := IsSheaf (coherentTopology Profinite)))

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.obj |>.mp
    X.property |>.1

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.left, Iff.mp
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Sheaf.{u, v_1, u + 1, u_1} (coherentTopology Profinite) A
⊢ EqualizerCondition (X.obj (P := IsSheaf (coherentTopology Profinite)))

Tactic:
isSheaf_iff_preservesFiniteProducts_and_equalizerCondition X.obj |>.mp X.property |>.2

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, And.right, Iff.mp
-- Module: Mathlib.Condensed.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : Sheaf.{u, v_1, u + 1, u_1} (coherentTopology Stonean) A
⊢ PreservesFiniteProducts (X.obj (P := IsSheaf (coherentTopology Stonean)))

Tactic:
isSheaf_iff_preservesFiniteProducts_of_projective X.obj |>.mp X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective, Iff.mp
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ Condensed.ulift.Full

Tactic:
show (sheafCompose _ _).Full from inferInstance

Premises used: Condensed.ulift, inferInstance
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ Condensed.ulift.Faithful

Tactic:
show (sheafCompose _ _).Faithful from inferInstance

Premises used: Condensed.ulift, inferInstance
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ compHausToCondensed'.Full

Tactic:
inferInstanceAs ((coherentTopology CompHaus).yoneda).Full

Premises used: _private.0.instFullCompHausCondensedTypeCompHausToCondensed'._proof_1
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ compHausToCondensed'.Faithful

Tactic:
inferInstanceAs ((coherentTopology CompHaus).yoneda).Faithful

Premises used: _private.0.instFaithfulCompHausCondensedTypeCompHausToCondensed'._proof_1
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ compHausToCondensed.Full

Tactic:
inferInstanceAs (_ ⋙ _).Full

Premises used: _private.0.instFullCompHausCondensedSetCompHausToCondensed._proof_1
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ compHausToCondensed.Faithful

Tactic:
inferInstanceAs (_ ⋙ _).Faithful

Premises used: _private.0.instFaithfulCompHausCondensedSetCompHausToCondensed._proof_1
-- Module: Mathlib.Condensed.Functors
Goal:
⊢ PreservesFiniteCoproducts compHausToCondensed

Tactic:
inferInstanceAs <| PreservesFiniteCoproducts (coherentTopology _).uliftYoneda

Premises used: _private.0.instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed._proof_1
-- Module: Mathlib.Condensed.Light.AB
Goal:
R : Type u
inst : Ring R
⊢ CountableAB4Star.{u + 1, u + 1} (LightCondMod R)

Tactic:
have := hasExactLimitsOfShape_of_preservesEpi (LightCondMod R) (Discrete ℕ)
  CountableAB4Star.of_hasExactLimitsOfShape_nat _

Premises used: CategoryTheory.hasExactLimitsOfShape_of_preservesEpi, Nat, CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat, LightCondMod, CategoryTheory.Discrete