mathlib-initiative/mathlib-tactics huggingface dataset:
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ᵒᵖ),
    colimMap (J.diagramPullback P (𝟙 X).unop) ≫ colimit.pre (J.diagram P (unop X)) (J.pullback (𝟙 X).unop).op =
      𝟙 (colimit (J.diagram P (unop X)))

Tactic:
by
    intro X
    refine colimit.hom_ext (fun S => ?_)
    dsimp
    simp only [diagramPullback_app, colimit.ι_pre, ι_colimMap_assoc, Category.comp_id]
    let e := S.unop.pullbackId
    dsimp only [Functor.op, pullback_obj]
    rw [← colimit.w _ e.inv.op, ← Category.assoc]
    convert! Category.id_comp (colimit.ι (diagram J P (unop X)) S)
    refine Multiequalizer.hom_ext _ _ _ (fun I => ?_)
    dsimp
    simp only [Multiequalizer.lift_ι, Category.id_comp, Category.assoc]
    dsimp [Cover.Arrow.map, Cover.Arrow.base]
    cases I
    congr
    simp

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

Goal state before:
pp: case mpr.refine_1
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
x : unop (op X)
Y₁ Y₂ Z : C
⊢ ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Y⦄ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₁ f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₂ f₂ h₂)

Tactic:
g₁

Goal state after:
case mpr.refine_1
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
x : unop (op X)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Y⦄ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : S.arrows f₁) (h₂ : S.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₁ f₁ h₁) =
        (ConcreteCategory.hom (P.map g₂.op)) ((fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) Y₂ f₂ h₂)
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:
congr 1

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
⊢ 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.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)) ⋯
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:
congr 1

Goal state after:
case right.e_a
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)) =
    E.π.app (WalkingMulticospan.left (S.shape.fst b))
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))ᵒᵖ
⊢ (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✝)) ≫
      colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝) =
    ((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)) ⋯) ≫
      colimit.ι (J.diagram Q (unop Y)) ((J.pullback f.unop).op.obj j✝)

Tactic:
congr 1

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
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
j✝ : (J.Cover (unop X))ᵒᵖ
⊢ 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✝) =
    (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)) ⋯
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:
congr 1

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 : 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 =
    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)) ⋯
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ᵒᵖ
⊢ (η.app x✝ ≫ Multiequalizer.lift (⊤.index Q) (Q.obj (op (unop x✝))) (fun I ↦ Q.map I.f.op) ⋯) ≫
      colimit.ι (J.diagram Q (unop x✝)) (op ⊤) =
    (Multiequalizer.lift (⊤.index P) (P.obj (op (unop x✝))) (fun I ↦ P.map I.f.op) ⋯ ≫
        (J.diagramNatTrans η (unop x✝)).app (op ⊤)) ≫
      colimit.ι (J.diagram Q (unop x✝)) (op ⊤)

Tactic:
congr 1

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

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 ⋯
⊢ (J.diagramNatTrans { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ }
          (unop X)).app
      S =
    (colimit.ι (J.diagram P (unop X)) S ≫ ⊤.toMultiequalizer (J.plusObj P)) ≫
      (J.diagram (J.plusObj P) (unop X)).map e.op
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:
congr 1

Goal state after:
case e_a.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 =
    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)) ⋯
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:
congr 1

Goal state after:
case h.right.right.e_a
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)) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b))
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.plusMap 0).app x✝ = 0

Tactic:
J.plusMap_zero,

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ᵒᵖ
⊢ NatTrans.app 0 x✝ = 0
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
⊢ range ((G.preimage p).ι ≫ p) ≤ G

Tactic:
rw [range_comp, range_ι, image_le_iff]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
⊢ ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ unop U⦄ ⦃f₂ : Y₂ ⟶ unop U⦄ (h₁ : (G.sieveOfSection s).arrows f₁)
    (h₂ : (G.sieveOfSection s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (G.toFunctor.map g₁.op)) (G.familyOfElementsOfSection s f₁ h₁) =
        (ConcreteCategory.hom (G.toFunctor.map g₂.op)) (G.familyOfElementsOfSection s f₂ h₂)

Tactic:
g₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
s : F.obj U
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ unop U⦄ ⦃f₂ : Y₂ ⟶ unop U⦄ (h₁ : (G.sieveOfSection s).arrows f₁)
    (h₂ : (G.sieveOfSection s).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (G.toFunctor.map g₁.op)) (G.familyOfElementsOfSection s f₁ h₁) =
        (ConcreteCategory.hom (G.toFunctor.map g₂.op)) (G.familyOfElementsOfSection s f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case 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
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op)) (x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op)) (x j)

Tactic:
apply t
    exact pullback.condition

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
⊢ ∀ (g₁ : V₃ ⟶ V₁) (g₂ : V₃ ⟶ V₂) ⦃f₁ : V₁ ⟶ U⦄ ⦃f₂ : V₂ ⟶ U⦄ (h₁ : S'.arrows f₁) (h₂ : S'.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' f₁ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)

Tactic:
g₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ V₂ V₃ : C
g₁ : V₃ ⟶ V₁
⊢ ∀ (g₂ : V₃ ⟶ V₂) ⦃f₁ : V₁ ⟶ U⦄ ⦃f₂ : V₂ ⟶ U⦄ (h₁ : S'.arrows f₁) (h₂ : S'.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' f₁ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
⊢ ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Y⦄ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : (B H).arrows f₁) (h₂ : (B H).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) (y H f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y H f₂ h₂)

Tactic:
g₁

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
Y : C
f : Y ⟶ X
H : U.arrows f
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Y⦄ ⦃f₂ : Y₂ ⟶ Y⦄ (h₁ : (B H).arrows f₁) (h₂ : (B H).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (P.map g₁.op)) (y H f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y H f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

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

Tactic:
delta diagramCompIso
  simp

Goal state after: