mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ uncurry (t.to (A ⟹ I) ≫ (ihom A).map (t.to (A ⊗ I))) = 𝟙 (A ⊗ I)

Tactic:
← eq_curry_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ t.to (A ⟹ I) ≫ (ihom A).map (t.to (A ⊗ I)) = curry (𝟙 (A ⊗ I))
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ ((F ⊗ G) ⋙ H).map f ≫ (prodComparisonIso H (F.obj Y) (G.obj Y)).hom =
    (prodComparisonIso H (F.obj X) (G.obj X)).hom ≫ (F ⋙ H ⊗ G ⋙ H).map f

Tactic:
dsimp; ext <;> simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map (𝟙 W ×ₘ f) ≫ F.map (𝟙 W ×ₘ g)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map (f ×ₘ 𝟙 W) ≫ F.map (g ×ₘ 𝟙 W)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (𝟙 X ×ₘ g) ≫ F.map (f ×ₘ 𝟙 Y') = F.map (f ×ₘ g)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c', t₁, t₂, h⟩ := (Types.FilteredColimit.colimit_eq_iff.{v₁, v₁, v₁} _).mp this

Goal state after:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
c' : C
t₁ t₂ : c ⟶ c'
h :
  (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₁)) s =
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₂)) s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ (ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom) ≤ R

pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ R ≤ ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom

Tactic:
· rintro _ _ ⟨X, h⟩
    exact h

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ R ≤ ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map (pullback.snd f₁ f₂).op ≫ P.map (pullback.lift g₁ g₂ comm).op)) (x f₂ hf₂) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)

Tactic:
← Functor.map_comp,

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
inst✝ : R.HasPairwisePullbacks
t : x.PullbackCompatible
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
⊢ (ConcreteCategory.hom (P.map ((pullback.snd f₁ f₂).op ≫ (pullback.lift g₁ g₂ comm).op))) (x f₂ hf₂) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ hf₂)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map ⋯.choose.op)) (x ⋯.choose ⋯) = x f hf

Tactic:
t h.choose (𝟙 _) _ hf _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map (𝟙 Y).op)) (x f hf) = x f hf

C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ h.choose ≫ ⋯.choose = 𝟙 Y ≫ f
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ pullback e.hom (ofArrows Z f) = ofArrows Z fun i ↦ f i ≫ e.inv

Tactic:
rw [Sieve.ext_iff]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
⊢ ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X'), (pullback e.hom (ofArrows Z f)).arrows f_1 ↔ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows f_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W✝ Y W : C
g : W ⟶ X
hg : R g
h : W✝ ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (generate R).arrows g

Tactic:
exact Sieve.le_generate R W _ hg

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map f₁.op ≫ P.map g₁.op)) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map (f₁.op ≫ g₁.op))) t =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (ConcreteCategory.hom (P.map ⋯.choose.op ≫ P.map ⋯.choose.op)) t

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (ConcreteCategory.hom (P.map (⋯.choose.op ≫ ⋯.choose.op))) t
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 : C
f : Y ⟶ X
S : Sieve X
⊢ functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

Tactic:
rw [Sieve.functorPushforward_le_iff_le_functorPullback, Sieve.functorPullback_pullback]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : Y ⟶ X
S : Sieve X
⊢ pullback f S ≤ pullback f (functorPullback F (functorPushforward F S))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

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

Tactic:
rw! [shrinkYonedaObjObjEquiv_symm_comp]

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

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ R.arrows (h' ≫ g)

Tactic:
apply R.downward_closed hg

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ IsSheafFor P S.arrows ↔ YonedaSheafCondition P S

Tactic:
by
  rw [isSheafFor_iff_bijective_shrinkFunctor_ι_comp, YonedaSheafCondition,
    Function.bijective_iff_existsUnique,
    Equiv.forall_congr_left S.shrinkFunctorIsoFunctor.homFromEquiv]
  refine forall_congr' fun a ↦ ?_
  rw [Equiv.existsUnique_congr_left (shrinkYonedaIsoYoneda.app X).homFromEquiv]
  refine existsUnique_congr fun b ↦ ?_
  dsimp
  rw [NatTrans.ext_iff, NatTrans.ext_iff, funext_iff, funext_iff]
  congr!
  rw [ConcreteCategory.hom_ext_iff, ConcreteCategory.hom_ext_iff]
  dsimp [functor]
  simp only [Subtype.forall, shrinkYonedaObjObjEquiv.forall_congr_left, Equiv.apply_symm_apply]
  congr!
  simp

Goal state after:
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
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔
    ∀ (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:
Presieve.isSheafFor_singleton

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.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)) ⋯ ≫
      colimit.ι (J.diagram P (unop Z)) (op ((unop S).pullback (g.unop ≫ f.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:
rw [← colimit.w _ e.inv.op, ← Category.assoc, ← Category.assoc]

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.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
⊢ (ConcreteCategory.hom (P.map j.op ≫ P.map f.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) =
    (ConcreteCategory.hom (P.map f.op)) (x j hj)

Tactic:
← Functor.map_comp,

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ (ConcreteCategory.hom (P.map (j.op ≫ f.op))) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) =
    (ConcreteCategory.hom (P.map f.op)) (x j hj)
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 ⋯
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap
        (J.diagramNatTrans
          { app := fun X ↦ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤), naturality := ⋯ } (unop X)) =
    colimit.ι (J.diagram P (unop X)) S ≫
      ⊤.toMultiequalizer (J.plusObj P) ≫ colimit.ι (J.diagram (J.plusObj P) (unop X)) (op ⊤)

Tactic:
rw [ι_colimMap, ← colimit.w _ e.op, ← Category.assoc, ← Category.assoc]

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.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.right b) = K.π.app (WalkingMulticospan.right b)

Tactic:
rw [← K.w (WalkingMulticospan.Hom.fst b), ←
        (T.multifork P).w (WalkingMulticospan.Hom.fst b), ← assoc]

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.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 ≫ γ
⊢ η = γ

Tactic:
by
  have : γ = J.plusLift (J.toPlus P ≫ γ) hQ := by
    apply plusLift_unique
    rfl
  rw [this]
  apply plusLift_unique
  exact h

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₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map f₁.op ≫ F.map g₁.op)) s =
    (ConcreteCategory.hom (F.map g₂.op)) ((ConcreteCategory.hom (F.map f₂.op)) s)

Tactic:
← Functor.map_comp,

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₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map (f₁.op ≫ g₁.op))) s =
    (ConcreteCategory.hom (F.map g₂.op)) ((ConcreteCategory.hom (F.map f₂.op)) s)
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₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map (f₁.op ≫ g₁.op))) s = (ConcreteCategory.hom (F.map f₂.op ≫ F.map g₂.op)) s

Tactic:
← Functor.map_comp,

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₂
e : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map (f₁.op ≫ g₁.op))) s = (ConcreteCategory.hom (F.map (f₂.op ≫ g₂.op))) s
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
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
⊢ G = sheafify J G

Tactic:
apply (G.le_sheafify J).antisymm

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
⊢ sheafify J G ≤ G