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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (F.map f.op)) y = x) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (F.map f.op)) y = x) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y
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
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))

Tactic:
]

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
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P Y) ((J.pullback f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P f).app (op S))) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P Y) (op (S.pullback f))))
      ((Meq.equiv P (S.pullback f)).symm (x.pullback f))
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))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ (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) ≫
      colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop)) =
    (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)) ⋯) ≫
      colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop))

Tactic:
]

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))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ (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) ≫
      colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop)) =
    (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)) ⋯) ≫
      colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop))
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
i : (S.pullback f).Arrow
⊢ ↑x i.base = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }

Tactic:
]

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
i : (S.pullback f).Arrow
⊢ ↑x i.base = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
A✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} A✝
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
ℱ : Sheaf J A
E : A
⊢ Presieve.IsSheaf J (ℱ.obj ⋙ coyoneda.obj (op E))

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
A✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} A✝
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
ℱ : Sheaf J A
E : A
⊢ Presieve.IsSheaf J (ℱ.obj ⋙ coyoneda.obj (op E))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: 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
⊢ IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
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
⊢ IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
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 : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
]

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 : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ (J.diagram P X).map e.op ≫ colimit.ι (J.diagram P X) (op S))) x =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))
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.left (S.shape.fst b))) ≫
      (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
]

Goal state after:
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.left (S.shape.fst b))) ≫
      (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b)) ≫ (S.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
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 : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S)))
      ((ConcreteCategory.hom ((J.diagram P X).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S x))

Tactic:
]

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 : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S)))
      ((ConcreteCategory.hom ((J.diagram P X).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I ↦ P.map I.f.op) ⋯)) x)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P X) (op S))) ((Meq.equiv P S).symm (Meq.mk S 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
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)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ E.π.app (WalkingMulticospan.left I) = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op

Tactic:
]

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'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ E.π.app (WalkingMulticospan.left I) = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op
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:
]

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
⊢ x (f ≫ j) ⋯ = (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x (f ≫ j) ⋯)
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ᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    𝟙
      ({ 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:
]

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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    𝟙
      ({ 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✝)
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
⊢ π j = π j

Tactic:
]

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)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (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 (colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Tactic:
]

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
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (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 (colimit.ι (J.diagram P I.Y) ((J.pullback I.f).op.obj (op S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1.refine_1
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
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t ↦ hx.familyOfElements.IsAmalgamation t) y → y = t
i : I
⊢ x i = x i

Tactic:
]

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
X Y : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
⊢ ((P.map f ≫ Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯) ≫
        (J.diagram P (unop Y)).map e.op) ≫
      colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤)) =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop 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) (Cover.Arrow.base I)) ⋯) ≫
      colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤))

Tactic:
]

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 : Cᵒᵖ
f : X ⟶ Y
e : (J.pullback f.unop).obj ⊤ ⟶ ⊤ := homOfLE ⋯
⊢ ((P.map f ≫ Multiequalizer.lift (⊤.index P) (P.obj (op (unop Y))) (fun I ↦ P.map I.f.op) ⋯) ≫
        (J.diagram P (unop Y)).map e.op) ≫
      colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤)) =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop 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) (Cover.Arrow.base I)) ⋯) ≫
      colimit.ι (J.diagram P (unop Y)) (op ((J.pullback f.unop).obj ⊤))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1.refine_2
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
h : IsSheafFor P (ofArrows X π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
t : P.obj (op B)
ht₁ : hx.familyOfElements.IsAmalgamation t
ht₂ : ∀ (y : P.obj (op B)), (fun t ↦ hx.familyOfElements.IsAmalgamation t) y → y = t
t' : (fun X ↦ X) (P.obj (op B))
ht' : (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) t'
x✝² : C
x✝¹ : x✝² ⟶ B
x✝ : ofArrows X π x✝¹
i : I
⊢ x i = x i

Tactic:
]

Goal state after: