mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones (curry.obj G)
Q : (j : J) → IsLimit (D.obj j)
c : Cone G
x✝¹ j' : J
x✝ : x✝¹ ⟶ j'
⊢ ∀ (j : K),
    (((const J).obj c.pt).map x✝ ≫
          (Q j').lift { pt := c.pt, π := { app := fun k ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
        (D.obj j').π.app j =
      ((Q x✝¹).lift { pt := c.pt, π := { app := fun k ↦ c.π.app (x✝¹, k), naturality := ⋯ } } ≫ D.conePoints.map x✝) ≫
        (D.obj j').π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ 𝟙 c.pt

Tactic:
simp only [Category.comp_id]

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k)
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones (curry.obj G)
Q : (j : J) → IsColimit (D.obj j)
c : Cocone G
j x✝¹ : J
x✝ : j ⟶ x✝¹
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        D.coconePoints.map x✝ ≫ (Q x✝¹).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (x✝¹, k), naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫
        (Q j).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j, k), naturality := ⋯ } } ≫ ((const J).obj c.pt).map x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.right
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
d✝ : J₂
c : J₁
s✝ s'✝ : hf.functor.obj c ⟶ d✝
⊢ ∃ c' t, hf.functor.map t ≫ s✝ = hf.functor.map t ≫ s'✝

Tactic:
exact ⟨ c, 𝟙 _, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G✝ : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)

Tactic:
let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G✝ : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun j ↦ limit.isLimit (F.obj j)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
φ : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N
⊢ ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM),
    (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ)) (r • m) =
      r • (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ)) m

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
⊢ ∀ (x y : ModuleColimit hcR hcM),
    ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) (x + y) =
      ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) x + ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j : J
⊢ c'.ι.app j ≫
      (fun g ↦
          hc'.desc
            { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } })
        ((fun f ↦
            hc.desc
              { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } })
          f) =
    c'.ι.app j ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j : J
⊢ c.ι.app j ≫
      (fun f ↦
          hc.desc
            { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } })
        ((fun g ↦
            hc'.desc
              { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } })
          g) =
    c.ι.app j ≫ g

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j : J
⊢ (fun g ↦
          hc'.lift
            { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } })
        ((fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } })
          f) ≫
      c'.π.app j =
    f ≫ c'.π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j : J
⊢ (fun f ↦
          hc.lift
            { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } })
        ((fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } })
          g) ≫
      c.π.app j =
    g ≫ c.π.app j

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₀₁₁' : G₁'₁ ⋙ G₁₀ ≅ G₁₀
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
h : e₀₁₁' = isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
subst h
  ext X₀
  simp [leftAdjointCompIso_hom_app, leftAdjointIdIso_hom_app,
    ← Functor.map_comp_assoc, -Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
x : ↑(M.obj (F.op.obj X))
⊢ (ConcreteCategory.hom (M.map (𝟙 (F.op.obj X)))) x =
    (ModuleCat.Hom.hom
        ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))))
      x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝¹.obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊤ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊥ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊥

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : ↑(M.obj (F.op.obj X✝))
⊢ (ConcreteCategory.hom (M.map (F.op.map f ≫ F.op.map g))) x =
    (ModuleCat.Hom.hom
        (M.map (F.op.map f) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                    (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
              (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))))
      x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
i : IsIso f
⊢ Sieve.generate (Presieve.singleton f) = ⊤

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y✝ Z : C
g✝ : Y✝ ⟶ Z
f : Z ⟶ X
hf : S f
Y W : C
h : Y ⟶ W
g : W ⟶ Z
hg : Ti f hf g
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ (X : C), ⊤ ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S R : Sieve X✝
J : GrothendieckTopology C
X Y : C
f : Sieve X
⊢ ∀ (f_1 : Y ⟶ X), f ∈ Set.univ → Sieve.pullback f_1 f ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ Set.univ → ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ Set.univ) → R ∈ Set.univ

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : J = ⊤
⊢ ∀ (X : C), ⊥ ∈ ⊤ X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (f ≫ inv g) ≫ g = 𝟙 Y ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯ ≫ pullback.snd g f = 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑(S.pullback (𝟙 X))).arrows f ↔ (↑S).arrows f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝¹ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y✝ Z : C
S : J.Cover X
f✝ : Z ⟶ Y✝
g : Y✝ ⟶ X
Y : C
f : Y ⟶ Z
⊢ (↑(S.pullback (f✝ ≫ g))).arrows f ↔ (↑((S.pullback g).pullback f✝)).arrows f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ IsSheafFor P S.arrows

Tactic:
have gRS : ⇑(generate R) ≤ S := by
      apply giGenerate.gc.monotone_u
      rwa [generate_le_iff]

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
gRS : (generate R).arrows ≤ S.arrows
⊢ IsSheafFor P S.arrows
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ F.hom.1 ≫ g₂.obj.hom = 𝟙 (unop (op g₁.obj.left)) ≫ g₁.obj.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ F.map f₁ = 𝟙 (F.obj X) ≫ F.map f₁

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : D
g₁ : x ⟶ G.obj X
X' : C
f₂ : X' ⟶ X✝
g₂ : X ⟶ F.obj X'
h₁ : R f₂
⊢ g₁ ≫ G.map (g₂ ≫ F.map f₂) = (g₁ ≫ G.map g₂) ≫ (F ⋙ G).map f₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
R : Presieve X
f : Y ⟶ X
h : R f
⊢ F.map f = 𝟙 (F.obj Y) ≫ F.map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
f : Y ⟶ F.obj X
x✝ : map F R f
Y✝ : C
u : Y✝ ⟶ X
hu : R u
⊢ F.map u = eqToHom ⋯ ≫ F.map u

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
⊢ singleton f f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ (fun x ↦ x f ⋯) ((fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) x) = x

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
S R✝ : Sieve X
R : Presieve X
Y Z W : C
g : Y ⟶ W
f : W ⟶ X
hf : R f
h : Z ⟶ Y
⊢ (h ≫ g) ≫ f = h ≫ g ≫ f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ generate R = ⊤

Tactic:
← id_mem_iff_eq_top

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ (generate R).arrows (𝟙 X)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
R : Presieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
hf : R f
⊢ section_ f ≫ f = 𝟙 X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ S.arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Y : I → C
f : (i : I) → Y i ⟶ X
i : I
⊢ 𝟙 (Y i) ≫ f i = f i

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
Y : C
f : Over S
hf : R f.hom
⊢ 𝟙 { obj := f, property := hf }.obj.left ≫ f.hom = { obj := f, property := hf }.obj.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ a ≫ f i = (a ≫ f i ≫ e.inv) ≫ e.hom

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (Q.map g.op)) ((ConcreteCategory.hom (f.app (op X))) t) = x.map f g hg

Tactic:
dsimp [FamilyOfElements.map]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (Q.map g.op)) ((ConcreteCategory.hom (f.app (op X))) t) =
    (ConcreteCategory.hom (f.app (op Y))) (x g hg)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map f''

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R✝ : Sieve X✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ g ≫ β ≫ F.map α = (g ≫ β) ≫ F.map α

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ f = 𝟙 X ≫ (𝟭 C).map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Sieve X
V : C
f : V ⟶ X
h : R.arrows f
⊢ F.map f = 𝟙 (F.obj V) ≫ F.map f

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ iYX = e.counitInv.app Y ≫ e.functor.map (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

Tactic:
Sieve.mem_functorPushforward_iff_of_full

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ (∃ g, F.map g = F.map f ∧ R.arrows g) ↔ R.arrows f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
X : Cᵒᵖ
a : (shrinkYoneda.{w, v₁, u₁}.obj X✝).obj X
⊢ a ∈ (shrinkFunctor.{w, v₁, u₁} S).obj X ↔
    (shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm) a ∈ (shrinkFunctor.{max w' w, v₁, u₁} S).obj X

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y✝ Z : C
f : Y✝ ⟶ X
S R : Sieve X
Y : Cᵒᵖ
⊢ ∀ (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj Y),
    a ∈ (shrinkFunctor.{v₁, v₁, u₁} S).obj Y ↔ S.arrows (shrinkYonedaObjObjEquiv a)

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
X✝ : Sheaf J A
m✝ : X✝ ⟶ terminal J hX
x✝ : Cᵒᵖ
⊢ m✝.hom.app x✝ = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X✝.obj }.hom.app x✝

Tactic:
simpa using! hX.hom_ext _ _

Goal state after: