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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
⊢ R.arrows f → (functorPullback F S).arrows f

Tactic:
hf

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X✝
hf : R.arrows f
⊢ (functorPullback F S).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 : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)

Tactic:
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:
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
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
⊢ S.arrows f → (functorPushforward F (functorPullback F S)).arrows f

Tactic:
hf

Goal state after:
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
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
S : Sieve (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPushforward F (functorPullback F S)).arrows f
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
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ∀ (hf : S.arrows f),
    (fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Z (g ≫ f) ⋯ =
      (ConcreteCategory.hom (F.map g.op))
        ((fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Y f hf)

Tactic:
hf

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ (fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Z (g ≫ f) ⋯ =
    (ConcreteCategory.hom (F.map g.op))
      ((fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩) Y f hf)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
⊢ ∀ (h : R f), (ConcreteCategory.hom (P.map f.op)) t = x f h

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf
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:
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
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type t
inst✝ : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₂
⊢ z₁ = z₂

Tactic:
by
  apply Limits.Types.limit_ext
  rintro ⟨i⟩
  exact h i

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
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂
⊢ z₁ = z₂

Tactic:
by
  apply Limits.Types.limit_ext
  rintro ⟨i⟩
  exact h i

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
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑x f✝ ⋯ = ↑x f✝ hf✝

Tactic:
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 : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
Y Z : C
t : R.obj (Opposite.op Y)
g : Z ⟶ Y
⊢ (hom (f.app (Opposite.op Z))) ((hom (R.map g.op)) t) = g ≫ (hom (f.app (Opposite.op Y))) t

Tactic:
simp

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
Y : Cᵒᵖ
u : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hu : u ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ (ConcreteCategory.hom (((shrinkFunctor.{w, v₁, u₁} S).ι ≫ g).app Y)).toFun ⟨u, hu⟩ =
    (ConcreteCategory.hom (g.app (op (unop Y)))) (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv u))

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y✝ : C
g : Y✝ ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y✝
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
W : C
u : W ⟶ Y✝
Y : C
i : ι
v : W ⟶ X i
heq : v ≫ f i = u ≫ g
⊢ ⋯.lift u v ⋯ ≫ p₁ i = u

Tactic:
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✝
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:
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
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ULift.{w', w} ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ (hom ((shrinkYoneda.{max w w', v₁, u₁}.obj X).map f.unop.op))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down)) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))

Tactic:
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:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝¹ : Cᵒᵖ
a✝ : unop a✝¹ ⟶ X
⊢ (∀ (b_1 : shrinkYonedaObjObjEquiv.symm a✝ ∈ {f | S.arrows (shrinkYonedaObjObjEquiv f)}),
      (ConcreteCategory.hom (b.app a✝¹)) a✝ = (ConcreteCategory.hom (a.app a✝¹)) ⟨a✝, ⋯⟩) ↔
    ∀ (b_1 : S.arrows a✝), (ConcreteCategory.hom (b.app a✝¹)) a✝ = (ConcreteCategory.hom (a.app a✝¹)) ⟨a✝, b_1⟩

Tactic:
simp

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

Goal state before:
pp: 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
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ ((J.diagram P Y).map f ≫
        Multiequalizer.lift ((unop ((J.pullback f✝).op.obj T)).index P) ((J.diagram P Y).obj T)
          (fun I ↦ Multiequalizer.ι ((unop T).index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I =
    (Multiequalizer.lift ((unop ((J.pullback f✝).op.obj S)).index P) ((J.diagram P Y).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        ((J.pullback f✝).op ⋙ J.diagram P X).map f) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I

Tactic:
simp

Goal state after:
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
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ Multiequalizer.ι ((unop S).index P) ((Cover.Arrow.base I).map f.unop) =
    Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I ((J.pullback f✝).map f.unop)).base
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: 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)
X : C
P : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (𝟙 P) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i =
    (𝟙 (J.diagram P X)).app x✝ ≫ Multiequalizer.ι ((unop x✝).index P) i

Tactic:
simp

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

Goal state before:
pp: 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)
inst✝ : Preadditive D
X : C
P Q : Cᵒᵖ ⥤ D
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans 0 X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i =
    NatTrans.app 0 x✝ ≫ Multiequalizer.ι ((unop x✝).index Q) i

Tactic:
simp

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

Goal state before:
pp: 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 Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
X : C
x✝ : (J.Cover X)ᵒᵖ
i : (unop x✝).shape.L
⊢ (J.diagramNatTrans (η ≫ γ) X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i =
    (J.diagramNatTrans η X ≫ J.diagramNatTrans γ X).app x✝ ≫ Multiequalizer.ι ((unop x✝).index R) i

Tactic:
simp

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
Y : C
⊢ (ConcreteCategory.hom (P.map (𝟙 X).op)) (x (𝟙 X) ⋯) = x (𝟙 X) ⋯

Tactic:
simp

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

Goal state before:
pp: case e'_2.mk.e_6
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)))
Y✝ : C
f✝ : Y✝ ⟶ unop X
hf✝ : (↑(unop (op (unop S)))).arrows f✝
⊢ { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ 𝟙 (unop X) = f✝

Tactic:
simp

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

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
⊢ ∀ (h : S.arrows f),
    (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
        (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯) =
      z f h

Tactic:
hf

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
      (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯) =
    z f hf
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
x : unop (op X)
Y' : C
f : Y' ⟶ Y
⊢ S.arrows f →
    (ConcreteCategory.hom (P.map f.op)) ((ConcreteCategory.hom y) x) =
      (ConcreteCategory.hom (P.map f.op))
        ((ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x)

Tactic:
hf

Goal state after:
case mpr.refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
y : (P ⋙ coyoneda.obj (op X)).obj (op Y)
hy : z.IsAmalgamation y
x : unop (op X)
Y' : C
f : Y' ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) ((ConcreteCategory.hom y) x) =
    (ConcreteCategory.hom (P.map f.op))
      ((ConcreteCategory.hom (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)) x)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a.mk.e_6
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 Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
Y✝ : C
f✝ : Y✝ ⟶ unop Z
hf✝ : (↑(unop (op (((unop S).pullback f.unop).pullback g.unop)))).arrows f✝
⊢ f✝ ≫ g.unop ≫ f.unop = (f✝ ≫ g.unop) ≫ f.unop

Tactic:
simp

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

Goal state before:
pp: 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
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
I : (unop ((J.pullback f.unop).op.obj j✝)).shape.L
⊢ (Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index P) ((J.diagram P (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagramNatTrans η (unop Y)).app ((J.pullback f.unop).op.obj j✝)) ≫
      Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j✝)).index Q) I =
    ((J.diagramNatTrans η (unop X)).app j✝ ≫
        Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj j✝)).index Q) ((J.diagram Q (unop X)).obj j✝)
          (fun I ↦ Multiequalizer.ι ((unop j✝).index Q) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj j✝)).index Q) I

Tactic:
simp

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

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
⊢ (Sieve.pullback j S).arrows f →
    (ConcreteCategory.hom (P.map f.op))
        ((ConcreteCategory.hom (P.map j.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯)) =
      (ConcreteCategory.hom (P.map f.op)) (x j hj)

Tactic:
hf

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ (ConcreteCategory.hom (P.map f.op))
      ((ConcreteCategory.hom (P.map j.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯)) =
    (ConcreteCategory.hom (P.map f.op)) (x j hj)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ x (f ≫ j) ⋯ = (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x (f ≫ j) ⋯)

Tactic:
simp

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

Goal state before:
pp: 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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j✝ : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) j✝ ≫ colimMap (𝟙 (J.diagram P (unop x✝))) =
    colimit.ι (J.diagram P (unop x✝)) j✝ ≫
      𝟙
        ({ obj := fun X ↦ colimit (J.diagram P (unop X)),
              map := fun {X Y} f ↦
                colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
              map_id := ⋯, map_comp := ⋯ }.obj
          x✝)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
i : {Z : C} → (g : Z ⟶ B) → ofArrows X π g → I
h : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), X (i g hg) = Z
h' : ∀ {Z : C} (g : Z ⟶ B) (hg : ofArrows X π g), g = eqToHom ⋯ ≫ π (i g hg)
j : I
⊢ (ConcreteCategory.hom (P.map (𝟙 (X j)).op)) (x j) = x j

Tactic:
simp

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

Goal state before:
pp: case h.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
Y : C
f : Y ⟶ X
⊢ ∀ (h : S.arrows f), (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op E)).map f.op)) (hh.lift K) = x f h

Tactic:
hf

Goal state after:
case h.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op E)).map f.op)) (hh.lift K) = x f hf
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
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 Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
I : (unop (op ((J.pullback f.unop).obj ⊤))).shape.L
⊢ P.map f ≫
      Multiequalizer.lift (⊤.index P) (P.obj Y) (fun I ↦ P.map I.f.op) ⋯ ≫
        (J.diagram P (unop Y)).map e.op ≫ Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I =
    Multiequalizer.lift (⊤.index P) (P.obj X) (fun I ↦ P.map I.f.op) ⋯ ≫
      Multiequalizer.lift (((J.pullback f.unop).obj ⊤).index P) ((J.diagram P (unop X)).obj (op ⊤))
          (fun I ↦ Multiequalizer.ι (⊤.index P) { Y := I.Y, f := I.f ≫ f.unop, hf := ⋯ }) ⋯ ≫
        Multiequalizer.ι (((J.pullback f.unop).obj ⊤).index P) I

Tactic:
simp

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

Goal state before:
pp: 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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
x✝ : Cᵒᵖ
I : ⊤.shape.L
⊢ (η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I ↦ Q.map I.f.op) ⋯) ≫
      Multiequalizer.ι (⊤.index Q) I =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I ↦ P.map I.f.op) ⋯ ≫
        (J.diagramNatTrans η (unop x✝)).app (op ⊤)) ≫
      Multiequalizer.ι (⊤.index Q) I

Tactic:
simp

Goal state after: