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
F : J ⥤ K ⥤ C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
| colimit.ι (F.flip.obj k) j ≫
    colimit.ι (F.flip ⋙ colim) k ≫
      (colimitUncurryIsoColimitCompColim F.flip).inv ≫
        (HasColimit.isoOfNatIso F.uncurryObjFlip).hom ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
            (colimitUncurryIsoColimitCompColim F).hom

Tactic:
slice 1 3

Goal state after:
case a.a.a
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 J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
| colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k ≫ (colimitUncurryIsoColimitCompColim F.flip).inv

case a.a.a
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 J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
| (HasColimit.isoOfNatIso F.uncurryObjFlip).hom

case a.a
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 J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
| (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom

case a
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 J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
| (colimitUncurryIsoColimitCompColim F).hom
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 J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
| colimit.ι (F.obj j) k ≫
    colimit.ι (F ⋙ colim) j ≫
      (((colimitUncurryIsoColimitCompColim F).inv ≫
            (HasColimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv) ≫
          (HasColimit.isoOfNatIso F.uncurryObjFlip).inv) ≫
        (colimitUncurryIsoColimitCompColim F.flip).hom

Tactic:
slice 1 3

Goal state after:
case a.a.a
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 J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
| colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitUncurryIsoColimitCompColim F).inv

case a.a.a
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 J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
| (HasColimit.isoOfEquivalence (Prod.braiding K J) (NatIso.ofComponents (fun x ↦ Iso.refl ((F.obj x.2).obj x.1)) ⋯)).inv

case a.a
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 J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
| (HasColimit.isoOfNatIso F.uncurryObjFlip).inv

case a
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 J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
| (colimitUncurryIsoColimitCompColim F.flip).hom
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
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
by
  simp [limitCurrySwapCompLimIsoLimitCurryCompLim]

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
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
    colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
      ((colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv ≫
          (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
        (colimitIsoColimitCurryCompColim G).hom

Tactic:
slice 1 3

Goal state after:
case a.a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
    colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫ (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv

case a.a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom

case a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| (colimitIsoColimitCurryCompColim G).hom
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| colimit.ι ((curry.obj G).obj j) k ≫
    colimit.ι (curry.obj G ⋙ colim) j ≫
      (colimitIsoColimitCurryCompColim G).inv ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv ≫
          (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom

Tactic:
slice 1 3

Goal state after:
case a.a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv

case a.a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).inv

case a
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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
| (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ 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₃₂ ⋙ G₂₁ ⋙ G₁₀)

Tactic:
Category.comp_id,

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₁₂)) τ₀₁₂)
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: 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
Z : C
g : Z ⟶ S
hg : Presieve.ofArrows X f g
⊢ Presieve.ofArrows (fun i ↦ X (a i)) (fun i ↦ f (a i)) g

Tactic:
exact .mk' (Sum.inl ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

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

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.fst g f = 𝟙 (Limits.pullback g f) ≫ pullback.fst g f

pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f

Tactic:
· rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
        simp

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ (pullback.snd g f ≫ pullback.lift (f ≫ inv g) (𝟙 Y) ⋯) ≫ pullback.snd g f = 𝟙 (Limits.pullback g f) ≫ pullback.snd g f
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
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows f

Tactic:
← h3

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows (e1 ≫ e2)
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows Z g).bind Ti ≤ ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst

pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti

Tactic:
· rintro T u ⟨S, v, w, ⟨i⟩, hv, rfl⟩
        rw [hp] at hv
        obtain ⟨j⟩ := hv
        exact .mk <| Sigma.mk (β := fun i : ι ↦ κ (g i) ⟨i⟩) i j

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
⊢ (ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst) ≤ (ofArrows Z g).bind Ti
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
⊢ IsSeparatedFor P R → IsSeparatedFor P (generate R).arrows

Tactic:
intro h x t₁ t₂ ht₁ ht₂
    apply h (x.restrict (le_generate R)) t₁ t₂ _ _
    · exact isAmalgamation_restrict _ x t₁ ht₁
    · exact isAmalgamation_restrict _ x t₂ ht₂

Goal state after:
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:
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: 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 (f.unop ≫ shrinkYonedaObjObjEquiv ↑x✝.down) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))

Tactic:
shrinkYonedaObjObjEquiv_symm_comp

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)}
⊢ (hom ((shrinkYoneda.{max w w', v₁, u₁}.obj X).map f.unop.op))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down)) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))
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).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ (Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop X)).map e.inv.op) ≫
      colimit.ι (J.diagram P (unop X)) (op (unop S)) =
    colimit.ι (J.diagram P (unop X)) S

Tactic:
convert! Category.id_comp (colimit.ι (diagram J P (unop X)) S)

Goal state after:
case e'_2
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).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
e_1✝ :
  (multiequalizer ((unop S).index P) ⟶ colimit (J.diagram P (unop X))) =
    ((J.diagram P (unop X)).obj S ⟶ colimit (J.diagram P (unop X)))
⊢ Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagram P (unop X)).map e.inv.op =
    𝟙 ((J.diagram P (unop X)).obj S)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
rw [isSheaf_iff_isSheaf_of_type] at hP

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e'_2
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 ⟶ ⊤ := ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1✝ :
  ((J.diagram P (unop X)).obj S ⟶ ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
    (multiequalizer ((unop S).index P) ⟶
      ((unop S).index P).right
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } })
⊢ ((Multiequalizer.ι ((unop S).index P) I ≫ ⊤.toMultiequalizer P) ≫ (J.diagram P I.Y).map ee.op) ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II =
    Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.fst
          { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }) ≫
      ((unop S).index P).fst
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }

pp: case e'_3
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 ⟶ ⊤ := ⋯
I : (unop S).shape.L
ee : (J.pullback (Cover.Arrow.map I e).f).obj (unop S) ⟶ ⊤ := ⋯
II : (unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).shape.L
e_1✝ :
  ((J.diagram P (unop X)).obj S ⟶ ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P).left II) =
    (multiequalizer ((unop S).index P) ⟶
      ((unop S).index P).right
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } })
⊢ 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)) ⋯ ≫
      Multiequalizer.ι ((unop (op ((J.pullback (Cover.Arrow.map I e).f).obj (unop S)))).index P) II =
    Multiequalizer.ι ((unop S).index P)
        ((unop S).shape.snd
          { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }) ≫
      ((unop S).index P).snd
        { fst := I, snd := Cover.Arrow.base II, r := { Z := II.Y, g₁ := II.f, g₂ := 𝟙 II.Y, w := ⋯ } }

Tactic:
all_goals simp

Goal state after:
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
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⇑(ConcreteCategory.hom (p.app U✝)) ⁻¹' ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' G.obj V✝ ⊆
    ⇑(ConcreteCategory.hom (F'.map f)) ⁻¹' ⇑(ConcreteCategory.hom (p.app V✝)) ⁻¹' G.obj V✝

Tactic:
by
    simp only [Set.preimage_preimage, NatTrans.naturality_apply]
    rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h : (ConcreteCategory.hom f) (prod.fst.hom' x, ?m.86).1 = (ConcreteCategory.hom g) (?m.92, prod.snd.hom' x).2
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))

Tactic:
use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩

Goal state after:
case h
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : ↑(X ⨯ Y)
h :
  (ConcreteCategory.hom f) (prod.fst.hom' x, prod.snd.hom' x).1 =
    (ConcreteCategory.hom g) (prod.fst.hom' x, prod.snd.hom' x).2
⊢ (ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))
      ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(prod.fst.hom' x, prod.snd.hom' x), h⟩) =
    x