mathlib-initiative/mathlib-tactics huggingface dataset:
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 ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))))
      ((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 (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj 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
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))))
      ((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 (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj 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: 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))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    Function.Bijective (Arrows.toCompatible P π)

Tactic:
]

Goal state after:
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))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    Function.Bijective (Arrows.toCompatible P π)
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))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S))

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
            (unop X)).app
        S ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) S =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      colimit.ι (J.diagram (J.plusObj P) (unop X)) (op (unop S))
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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }.app (op I.Y) =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I

Tactic:
]

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
⊢ Multiequalizer.ι ((unop S).index P) I ≫
      { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }.app (op I.Y) =
    ((colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
        (J.diagram (J.plusObj P) (unop X)).map e.op) ≫
      Multiequalizer.ι ((unop S).index (J.plusObj P)) I
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case 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 : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : ↑(Arrows.toCompatible P π y) = ↑⟨x, hx⟩
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
]

Goal state after:
case 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 : Function.Bijective (Arrows.toCompatible P π)
x : (i : I) → P.obj (op (X i))
hx : Arrows.Compatible P π x
y : P.obj (op B)
hy : ↑(Arrows.toCompatible P π y) = ↑⟨x, hx⟩
⊢ ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))) =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        ((J.diagram P (unop X)).obj S) (fun I_1 ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯ ≫
      colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)

Tactic:
]

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : unop S ⟶ ⊤ := homOfLE ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := homOfLE ⋯
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      colimit.ι (J.diagram P I.Y) (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S))) =
    Multiequalizer.lift ((unop ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)).index P)
        ((J.diagram P (unop X)).obj S) (fun I_1 ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I_1)) ⋯ ≫
      colimit.ι (J.diagram P (unop (op (Cover.Arrow.map I e.op.unop).Y)))
        ((J.pullback (Cover.Arrow.map I e.op.unop).f.op.unop).op.obj S)
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 (P.map (Cover.Arrow.map i e).f.op)) (↑x I) =
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) (Cover.Arrow.base i))) ((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
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 (P.map (Cover.Arrow.map i e).f.op)) (↑x I) =
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) (Cover.Arrow.base i))) ((Meq.equiv P S).symm x)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h.right.right
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 ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
]

Goal state after:
case h.right.right
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 ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ (e ≫ (T.multifork P).π.app (WalkingMulticospan.left (T.shape.fst b))) ≫
      (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.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 : 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 (P.map (Cover.Arrow.map i e).f.op)) (↑x I) = ↑x (Cover.Arrow.base i)

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
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 (P.map (Cover.Arrow.map i e).f.op)) (↑x I) = ↑x (Cover.Arrow.base 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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
⊢ IsIso (J.toPlus P)

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
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
⊢ IsIso (J.toPlus P)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case h
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)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = mk ((Meq.equiv P (unop S)) y)

Tactic:
]

Goal state after:
case h
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)
X : C
P : Cᵒᵖ ⥤ D
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = mk ((Meq.equiv P (unop S)) y)
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
hQ : Presheaf.IsSheaf J Q
⊢ (J.toPlus P ≫ J.plusMap η) ≫ (J.isoToPlus Q hQ).inv = η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (J.toPlus P ≫ J.plusMap η) ≫ (J.isoToPlus Q hQ).inv = η
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
hQ : Presheaf.IsSheaf J Q
⊢ J.toPlus P ≫ J.plusMap η = η ≫ (J.isoToPlus Q hQ).hom

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ J.toPlus P ≫ J.plusMap η = η ≫ (J.isoToPlus Q hQ).hom
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
hQ : Presheaf.IsSheaf J Q
⊢ J.toPlus P ≫ J.plusMap η = J.toPlus P ≫ J.plusMap η

Tactic:
]

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

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

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'
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
X : C
S : J.Cover X
⊢ IsLimit (S.multifork P)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ (Y i₂).hom

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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
γ : J.plusObj P ⟶ Q
hγ : J.toPlus P ≫ γ = η
⊢ γ ≫ (J.isoToPlus Q hQ).hom = J.plusMap (J.toPlus P) ≫ J.plusMap γ
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
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)

Tactic:
]

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
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
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
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ η = J.plusLift (J.toPlus P ≫ γ) hQ

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 Q : Cᵒᵖ ⥤ D
η γ : J.plusObj P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toPlus P ≫ η = J.toPlus P ≫ γ
this : γ = J.plusLift (J.toPlus P ≫ γ) hQ
⊢ η = J.plusLift (J.toPlus P ≫ γ) hQ
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
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P = (J.isoToPlus P hP).hom

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
hP : Presheaf.IsSheaf J P
⊢ J.toPlus P = (J.isoToPlus P hP).hom
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 R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ η ≫ γ = η ≫ γ

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
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ 0 = 0

Tactic:
]

Goal state after: