mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ ∃ c, Nonempty (x✝ ⟶ F.obj c)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
· use Classical.choice IsFiltered.nonempty
    exact ⟨Discrete.eqToHom (by simp)⟩

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ c' t, x✝¹ ≫ F.map t = x✝ ≫ F.map t
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)
j : J
k k' : K
f : k ⟶ k'
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
← uncurry_obj_map F (𝟙 j ×ₘ f)

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)
j : J
k k' : K
f : k ⟶ k'
| (uncurry.obj F).map (𝟙 j ×ₘ f)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
X Y : Cᵒᵖ
f : X ⟶ Y
x : F.obj X
⊢ (ConcreteCategory.hom
        (ModuleCat.freeDesc (↾fun x ↦ ModuleCat.freeMk ((ConcreteCategory.hom (F.map f)) x)) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y))))
      (ModuleCat.freeMk x) =
    (ConcreteCategory.hom (ModuleCat.freeDesc (φ.app X) ≫ G.map f)) (ModuleCat.freeMk x)

Tactic:
simpa using! NatTrans.naturality_apply φ f x

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 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:
(choice
 (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
 (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "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:
(choice
 (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
 (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "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.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
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 a_1 x_1,
    (ιR cR) a_1 =
        ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
            (a, x)).1 ∧
      ιM x_1 =
        ((ConcreteCategory.hom ((((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).ι.app U))
            (a, x)).2

Tactic:
exact ⟨U, a, x, rfl, rfl⟩

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:
(choice
 (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
 (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "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:
(choice
 (Mathlib.Tactic.Slice.convSlice___ "slice" (num "1") (group) (num "3"))
 (Mathlib.Tactic.Slice.slice "slice" (num "1") (num "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.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ M.map (F.op.map (f ≫ g)) =
    M.map (F.op.map f) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
        (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))

Tactic:
refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))
      exact (M.congr_map_apply (F.op.map_comp f g) x).trans (by simp)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X
x : E
f : x ⟶ (F ⋙ G).obj X
⊢ functorPushforward (F ⋙ G) R f → functorPushforward G (functorPushforward F R) f

Tactic:
rintro ⟨X, f₁, g₁, h₁, rfl⟩

Goal state after:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Presieve X✝
x : E
X : C
f₁ : X ⟶ X✝
g₁ : x ⟶ (F ⋙ G).obj X
h₁ : R f₁
⊢ functorPushforward G (functorPushforward F R) (g₁ ≫ (F ⋙ G).map f₁)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
Z : C
g : Z ⟶ Y
hg : (R h).arrows g
⊢ (bind S R).arrows (g ≫ f)

Tactic:
exact ⟨_, g, f, h, hg, rfl⟩

Goal state after:
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 [

Goal state after:
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
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
R : Presieve X
inst✝ : R.HasPairwisePullbacks
| Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a

Tactic:
enter [

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
| Presieve.IsSheafFor P R ↔
    ∀ (a : Presieve.FamilyOfElements P R),
      ((ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P R)) x = (firstObjEqFamily P R).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ x.IsAmalgamation t → (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x → x.IsAmalgamation t

Tactic:
· intro q
    funext Y f hf
    simpa [Iso.toEquiv, forkMap] using q _ _

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
⊢ (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x → x.IsAmalgamation t
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
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ ((J.diagram P Y).map f ≫
        Multiequalizer.lift ((unop ((J.pullback f✝).op.obj T)).index P) ((J.diagram P Y).obj T)
          (fun I ↦ Multiequalizer.ι ((unop T).index P) (Cover.Arrow.base I)) ⋯) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I =
    (Multiequalizer.lift ((unop ((J.pullback f✝).op.obj S)).index P) ((J.diagram P Y).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        ((J.pullback f✝).op ⋙ J.diagram P X).map f) ≫
      Multiequalizer.ι ((unop ((J.pullback f✝).op.obj T)).index P) I

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom

Tactic:
reassoc_of% h,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
this : Over.Hom.left (f i₂) ≫ X.hom = (Y i₂).hom
⊢ Over.Hom.left g₂ ≫ (Y i₂).hom = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂) ≫ X.hom
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
⊢ Epi (toRange p)

Tactic:
simp [epi_iff_range_eq_top]

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

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

Tactic:
intro V₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
H : ∀ (s : (sheafify J G).toFunctor.obj (op U)), x''.IsAmalgamation ↑s → x.IsAmalgamation s
V₁ : C
⊢ ∀ ⦃Y₂ Z : C⦄ (g₁ : Z ⟶ V₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : V₁ ⟶ U⦄ ⦃f₂ : Y₂ ⟶ U⦄ (h₁ : S'.arrows f₁) (h₂ : S'.arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x'' f₁ h₁) = (ConcreteCategory.hom (F.map g₂.op)) (x'' f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.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✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
E : Cocone (F ⋙ sheafToPresheaf J D)
k : K
⊢ 𝟙 ((presheafToSheaf J D).obj (F.obj k).obj).obj ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [Category.id_comp, toSheafify_naturality, sheafificationAdjunction_counit_app_val,
    sheafifyLift_id_toSheafify_assoc]

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ Continuous ⇑(ConcreteCategory.hom (c.π.app j))

Tactic:
rw [continuous_iff_le_induced]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ topologicalSpaceConePtOfConeForget c ≤ induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.1 j).str
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)
inst✝ : (forget D).ReflectsIsomorphisms
P : Cᵒᵖ ⥤ D
X : C
S : J.Cover X
x y : ToType ((J.plusObj P).obj (op X))
⊢ (∀ (I : S.Arrow),
      (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) x = (ConcreteCategory.hom ((J.plusObj P).map I.f.op)) y) →
    x = y

Tactic:
apply sep

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [continuous_iff_le_induced]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : ↑(W ⨯ X)
⊢ (ConcreteCategory.hom prod.fst) ((ConcreteCategory.hom (prod.map f g)) y) ∈ range ⇑(ConcreteCategory.hom f) ∧
    (ConcreteCategory.hom prod.snd) ((ConcreteCategory.hom (prod.map f g)) y) ∈ range ⇑(ConcreteCategory.hom g)

Tactic:
Set.mem_range,

Goal state after:
case mp
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
y : ↑(W ⨯ X)
⊢ (∃ y_1, (ConcreteCategory.hom f) y_1 = (ConcreteCategory.hom prod.fst) ((ConcreteCategory.hom (prod.map f g)) y)) ∧
    ∃ y_1, (ConcreteCategory.hom g) y_1 = (ConcreteCategory.hom prod.snd) ((ConcreteCategory.hom (prod.map f g)) y)