mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
⊢ ∀ {X_1 Y : (J.Cover X)ᵒᵖ} (f : X_1 ⟶ Y),
    (J.diagram P X ⋙ F).map f ≫
        ((isLimitOfPreserves F (limit.isLimit ((unop Y).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop Y).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop Y)).symm).hom =
      ((isLimitOfPreserves F (limit.isLimit ((unop X_1).index P).multicospan)).conePointUniqueUpToIso
              (limit.isLimit (((unop X_1).index P).multicospan ⋙ F)) ≪≫
            HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop X_1)).symm).hom ≫
        (J.diagram (P ⋙ F) X).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
E : Type u_2
inst✝³ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝² : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝¹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).Arrow
⊢ (J.diagramCompIso F P X).hom.app W ≫ Multiequalizer.ι ((unop W).index (P ⋙ F)) i =
    F.map (Multiequalizer.ι ((unop W).index P) i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
⊢ (J.plusObj P ⋙ F).obj X ≅ (J.plusObj (P ⋙ F)).obj X

Tactic:
by

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 G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
⊢ sheafify J G ≤ G'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Presheaf.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImage f ≫ imageι f = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono ((sheafToPresheaf J (Type w)).map (Sheaf.imageι f))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (II.r.g₁ ≫ II.fst.toMiddleHom) ≫ { Y := II.fst.middle, f := II.fst.fromMiddleHom, hf := ⋯ }.f =
    (II.r.g₂ ≫ II.snd.toMiddleHom) ≫ { Y := II.snd.middle, f := II.snd.fromMiddleHom, hf := ⋯ }.f

Tactic:
by

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 u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
⊢ IsSheafFor P (Sieve.bind U.arrows B).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Epi (Sheaf.toImage f)

Tactic:
by

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 u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
⊢ (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
⊢ ∀ (I : (S.bind T).Relation),
    (ConcreteCategory.hom (P.map I.r.g₁.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) I.fst) =
      (ConcreteCategory.hom (P.map I.r.g₂.op)) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) I.snd)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ (imageMonoFactorization f).I ⟶ I.I

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ { hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) } ≫ I.m = (imageMonoFactorization f).m

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁹ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁸ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P✝ P : Cᵒᵖ ⥤ D
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (whiskeringLeft Cᵒᵖ D E).obj (J.sheafify P) ≅ (whiskeringLeft Cᵒᵖ D E).obj P ⋙ J.sheafification E

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.sheafification D ⋙ (whiskeringRight Cᵒᵖ D E).obj F ≅ (whiskeringRight Cᵒᵖ D E).obj F ⋙ J.sheafification E

Tactic:
by

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 u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S) = Sieve.pullback f R

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv

Tactic:
by

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 u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
⊢ IsSheafFor P S.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : F ⊣ sheafToPresheaf J A
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J_1 : Type) [inst : SmallCategory J_1] [FinCategory J_1],
    PreservesLimitsOfShape J_1 (sheafToPresheaf J A).leftAdjoint

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
⊢ sheafifyMap J (𝟙 P) = 𝟙 (sheafify J P)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ sheafifyMap J (η ≫ γ) = sheafifyMap J η ≫ sheafifyMap J γ

Tactic:
by

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP }) ≫
      (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { obj := P, property := hP }) =
    𝟙 (sheafify J P)

Tactic:
← (sheafificationAdjunction J D).inv_counit_map (X := ⟨P, hP⟩)

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP }) ≫
      inv ((sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { obj := P, property := hP })) =
    𝟙 (sheafify J P)
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (toSheafify J P)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ((sheafificationAdjunction J D).counit.app P).hom = sheafifyLift J (𝟙 P.obj) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toSheafify J P ≫ sheafifyLift J η hQ = η

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : sheafify J P ⟶ Q
⊢ toSheafify J P ≫ γ = η → γ = sheafifyLift J η hQ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom = J.toSheafify (P ⋙ F)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ (isoSheafify J hP).inv = sheafifyLift J (𝟙 P) hP

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ η = γ

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
⊢ J.toSheafify (P ⋙ F) ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify P) F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ sheafifyMap J η ≫ sheafifyLift J γ hR = sheafifyLift J (η ≫ γ) hR

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
F P Q : Cᵒᵖ ⥤ D
a : F ⟶ P
hP : Presheaf.IsSheaf J P
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ toSheafify J F ≫ sheafifyLift J a hP ≫ η = a ≫ η

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ { hom := (isoSheafify J ⋯).hom } ≫ { hom := (isoSheafify J ⋯).inv } = 𝟙 P

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ { hom := (isoSheafify J ⋯).inv } ≫ { hom := (isoSheafify J ⋯).hom } = 𝟙 ((presheafToSheaf J D).obj P.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹² : Category.{v_1, u_1} D
E : Type u_2
inst✝¹¹ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝¹⁰ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁹ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁸ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝⁵ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
FD : D → D → Type u_3
CD : D → Type u_4
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
inst✝² : PreservesLimitsOfSize.{max v u, max v u, v_1, u_4, u_1, u_4 + 1} (forget D)
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
⊢ (J.sheafifyCompIso F P).inv = J.sheafifyLift (whiskerRight (J.toSheafify P) F) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ sheafifyLift J (𝟙 P) hP ≫ toSheafify J P = 𝟙 (sheafify J P)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
⊢ ∀ {X Y : Sheaf J D} (f : X ⟶ Y),
    (𝟭 (Sheaf J D)).map f ≫ (sheafificationIso Y).hom =
      (sheafificationIso X).hom ≫ (sheafToPresheaf J D ⋙ presheafToSheaf J D).map f

Tactic:
by

Goal state after:
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
k : K
⊢ ∀ (b : W.shape.R),
    (S.ι (W.shape.fst b) ≫ (E.π.app k).app (op (W.shape.fst b).Y)) ≫ (W.index (F.obj k).obj).fst b =
      (S.ι (W.shape.snd b) ≫ (E.π.app k).app (op (W.shape.snd b).Y)) ≫ (W.index (F.obj k).obj).snd b

Tactic:
by

Goal state after: