awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Condensed.Light.AB
Goal:
R : Type u
inst : Ring R
⊢ IsGrothendieckAbelian.{u, u + 1, u + 1} (LightCondMod R)

Tactic:
Sheaf.isGrothendieckAbelian_of_essentiallySmall _ _

Premises used: CategoryTheory.Sheaf.isGrothendieckAbelian_of_essentiallySmall
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X : LightCondensed.{u, v, w} C
⊢ InducedCategory.Hom.hom (𝟙 X) = 𝟙 (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y Z : LightCondensed.{u, v, w} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : LightCondensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
h₁ : f.hom = g.hom
⊢ f = g

Tactic:
apply Sheaf.hom_ext

Premises used: CategoryTheory.Sheaf.hom_ext
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : LightCondensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
h₁ : ∀ (x : LightProfiniteᵒᵖ), f.hom.app x = g.hom.app x
⊢ f.hom = g.hom

Tactic:
ext
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : LightCondensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
x : LightProfiniteᵒᵖ
⊢ f.hom.app x = g.hom.app x

Tactic:
h _
-- Module: Mathlib.Condensed.Light.Basic
Goal:
C : Type w
inst : Category.{v, w} C
X Y : LightCondensed.{u, v, w} C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
x : LightProfiniteᵒᵖ
⊢ f.hom.app x = g.hom.app x

Tactic:
exact h _
-- Module: Mathlib.Condensed.Light.Basic
Goal:
X Y : LightCondSet
f : X ⟶ Y
S T : LightProfiniteᵒᵖ
g : S ⟶ T
x : X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S
⊢ Eq (α := (fun (X : Type u) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app T) :
          (a : (fun (X : Type u) ↦ X) (X.obj.obj T)) → (fun (X : Type u) ↦ X) (Y.obj.obj T))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map g) :
              (a : (fun (X : Type u) ↦ X) (X.obj.obj S)) → (fun (X : Type u) ↦ X) (X.obj.obj T))
            x :
          (fun (X : Type u) ↦ X) (X.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T)) :
      (fun (X : Type u) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).map g) :
          (a : (fun (X : Type u) ↦ X) (Y.obj.obj S)) → (fun (X : Type u) ↦ X) (Y.obj.obj T))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app S) :
              (a : (fun (X : Type u) ↦ X) (X.obj.obj S)) → (fun (X : Type u) ↦ X) (Y.obj.obj S))
            x :
          (fun (X : Type u) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj S)) :
      (fun (X : Type u) ↦ X) (Y.obj (P := Presheaf.IsSheaf (coherentTopology LightProfinite)).obj T))

Tactic:
simp
-- Module: Mathlib.Condensed.Light.EffectiveEpi
Goal:
⊢ IsRegularEpiCategory LightCondSet

Tactic:
inferInstanceAs <| IsRegularEpiCategory (Sheaf _ _)

Premises used: _private.0.instIsRegularEpiCategoryLightCondSet._proof_1
-- Module: Mathlib.Condensed.Light.EffectiveEpi
Goal:
⊢ lightProfiniteToLightCondSet.PreservesEffectiveEpis

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf : Epi (X := Functor.obj (LightCondensed.forget R) X_1) (CategoryTheory.Functor.map (LightCondensed.forget R) f)
rw :
  ∀
    (hf :
      IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
        (CategoryTheory.Functor.map (LightCondensed.forget R) f)),
    IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA :=
      ModuleCat.carrier) f
⊢ Epi f

Tactic:
rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf :
  IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
    (CategoryTheory.Functor.map (LightCondensed.forget R) f)
⊢ IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
    f

Tactic:
(Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mpr hf

Premises used: Iff.mpr, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf :
  IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
    (CategoryTheory.Functor.map (LightCondensed.forget R) f)
⊢ IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
    f

Tactic:
exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mpr hf

Premises used: Iff.mpr, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf : Epi f
rw :
  ∀
    (hf :
      IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA :=
        ModuleCat.carrier) f),
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
      (CategoryTheory.Functor.map (LightCondensed.forget R) f)
⊢ Epi (X := Functor.obj (LightCondensed.forget R) X_1) (CategoryTheory.Functor.map (LightCondensed.forget R) f)

Tactic:
rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢

Premises used: CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf :
  IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
    f
⊢ IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
    (CategoryTheory.Functor.map (LightCondensed.forget R) f)

Tactic:
(Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mp hf

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, CategoryTheory.Functor.whiskerRight, Iff.mp, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f_1 : X ⟶ Y
X_1 Y_1 : LightCondMod R
f : X_1 ⟶ Y_1
hf :
  IsLocallySurjective (FA := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CA := ModuleCat.carrier)
    f
⊢ IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (LightCondensed.forget R) X_1)
    (CategoryTheory.Functor.map (LightCondensed.forget R) f)

Tactic:
exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.hom).mp hf

Premises used: CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget, Iff.mp, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u
inst : Ring R
X Y : LightCondMod R
f : X ⟶ Y
inst_1 : Epi f
S : LightProfinite
p : Functor.obj (LightCondensed.free R) S.toCondensed ⟶ Y
⊢ Epi (X := Functor.obj (LightCondensed.forget R) X) (CategoryTheory.Functor.map (LightCondensed.forget R) f)

Tactic:
have : Epi ((LightCondensed.forget _).map f) := inferInstance
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
apply :
  Epi (X := Functor.obj (forget R) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)))
    (CategoryTheory.Functor.map (forget R) (c.π.app (Opposite.op 0)))
⊢ Epi (X := Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)) (c.π.app (Opposite.op 0))

Tactic:
apply Functor.epi_of_epi_map (forget R)

Premises used: CategoryTheory.Functor.epi_of_epi_map, LightCondensed.forget
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
change :
  Epi (X :=
    Functor.obj (C := ℕᵒᵖ)
      (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c))) (Opposite.op 0))
    (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))
⊢ Epi (X := Functor.obj (forget R) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) c.pt) (Opposite.op 0)))
    (CategoryTheory.Functor.map (forget R) (c.π.app (Opposite.op 0)))

Tactic:
change Epi (((forget R).mapCone c).π.app ⟨0⟩)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Epi, Opposite.op, CategoryTheory.Functor.mapCone, OfNat.ofNat, CategoryTheory.NatTrans.app, LightCondensed.forget
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
h :
  ∀ (G : ℕᵒᵖ ⥤ LightProfinite),
    (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) →
      EffectiveEpi (X := G.obj (Opposite.op 0)) (Y := limit G) (limit.π G (Opposite.op 0))
hc₁ : IsLimit (F := F ⋙ forget R) (Functor.mapCone (forget R) c)
hF₁ : ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)
⊢ Epi (X :=
    Functor.obj (C := ℕᵒᵖ)
      (Functor.obj (Functor.const ℕᵒᵖ) (Cone.pt (F := F ⋙ forget R) (Functor.mapCone (forget R) c))) (Opposite.op 0))
    (NatTrans.app (Cone.π (Functor.mapCone (forget R) c)) (Opposite.op 0))

Tactic:
apply coherentTopology.epi_π_app_zero_of_epi

Premises used: CategoryTheory.coherentTopology.epi_π_app_zero_of_epi
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ Functor.IsRightAdjoint (D := LightCondMod R) (forget R)

Tactic:
have := (freeForgetAdjunction R).isRightAdjoint
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
this : Functor.IsRightAdjoint (D := LightCondMod R) (forget R)
⊢ IsLimit (F := F ⋙ forget R) (Functor.mapCone (forget R) c)

Tactic:
exact isLimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)

Tactic:
fun _ ↦ (forget R).map_epi _

Premises used: Quiver.Hom.op, CategoryTheory.Functor.map_epi, Nat.le_succ, CategoryTheory.Functor.map, CategoryTheory.homOfLE, CategoryTheory.ObjectProperty.homMk, LightCondensed.forget
-- Module: Mathlib.Condensed.Light.Epi
Goal:
R : Type u_1
inst : Ring R
F : ℕᵒᵖ ⥤ LightCondMod R
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Epi (F.map (homOfLE ⋯).op)
⊢ ∀ (n : ℕ), Epi ((F ⋙ forget R).map (homOfLE ⋯).op)

Tactic:
exact fun _ ↦ (forget R).map_epi _

Premises used: CategoryTheory.Functor.map_epi, LightCondensed.forget
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n_1 : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f n)
n : ℕ
simp : Epi (X := functorObj M N (n + 1)) (functorMap f n)
⊢ Epi ((Functor.ofOpSequence (X := functorObj M N) (functorMap f)).map (homOfLE ⋯).op)

Tactic:
simp only [Nat.succ_eq_add_one, Functor.ofOpSequence_obj, homOfLE_leOfHom,
      Functor.ofOpSequence_map_homOfLE_succ]

Premises used: Nat.succ_eq_add_one, CategoryTheory.Functor.ofOpSequence_obj, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n_1 : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f n)
n : ℕ
⊢ Epi (X := functorObj M N (n + 1)) (functorMap f n)

Tactic:
infer_instance
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
w :
  ∀ (j : Discrete ℕ),
    Eq (α := Functor.obj lim X ⟶ Y.obj j) (CategoryTheory.Functor.map lim f ≫ limit.π Y j)
      (CategoryStruct.comp (Y := limit Y)
        (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
          (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
            (Iso.hom (Pi.isoLimit Y))))
        (limit.π Y j))
⊢ Eq (α := Functor.obj lim X ⟶ Functor.obj lim Y) (CategoryTheory.Functor.map lim f)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))

Tactic:
apply limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n_1 : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
n : ℕ
⊢ Eq (α := Functor.obj lim X ⟶ Y.obj { as := n }) (CategoryTheory.Functor.map lim f ≫ limit.π Y { as := n })
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
        (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
          (Iso.hom (Pi.isoLimit Y))))
      (limit.π Y { as := n }))

Tactic:
simp
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
this :
  Eq (α := Functor.obj lim X ⟶ Functor.obj lim Y) (CategoryTheory.Functor.map lim f)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))
rw :
  Epi (X := Functor.obj lim X) (Y := Functor.obj lim Y)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))
⊢ Epi (X := Functor.obj lim X) (CategoryTheory.Functor.map lim f)

Tactic:
rw [this]
-- Module: Mathlib.Condensed.Light.Epi
Goal:
n : ℕ
R : Type u
inst : Ring R
M N : ℕ → LightCondMod R
f_1 : (n : ℕ) → M n ⟶ N n
inst_1 : ∀ (n : ℕ), Epi (f_1 n)
X Y : Discrete ℕ ⥤ LightCondMod R
f : X ⟶ Y
h : Epi f
this :
  Eq (α := Functor.obj lim X ⟶ Functor.obj lim Y) (CategoryTheory.Functor.map lim f)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))
⊢ Epi (X := limit X) (Y := limit Y)
    (CategoryStruct.comp (Y := ∏ᶜ fun (j : ℕ) ↦ X.obj { as := j }) (Iso.inv (Pi.isoLimit X))
      (CategoryStruct.comp (Y := ∏ᶜ fun (x : ℕ) ↦ Y.obj { as := x }) (Limits.Pi.map fun (x : ℕ) ↦ f.app { as := x })
        (Iso.hom (Pi.isoLimit Y))))

Tactic:
infer_instance
-- Module: Mathlib.Condensed.Light.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
rw : PreservesFiniteProducts F ∧ EqualizerCondition F
⊢ IsSheaf (coherentTopology LightProfinite) F

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition F]

Premises used: CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
-- Module: Mathlib.Condensed.Light.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ 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.Light.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
F : CategoryTheory.Functor.{u, v_1, u + 1, u_1} LightProfiniteᵒᵖ A
inst_1 : PreservesFiniteProducts F
hF : EqualizerCondition F
⊢ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩
-- Module: Mathlib.Condensed.Light.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} LightProfiniteᵒᵖ 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 LightProfinite) (F ⋙ CategoryTheory.forget A (FC := FA) (CC := CA))
⊢ IsSheaf (coherentTopology LightProfinite) 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.Light.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} LightProfiniteᵒᵖ 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 LightProfinite) (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.Light.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} LightProfiniteᵒᵖ 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.Light.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} LightProfiniteᵒᵖ 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.Light.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : LightCondensed.{u_2, v_1, u_1} A
⊢ EqualizerCondition (X.obj (P := IsSheaf (coherentTopology LightProfinite)))

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.Light.Explicit
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
X : LightCondensed.{u_2, v_1, u_1} A
⊢ PreservesFiniteProducts (X.obj (P := IsSheaf (coherentTopology LightProfinite)))

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.Light.Functors
Goal:
⊢ lightProfiniteToLightCondSet.Full

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

Premises used: _private.0.instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet._proof_1
-- Module: Mathlib.Condensed.Light.Functors
Goal:
⊢ lightProfiniteToLightCondSet.Faithful

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

Premises used: _private.0.instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet._proof_1
-- Module: Mathlib.Condensed.Light.Functors
Goal:
J : Type
inst : SmallCategory J
inst_1 : CountableCategory J
⊢ PreservesLimitsOfShape J lightProfiniteToLightCondSet

Tactic:
haveI : Functor.IsRightAdjoint topCatToLightCondSet.{u} :=
    LightCondSet.topCatAdjunction.isRightAdjoint
  haveI : PreservesLimitsOfShape J LightProfinite.toTopCat.{u} :=
    inferInstanceAs (PreservesLimitsOfShape J (lightToProfinite ⋙ Profinite.toTopCat))
  preservesLimitsOfShape_of_natIso lightProfiniteToLightCondSetIsoTopCatToLightCondSet.symm

Premises used: lightProfiniteToLightCondSetIsoTopCatToLightCondSet, CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.Condensed.Light.Functors
Goal:
⊢ PreservesFiniteCoproducts lightProfiniteToLightCondSet

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

Premises used: _private.0.instPreservesFiniteCoproductsLightProfiniteLightCondSetLightProfiniteToLightCondSet._proof_1
-- Module: Mathlib.Condensed.Light.Instances
Goal:
A : Type u'
inst : Category.{u, u'} A
inst_1 : HasLimits.{u, u'} A
inst_2 : HasColimits.{u, u'} A
FA : A → A → Type v
CA : A → Type u
inst_3 : (X Y : A) → FunLike.{v + 1, u + 1, u + 1} (FA X Y) (CA X) (CA Y)
inst_4 : ConcreteCategory A FA (CC := CA)
inst_5 : PreservesFilteredColimits (forget A (FC := FA) (CC := CA))
inst_6 : PreservesLimits (forget A (FC := FA) (CC := CA))
inst_7 : Functor.ReflectsIsomorphisms (forget A (FC := FA) (CC := CA))
⊢ HasSheafify (coherentTopology LightProfinite) A

Tactic:
hasSheafifyEssentiallySmallSite _ _

Premises used: CategoryTheory.hasSheafifyEssentiallySmallSite