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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) f hf = x f hf

Tactic:
simpa [Iso.toEquiv, forkMap] using q _ _

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
⊢ Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))

Tactic:
by
  rw [Types.type_equalizer_iff_unique,
    ← Equiv.forall_congr_right (firstObjEqFamily P (S : Presieve X)).toEquiv.symm]
  simp_rw [← compatible_iff]
  conv => enter [2, a, 1, 1, 2]; rw [(firstObjEqFamily P S.arrows).toEquiv_symm_apply]
  simp only [Iso.inv_hom_id_apply]
  apply forall₂_congr
  intro x _
  apply existsUnique_congr
  intro t
  rw [Equiv.eq_symm_apply]
  constructor
  · intro q
    ext Y f hf
    simpa [Iso.toEquiv, forkMap] using q _ _
  · intro q Y f hf
    rw [← q]
    simp [Iso.toEquiv, forkMap]

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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
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 : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : R f
⊢ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) f hf = x f hf

Tactic:
simpa [Iso.toEquiv, forkMap] using q _ _

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
t : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ (ConcreteCategory.hom
          ((shrinkFunctor.{w, v₁, u₁} S).toFunctor.map g ≫ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯)).toFun
      ⟨f, hf⟩ =
    (ConcreteCategory.hom ((↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯) ≫ F.map g)).toFun ⟨f, hf⟩

Tactic:
dsimp

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 : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ ↑t (shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g)) f)) ⋯ =
    (ConcreteCategory.hom (F.map g)) (↑t (shrinkYonedaObjObjEquiv 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
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑((fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩)
          ((fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ }) x))
      f✝ hf✝ =
    ↑x f✝ hf✝

Tactic:
dsimp

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
x : { x // x.Compatible }
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : S.arrows f✝
⊢ ↑x (shrinkYonedaObjObjEquiv (shrinkYonedaObjObjEquiv.symm f✝)) ⋯ = ↑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
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
⊢ ((shrinkFunctor.{w, v₁, u₁} S).toFunctor ⋙ CategoryTheory.uliftFunctor.{w', w}).map f ≫
      (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom =
    (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom ≫
      (shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor.map f

Tactic:
dsimp

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
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
⊢ (↾fun x ↦ { down := ⟨(hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map f)) ↑x.down, ⋯⟩ }) ≫
      (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom =
    (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom ≫
      ↾fun x ↦ ⟨(hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f)) ↑x, ⋯⟩
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
⊢ (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (shrinkYonedaIsoYoneda.app X).homFromEquiv.symm b =
      S.shrinkFunctorIsoFunctor.homFromEquiv.symm a ↔
    S.functorInclusion ≫ b = a

Tactic:
dsimp

Goal state after:
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
⊢ (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b =
      S.shrinkFunctorIsoFunctor.hom ≫ a ↔
    S.functorInclusion ≫ b = a
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
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap (J.diagramPullback P (𝟙 X).unop) ≫ colimit.pre (J.diagram P (unop X)) (J.pullback (𝟙 X).unop).op =
    colimit.ι (J.diagram P (unop X)) S ≫ 𝟙 (colimit (J.diagram P (unop X)))

Tactic:
dsimp

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
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap (J.diagramPullback P (𝟙 (unop X))) ≫ colimit.pre (J.diagram P (unop X)) (J.pullback (𝟙 (unop X))).op =
    colimit.ι (J.diagram P (unop X)) S ≫ 𝟙 (colimit (J.diagram P (unop X)))
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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op = y ≫ P.map { Y := Z, f := g ≫ f i, hf := ⋯ }.f.op

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ x ≫ P.map ((f i).op ≫ g.op) = y ≫ P.map ((f i).op ≫ g.op)
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) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop X)).map e.inv.op) ≫
      Multiequalizer.ι ((unop (op (unop S))).index P) I =
    𝟙 ((J.diagram P (unop X)).obj S) ≫ Multiequalizer.ι ((unop (op (unop S))).index P) I

Tactic:
dsimp

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.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
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
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
    colimit.ι (J.diagram P (unop X)) S ≫
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op

Tactic:
dsimp

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
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap (J.diagramPullback P (g.unop ≫ f.unop)) ≫
        colimit.pre (J.diagram P (unop Z)) (J.pullback (g.unop ≫ f.unop)).op =
    colimit.ι (J.diagram P (unop X)) S ≫
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ (fun t ↦ x₂.IsAmalgamation t) (e (hP₁.amalgamate x₁ hx₁))

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
⊢ x₂.IsAmalgamation (e (hP₁.amalgamate x₁ hx₁))
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (Meq.equiv P (unop ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (Meq.equiv P (unop ((J.pullback f).op.obj (op S)))) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))

Tactic:
dsimp

Goal state after:
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)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
⊢ (Meq.equiv P (S.pullback f))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((S.pullback f).index P) (multiequalizer (S.index P))
            (fun I ↦ Multiequalizer.ι (S.index P) I.base) ⋯))
        ((Meq.equiv P S).symm x)) =
    (Meq.equiv P (S.pullback f)) ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
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 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
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
⊢ (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop Z)).map e.inv.op) ≫
      Multiequalizer.ι ((unop (op (((unop S).pullback f.unop).pullback g.unop))).index P) I =
    (Multiequalizer.lift (((unop S).pullback f.unop).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          ((J.diagram P (unop Y)).obj (op ((unop S).pullback f.unop)))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop (op (((unop S).pullback f.unop).pullback g.unop))).index P) I

Tactic:
dsimp

Goal state after:
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 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
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
⊢ (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) (multiequalizer ((unop S).index P))
          (fun I ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback (g.unop ≫ f.unop)).index P))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback (g.unop ≫ f.unop)).index P) (I.map e.inv)) ⋯) ≫
      Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I =
    (Multiequalizer.lift (((unop S).pullback f.unop).index P) (multiequalizer ((unop S).index P))
          (fun I ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback f.unop).index P))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) I.base) ⋯) ≫
      Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case right
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'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
b : S.shape.R
⊢ hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ (S.multifork P).π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.right b)

Tactic:
rw [← E.w (WalkingMulticospan.Hom.fst b),
        ← (S.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]
      congr 1
      apply hP.amalgamate_map

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

Goal state before:
pp: case h
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 := ⋯
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := ⋯
⊢ (fun t ↦ x.IsAmalgamation t) (hh.lift K) ∧
    ∀ (y : (P ⋙ coyoneda.obj (op E)).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = hh.lift K

Tactic:
dsimp

Goal state after:
case h
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 ⋯) ⋯
⊢ x.IsAmalgamation (hh.lift K) ∧ ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation y → y = hh.lift K
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) i))
      ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop (op ((J.pullback I.f).obj (unop (op S))))).index P) i))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Tactic:
dsimp

Goal state after:
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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P))
            (fun I_1 ↦ Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((ConcreteCategory.hom
          (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯))
        ((Meq.equiv P S).symm x))
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
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ ((J.plusFunctor D).map 0).app x✝ = NatTrans.app 0 x✝

Tactic:
dsimp

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
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (J.plusMap 0).app x✝ = 0