mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ (homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g) =
    (ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)

Tactic:
refine Prod.ext ?_ ?_

Goal state after:
case refine_1
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).1 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).1

case refine_2
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
F G : Cᵒᵖ ⥤ Type v
X Y : C
h₁ : F.RepresentableBy X
h₂ : G.RepresentableBy Y
I W : C
f : I ⟶ W
g : W ⟶ X ⊗ Y
⊢ ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) (f ≫ g)).2 =
    ((ConcreteCategory.hom ((F ⊗ G).map f.op)) ((homEquivToProd.trans (h₁.homEquiv.prodCongr h₂.homEquiv)) g)).2
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
X Y : C ⥤ Type u
⊢ (HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
      colimit.pre (X ⊠ Y) (Functor.diag C) ≫
        (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom =
    CartesianMonoidalCategory.prodComparison colim X Y

Tactic:
apply colimit.hom_ext

Goal state after:
C : Type u
inst✝ : SmallCategory C
X Y : C ⥤ Type u
⊢ ∀ (j : C),
    colimit.ι ((tensor (C ⥤ Type u)).obj (X, Y)) j ≫
        (HasColimit.isoOfNatIso ((externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom ≫
          colimit.pre (X ⊠ Y) (Functor.diag C) ≫
            (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y (curriedTensor (Type u))).hom =
      colimit.ι ((tensor (C ⥤ Type u)).obj (X, Y)) j ≫ CartesianMonoidalCategory.prodComparison colim X Y
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ FinallySmall J

Tactic:
suffices Functor.Final (ObjectProperty.ι (· ∈ s)) from
    finallySmall_of_final_of_essentiallySmall (ObjectProperty.ι (· ∈ s))

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ (ObjectProperty.ι fun x ↦ x ∈ s).Final
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
⊢ Nonempty (IsColimit (G.flip.mapCocone₂ c₁ c₂))

Tactic:
by
    constructor
    let E₀ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G).flip :=
      Iso.refl _
    let E₁ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        Prod.swap _ _ ⋙ uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) :=
      E₀ ≪≫ uncurryObjFlip _
    refine IsColimit.precomposeInvEquiv E₁ _ ?_
    apply IsColimit.ofWhiskerEquivalence (e := Prod.braiding _ _)
    refine IsColimit.equivOfNatIsoOfIso (Iso.refl _) (G.mapCocone₂ c₂ c₁) _ ?_ |>.toFun <|
      isColimitOfPreserves₂ G hc₂ hc₁
    exact Cocone.ext (Iso.refl _) (fun ⟨j₁, j₂⟩ ↦ by simp [E₁, E₀])

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

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)

Tactic:
obtain ⟨τ₁₂₃, rfl⟩ := (conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)).surjective τ₁₂₃

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₁₃ ≫ whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)) τ₁₂₃) G₁₀)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case h₁
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.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f

Tactic:
· simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ sInf ((fun J ↦ J.coverings) '' T) X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ sInf ((fun J ↦ J.coverings) '' T) Y
⊢ S.bind Ti ∈ sInf ((fun J ↦ J.coverings) '' T) X

Tactic:
simp only [sInf_apply, Set.iInf_eq_iInter, Set.iInter_coe_set, Set.mem_image,
        Set.iInter_exists, Set.biInter_and', Set.iInter_iInter_eq_right, Set.mem_iInter] at hS hTi ⊢

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : ∀ i ∈ T, S ∈ i.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), ∀ i ∈ T, Ti f H ∈ i.coverings Y
⊢ ∀ i ∈ T, S.bind Ti ∈ i.coverings X
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)
⊢ (fun x Z g hg ↦ (ConcreteCategory.hom (P.map (eqToHom ⋯).op)) x) ((fun x ↦ x f ⋯) x) = x

Tactic:
by ext _ _ ⟨rfl⟩; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
b✝ : (Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' }
x✝ : P.obj (op X)
⊢ (ConcreteCategory.hom ((forkMap P S.arrows ≫ firstMap P S) ≫ Pi.π (fun f ↦ P.obj (op f.snd.fst)) b✝)).toFun x✝ =
    (ConcreteCategory.hom ((forkMap P S.arrows ≫ secondMap P S) ≫ Pi.π (fun f ↦ P.obj (op f.snd.fst)) b✝)).toFun x✝

Tactic:
simp [firstMap, secondMap, forkMap]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x f hf) = x f hf

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f

Tactic:
· simp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ 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
U V : Cᵒᵖ
f : U ⟶ V
⊢ (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.map f ≫ (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom =
    (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom ≫ S.functor.map f

Tactic:
by
      dsimp [Equiv.subtypeEquiv_apply]
      ext
      simp [shrinkYonedaObjObjEquiv_obj_map]

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

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
e_1✝ :
  (multiequalizer ((unop S).index P) ⟶ colimit (J.diagram P (unop X))) =
    ((J.diagram P (unop X)).obj S ⟶ colimit (J.diagram P (unop X)))
I : (unop (op (unop S))).shape.L
⊢ (Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) (multiequalizer ((unop S).index P))
          (fun I ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯ ≫
        Multiequalizer.lift ((unop S).index P) (multiequalizer (((unop S).pullback (𝟙 (unop X))).index P))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback (𝟙 (unop X))).index P) (I.map e.inv)) ⋯) ≫
      Multiequalizer.ι ((unop S).index P) I =
    𝟙 (multiequalizer ((unop S).index P)) ≫ Multiequalizer.ι ((unop S).index P) I

Tactic:
simp only [Multiequalizer.lift_ι, Category.id_comp, Category.assoc]

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
e_1✝ :
  (multiequalizer ((unop S).index P) ⟶ colimit (J.diagram P (unop X))) =
    ((J.diagram P (unop X)).obj S ⟶ colimit (J.diagram P (unop X)))
I : (unop (op (unop S))).shape.L
⊢ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I e.inv).base = Multiequalizer.ι ((unop S).index P) I
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
t : P.obj (op X)
ht : x.sieveExtend.IsAmalgamation t
⊢ x.IsAmalgamation t

Tactic:
simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤

Tactic:
← arrows_top,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P ⊤.arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
apply isSheafFor_singleton_iso

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
hP : IsSheaf J P
X : C
S : J.Cover X
⊢ IsLimit (S.multifork P)

Tactic:
Presheaf.isSheaf_iff_multifork

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ IsLimit (S.multifork P)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor ((Over.map p).op ⋙ P) (Sieve.ofArrows Z g).arrows ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows

Tactic:
← isSheafFor_iff_generate,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ IsSheafFor ((Over.map p).op ⋙ P) (ofArrows Z g) ↔
    IsSheafFor P (Sieve.pullback e.inv (Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g))).arrows
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ range p ≤ G

Tactic:
by
  rw [← image_top, image_le_iff]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ s ∈ G.obj U

Tactic:
suffices ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).1 = s by
    rw [← this]
    exact ((hG _ hs).amalgamate _ (G.family_of_elements_compatible s)).2

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) = s
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : Nonempty (IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj X) R) ⋯))
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))

Tactic:
replace q := Classical.choice q

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj X) R) ⋯)
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (P' ⋙ coyoneda.obj (op U)) S.arrows

Tactic:
rw [Equalizer.Presieve.sheaf_condition]

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
⊢ Nonempty (IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj (op U)) S.arrows) ⋯))
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
Presheaf.isSheaf_iff_multifork

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork (P ⋙ F)))
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt

Tactic:
Presheaf.isSheaf_iff_multifork

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ IsClosed X ↔ ∀ (j : J), IsClosed (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff_of_isColimit _ hc,
    Functor.const_obj_obj, Set.preimage_compl]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom
        (ofHom
          { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
            continuous_toFun := ⋯ }))
      x

Tactic:
refine Prod.ext ?_ ?_

Goal state after:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).1 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).1

case refine_2
J : Type v
inst✝ : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : ↑S.pt
⊢ ((ConcreteCategory.hom m) x).2 =
    ((ConcreteCategory.hom
          (ofHom
            { toFun := fun s ↦ ((ConcreteCategory.hom (BinaryFan.fst S)) s, (ConcreteCategory.hom (BinaryFan.snd S)) s),
              continuous_toFun := ⋯ }))
        x).2
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : ↑(W ⨯ X)
⊢ (∃ y_1, (ConcreteCategory.hom f) y_1 = (ConcreteCategory.hom (prod.fst ≫ f)) y) ∧
    ∃ y_1, (ConcreteCategory.hom g) y_1 = (ConcreteCategory.hom (prod.map f g ≫ prod.snd)) y

Tactic:
Limits.prod.map_snd,

Goal state after:
case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : ↑(W ⨯ X)
⊢ (∃ y_1, (ConcreteCategory.hom f) y_1 = (ConcreteCategory.hom (prod.fst ≫ f)) y) ∧
    ∃ y_1, (ConcreteCategory.hom g) y_1 = (ConcreteCategory.hom (prod.snd ≫ g)) y
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)).hom ≫ pullback.fst (c.inj i) (c.inj j) =
    hY.to (X i)

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)).hom ≫ pullback.snd (c.inj i) (c.inj j) =
    hY.to (X j)

Tactic:
· simp

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)).hom ≫ pullback.snd (c.inj i) (c.inj j) =
    hY.to (X j)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
X : ι → C
inst✝¹ : CoproductDisjoint X
c : Cofan X
hc : IsColimit c
Y : C
hY : IsInitial Y
i j : ι
inst✝ : HasPullback (c.inj i) (c.inj j)
hij : i ≠ j
⊢ (hY.uniqueUpToIso (IsInitial.ofCoproductDisjointOfIsColimit hij hc)).hom ≫ pullback.snd (c.inj i) (c.inj j) =
    hY.to (X j)

Tactic:
· simp

Goal state after: