mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ IsColimit (c₁.tensor c₂)

Tactic:
refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1
    ((Functor.Final.isColimitWhiskerEquiv (Functor.diag J) _).2 (hc₁.tensor₂ hc₂))

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Functor.diag J ⋙ externalProduct F₁ F₂ ≅ F₁ ⊗ F₂

case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (Cocone.whisker (Functor.diag J) (c₁.tensor₂ c₂)) ≅ c₁.tensor c₂
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
j₂ : J₂
j₁ : J₁
h₁ : j₂ ≤ f j₁
⊢ ∃ c, Nonempty (j₂ ⟶ hf.functor.obj c)

Tactic:
exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
n : ((const J).obj s.pt).map fj ≫ s.π.app (j', k').1 = s.π.app (j, k).1 ≫ D.conePoints.map fj
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'

Tactic:
dsimp at n

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
n : 𝟙 s.pt ≫ s.π.app j' = s.π.app j ≫ (D.map fj).hom
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mpr.left
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁
j₂ : J₂
j₁ : J₁
h₁ : f j₁ ≤ j₂
⊢ ∃ c, Nonempty (hf.functor.obj c ⟶ j₂)

Tactic:
exact ⟨j₁, ⟨homOfLE h₁⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : D.coconePoints.map fj ≫ s.ι.app (j', k').1 = s.ι.app (j, k).1 ≫ ((const J).obj s.pt).map fj
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
dsimp at n

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j ≫ 𝟙 s.pt
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C✝ : Type u
inst✝¹ : Category.{v, u} C✝
R✝ : C✝ᵒᵖ ⥤ RingCat
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ IsColimit M.freeYonedaCoproductsCokernelCofork

Tactic:
let S := ShortComplex.mk _ _ M.toFreeYonedaCoproduct_fromFreeYonedaCoproduct
  let T := ShortComplex.mk _ _ (kernel.condition M.fromFreeYonedaCoproduct)
  let φ : S ⟶ T :=
    { τ₁ := fromFreeYonedaCoproduct _
      τ₂ := 𝟙 _
      τ₃ := 𝟙 _ }
  exact ((ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2
    (T.exact_of_f_is_kernel (kernelIsKernel _))).gIsCokernel

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv =
    colimit.ι (uncurry.obj F) (j, k)

Tactic:
dsimp [colimitUncurryIsoColimitCompColim, IsColimit.coconePointUniqueUpToIso,
    IsColimit.uniqueUpToIso]

Goal state after:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫
      colimit.ι (F ⋙ colim) j ≫
        (Cocone.forget (F ⋙ colim)).map
          ((colimit.isColimit (F ⋙ colim)).descCoconeMorphism
            (coconeOfCoconeUncurry (fun j ↦ colimit.isColimit (F.obj j)) (colimit.cocone (uncurry.obj F)))) =
    colimit.ι (uncurry.obj F) (j, k)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
r : ↑cR.pt
m₁ m₂ : ModuleColimit hcR hcM
⊢ r • (m₁ + m₂) = r • m₁ + r • m₂

Tactic:
obtain ⟨U, r, m₁, m₂, rfl, rfl, rfl⟩ := jointly_surjective₃' r m₁ m₂

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
r : ↑(R.obj U)
m₁ m₂ : ↑(M.obj U)
⊢ (ιR cR) r • (ιM m₁ + ιM m₂) = (ιR cR) r • ιM m₁ + (ιR cR) r • ιM m₂
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
    F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
ext X₀

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₁ : C₀ ⥤ C₁
F₁₁' : C₁ ⥤ C₁
G₁₀ : C₁ ⥤ C₀
G₁'₁ : C₁ ⥤ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
X₀ : C₀
⊢ (adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor)).hom.app X₀ =
    (F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor).hom.app X₀
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
    isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

Tactic:
ext X₀

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
inst✝¹ : Category.{v_1, u_1} C₀
inst✝ : Category.{v_2, u_2} C₁
F₀₀' : C₀ ⥤ C₀
F₀'₁ : C₀ ⥤ C₁
G₀'₀ : C₀ ⥤ C₀
G₁₀' : C₁ ⥤ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂)) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (τ₀₂₃ ≫ G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv)

Tactic:
obtain ⟨τ₀₂₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)).surjective τ₀₂₃

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂)) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃) =
    (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
        G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv)
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: case convert_4
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (fun i ↦ X (a i)) fun i ↦ f (a i)) ∈ J.coverings S

Tactic:
convert! hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ (Presieve.ofArrows (fun i ↦ X (a i)) fun i ↦ f (a i)) = Presieve.ofArrows X f
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
F : C ⥤ D
J K : Precoverage D
inst✝ : J.HasIsos
S T : C
f : S ⟶ T
hf : IsIso f
⊢ Presieve.singleton f ∈ (comap F J).coverings T

Tactic:
simpa using mem_coverings_of_isIso (F.map f)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
Y✝ : C
f✝ : Y✝ ⟶ Z
⊢ (pullback f (ofObjects X Y)).arrows f✝ ↔ (ofObjects X Z).arrows f✝

Tactic:
simp [Sieve.ofObjects]

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

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

Tactic:
change (f.app _ ≫ Q.map _) _ = _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
| Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
            ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
enter [2, a, 1, 1, 2]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a : Presieve.FamilyOfElements P S.arrows
| (firstObjEqFamily P S.arrows).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
· intro q x hx
    apply Exists.imp _ (q _ (hx.restrict (le_generate R)))
    intro t ht
    simpa [hx] using isAmalgamation_sieveExtend _ _ ht

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 (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
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:
← K.w (WalkingMulticospan.Hom.fst b),

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.right b) =
    K.π.app (WalkingMulticospan.left (T.shape.fst b)) ≫ (T.index P).multicospan.map (WalkingMulticospan.Hom.fst b)
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
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫ η.app (colimit (J.diagram P (unop X))) ≫ (J.plusCompIso G P).hom.app X =
    F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      (J.plusCompIso F P).hom.app X ≫ colimMap (J.diagramNatTrans (P.whiskerLeft η) (unop X))

Tactic:
simp only [ι_plusCompIso_hom, ι_colimMap, whiskerLeft_app, ι_plusCompIso_hom_assoc,
    NatTrans.naturality_assoc, GrothendieckTopology.diagramNatTrans_app]

Goal state after:
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
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ η.app (multiequalizer ((unop W).index P)) ≫
      (J.diagramCompIso G P (unop X)).hom.app W ≫ colimit.ι (J.diagram (P ⋙ G) (unop X)) W =
    (J.diagramCompIso F P (unop X)).hom.app W ≫
      Multiequalizer.lift ((unop W).index (P ⋙ G)) ((J.diagram (P ⋙ F) (unop X)).obj W)
          (fun x ↦ Multiequalizer.ι ((unop W).index (P ⋙ F)) x ≫ η.app (P.obj (op x.Y))) ⋯ ≫
        colimit.ι (J.diagram (P ⋙ G) (unop X)) W
Module: Mathlib.CategoryTheory.Sites.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj.map i.f.op =
    (multiforkEvaluationCone F E X W S).π.app k ≫ (F.obj k).obj.map i.f.op

Tactic:
dsimp only [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
m : S.pt ⟶ (W.multifork E.pt).pt
hm : ∀ (i : W.shape.L), m ≫ (W.multifork E.pt).ι i = S.ι i
k : K
i : W.Arrow
⊢ (m ≫ (E.π.app k).app (op X)) ≫ (F.obj k).obj.map i.f.op =
    ⋯.amalgamate W
        (fun x ↦ (Multifork.ofι (W.index (F.obj k).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app k).app (op i.Y)) ⋯).ι x) ⋯ ≫
      (F.obj k).obj.map i.f.op
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) f (c.ι.app j)

Tactic:
rw [← Category.comp_id f]

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
F G : J ⥤ C
α : F ⟶ G
inst✝ : IsIso α
c : Cocone G
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α' : F' ⟶ F
f : c'.pt ⟶ ((Cocone.precompose α).obj c).pt
e : α' ≫ ((Cocone.precompose α).obj c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α'
H : ∀ (j : J), IsPullback (c'.ι.app j) (α'.app j) f (((Cocone.precompose α).obj c).ι.app j)
j : J
⊢ IsPullback (c'.ι.app j) (α'.app j ≫ α.app j) (f ≫ 𝟙 ((Cocone.precompose α).obj c).pt) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k) f
    (c.ι.app k)

Tactic:
rw [← Category.comp_id f]

Goal state after:
case convert_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsUniversalColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
k : K
⊢ IsPullback ((Cocone.whisker e.inverse c').ι.app k) ((e.inverse.whiskerLeft α ≫ (e.invFunIdAssoc F).hom).app k)
    (f ≫ 𝟙 (Cocone.whisker e.functor c).pt) (c.ι.app k)