mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
        (limitIsoLimitCurryCompLim G).hom) ≫
      limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
Category.assoc,

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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ ((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
        (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ ((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
        (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
Category.assoc,

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
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom ≫
        (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j
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₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
        G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv) ≫
      (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
Category.assoc,

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₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv) ≫
        (G₃₂.associator G₂₁ G₁₀).hom
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₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫ (G₃₂.associator G₂₁ G₁₀).inv) ≫
        (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
Category.assoc,

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₀₃
⊢ (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))) ((F₀₁.associator F₁₂ F₂₃).inv ≫ whiskerRight τ₀₁₂ F₂₃ ≫ τ₀₂₃) ≫
      (G₃₂.associator G₂₁ G₁₀).hom =
    (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)) τ₀₂₃ ≫
      G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)) τ₀₁₂) ≫
        (G₃₂.associator G₂₁ G₁₀).inv ≫ (G₃₂.associator G₂₁ G₁₀).hom
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback f (Sieve.generate (S.bind Ti)) ∈ J Z

Tactic:
apply J.superset_covering _ (hTi _ hf)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.generate (Ti f hf) ≤ Sieve.pullback f (Sieve.generate (S.bind Ti))
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sInf (sieves '' T) X → Sieve.pullback f S ∈ sInf (sieves '' T) Y

Tactic:
rintro X Y S hS f _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X Y : C
S : Sieve X
hS : Y ⟶ X
f : S ∈ sInf (sieves '' T) X
J : GrothendieckTopology C
hJ : J ∈ T
⊢ Sieve.pullback hS S ∈ (fun f ↦ ↑f Y) ⟨J.sieves, ⋯⟩
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ (trivial C) X → S ∈ ⊥ X

Tactic:
hS

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ (trivial C) X
⊢ S ∈ ⊥ X
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.IsStableUnderComposition
ι : Type (max u v)
S : C
Y : ι → C
f : (i : ι) → Y i ⟶ S
σ : ι → Type (max u v)
Z : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Z i j ⟶ Y i
hf : (Presieve.ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)) ∈ J.coverings (F.obj S)
hg : ∀ (i : ι), (Presieve.ofArrows (fun i_1 ↦ F.obj (Z i i_1)) fun i_1 ↦ F.map (g i i_1)) ∈ J.coverings (F.obj (Y i))
⊢ (Presieve.ofArrows (fun i ↦ F.obj (Z i.fst i.snd)) fun i ↦ F.map (g i.fst i.snd) ≫ F.map (f i.fst)) ∈
    J.coverings (F.obj S)

Tactic:
exact J.comp_mem_coverings _ hf _ hg

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ { l // l ≫ (Fork.ofι f w).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = l }

Tactic:
refine ⟨↾fun i => ?_, ?_, ?_⟩

Goal state after:
case refine_1
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
i : s.pt
⊢ (Fork.ofι f w).pt

case refine_2
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ (↾fun i ↦ ?refine_1) ≫ (Fork.ofι f w).ι = s.ι

case refine_3
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = ↾fun i ↦ ?refine_1
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
h : S.arrows (𝟙 X)
Y : C
f : Y ⟶ X
x✝ : ⊤.arrows f
⊢ S.arrows f

Tactic:
by simpa using downward_closed _ h f

Goal state after:
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 Z : C
f✝ : Y ⟶ X
S R : Sieve X
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ULift.{w', w} ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ ↑((hom
            ((↾fun x ↦ { down := ⟨(hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map f)) ↑x.down, ⋯⟩ }) ≫
              (Equiv.ulift.trans
                    ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom)).toFun
        x✝) =
    ↑((hom
            ((Equiv.ulift.trans
                    ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom ≫
              ↾fun x ↦ ⟨(hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f)) ↑x, ⋯⟩)).toFun
        x✝)

Tactic:
dsimp [Equiv.subtypeEquiv_apply]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ULift.{w', w} ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ((hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map f)) ↑x✝.down)) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))
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 Z : C
f✝ : Y ⟶ X
S R : Sieve X
U V : Cᵒᵖ
f : U ⟶ V
⊢ (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.map f ≫ (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom =
    (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom ≫ S.functor.map f

Tactic:
dsimp [Equiv.subtypeEquiv_apply]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
U V : Cᵒᵖ
f : U ⟶ V
⊢ (↾fun x ↦ ⟨(hom ((shrinkYoneda.{v₁, v₁, u₁}.obj X).map f)) ↑x, ⋯⟩) ≫
      (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom =
    (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom ≫ ↾fun g ↦ ⟨f.unop ≫ ↑g, ⋯⟩
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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ (Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫ η.app (op ((unop W).shape.fst i).Y)) ≫
      ((unop W).index Q).fst i =
    (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd i

Tactic:
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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫
      η.app (op ((unop W).shape.fst i).Y) ≫ ((unop W).index Q).fst i =
    (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd 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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫
      η.app (op ((unop W).shape.fst i).Y) ≫ ((unop W).index Q).fst i =
    (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd i

Tactic:
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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫
      η.app (op ((unop W).shape.fst i).Y) ≫ ((unop W).index Q).fst i =
    Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫
      η.app (op ((unop W).shape.snd i).Y) ≫ ((unop W).index Q).snd 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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ (Multiequalizer.ι ((unop W).index P) ((unop W).shape.fst i) ≫ η.app (op ((unop W).shape.fst i).Y)) ≫
      ((unop W).index Q).fst i =
    (Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ η.app (op ((unop W).shape.snd i).Y)) ≫
      ((unop W).index Q).snd i

Tactic:
erw [Category.assoc, Category.assoc, ← η.naturality, ← η.naturality,
        Multiequalizer.condition_assoc]
      rfl

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

Goal state before:
pp: case mpr
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
⊢ S ∈ J Y → Presieve.IsSheafFor (P ⋙ coyoneda.obj (op X)) S.arrows

Tactic:
hS

Goal state after:
case mpr
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
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj (op X)) S.arrows
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
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
⊢ S ∈ J X → Presieve.IsSheafFor (P ⋙ coyoneda.obj (op E)) S.arrows

Tactic:
hS

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
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (P ⋙ coyoneda.obj (op E)) S.arrows
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op I.Y))) (↑x I) = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) (mk x)

Tactic:
dsimp only [toPlus, plusObj]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
⊢ (ConcreteCategory.hom (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P I.Y) (op ⊤))) (↑x I) =
    (ConcreteCategory.hom
        (colimMap (J.diagramPullback P I.f.op.unop) ≫ colimit.pre (J.diagram P I.Y) (J.pullback I.f.op.unop).op))
      (mk 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
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π ↑(Arrows.toCompatible P π y)
y' : (fun X ↦ X) (P.obj (op B))
hy' : (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = ↑(Arrows.toCompatible P π y) i) y'
⊢ Arrows.toCompatible P π y' = Arrows.toCompatible P π y

Tactic:
ext; apply hy'

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

Tactic:
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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ η ≫ J.toPlus Q ≫ J.plusLift γ hR = η ≫ γ
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
f : F' ⟶ F
G : Subfunctor F
hf : range f ≤ G
x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
⊢ (F'.map g ≫ ↾fun x ↦ ⟨(ConcreteCategory.hom (f.app x✝)) x, ⋯⟩) =
    (↾fun x ↦ ⟨(ConcreteCategory.hom (f.app x✝¹)) x, ⋯⟩) ≫ G.toFunctor.map g

Tactic:
by
    ext x
    simpa [Subtype.ext_iff, -NatTrans.naturality_apply] using NatTrans.naturality_apply f g x

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p

Tactic:
intro i x hx
    simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
    obtain ⟨y, rfl⟩ := hp _ x
    exact ⟨y, hx, rfl⟩

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
⊢ S ∈ J X → Presieve.IsSheafFor (P' ⋙ coyoneda.obj (op U)) S.arrows

Tactic:
hS

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor (P' ⋙ coyoneda.obj (op U)) S.arrows
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf' J P' → IsSheaf J P'

Tactic:
intro h U X S hS
    rw [Equalizer.Presieve.sheaf_condition]
    refine ⟨?_⟩
    refine isSheafForIsSheafFor' _ _ _ _ ?_
    letI := preservesSmallestLimits_of_preservesLimits (coyoneda.obj (op U))
    apply isLimitOfPreserves
    apply Classical.choice (h _ S.arrows _)
    simpa

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ mk x = mk y ↔ ∃ W h1 h2, x.refine h1 = y.refine h2

Tactic:
constructor
  · intro h
    obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq (C := D) _ _ _ h
    use W.unop, h1.unop, h2.unop
    ext I
    apply_fun Multiequalizer.ι (W.unop.index P) I at hh
    convert! hh
    all_goals
      dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases I; rfl
  · rintro ⟨S, h1, h2, e⟩
    apply Concrete.colimit_rep_eq_of_exists (C := D)
    use op S, h1.op, h2.op
    apply Concrete.multiequalizer_ext
    intro i
    apply_fun fun ee => ee i at e
    convert! e using 1
    all_goals
      dsimp [diagram]
      rw [← ConcreteCategory.comp_apply, Multiequalizer.lift_ι]
      erw [Meq.equiv_symm_eq_apply]
      cases i; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono ((sheafToPresheaf J (Type w)).map (Sheaf.imageι f))

Tactic:
by
      dsimp
      infer_instance

Goal state after: