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:
(Tactic.Conv.convSeq1Indented
 [(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:
(Tactic.Conv.convSeq1Indented
 [(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.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:
(Tactic.Conv.convSeq1Indented
 [(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:
(Tactic.Conv.convSeq1Indented
 [(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.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
⊢ g ≫ c.π.app j' =
    F.partialRightAdjointHomEquiv
      (F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j) ≫ F.partialRightAdjointMap (R.map φ))

Tactic:
partialRightAdjointHomEquiv_map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j j' : J
φ : j ⟶ j'
this : c.π.app j ≫ (R.map φ).hom = c.π.app j'
⊢ g ≫ c.π.app j' = F.partialRightAdjointHomEquiv (F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j)) ≫ (R.map φ).hom
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) (a • m₁) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
erw [M₁.map_smul]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ ((ConcreteCategory.hom ((R ⋙ forget₂ CommRingCat RingCat).map f)) a •
        (ConcreteCategory.hom (M₁.map f)) m₁) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
⊢ J = ⊤ ↔ ∀ (X : C), ⊥ ∈ J X

Tactic:
refine ⟨fun h ↦ h ▸ by simp, fun h ↦ ?_⟩
  rw [_root_.eq_top_iff]
  intro X S _
  exact J.superset_covering bot_le (h X)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : Y ⟶ X
⊢ singleton f g ↔ f = g

Tactic:
constructor
  · rintro ⟨a, rfl⟩
    rfl
  · rintro rfl
    apply singleton.mk

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
I : Type u_1
X : I → C
Y : C
⊢ functorPushforward F (ofObjects X Y) ≤ ofObjects (F.obj ∘ X) (F.obj Y)

Tactic:
rintro Z f ⟨W, g₁, g₂, ⟨i, ⟨g₃⟩⟩, hf⟩
  exact ⟨i, ⟨g₂ ≫ F.map g₃⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
⊢ ∃! t, x₂.IsAmalgamation t

Tactic:
let x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
⊢ ∃! t, x₂.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_1
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
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
x : unop (op X)
⊢ Presieve.FamilyOfElements.Compatible fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h
      exact (ConcreteCategory.congr_hom (hz g₁ g₂ hf₁ hf₂ h)) x

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
U : Sieve X
B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → Sieve Y
hU : IsSheafFor P U.arrows
hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), IsSheafFor P (B hf).arrows
hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y), IsSeparatedFor P (Sieve.pullback g (B h)).arrows
⊢ IsSheafFor P (Sieve.bind U.arrows B).arrows

Tactic:
intro s hs
  let y : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), Presieve.FamilyOfElements P (B hf : Presieve Y) :=
    fun Y f hf Z g hg => s _ (Presieve.bind_comp _ _ hg)
  have hy : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).Compatible := by
    intro Y f H Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm
    apply hs
    apply reassoc_of% comm
  let t : Presieve.FamilyOfElements P (U : Presieve X) :=
    fun Y f hf => (hB hf).amalgamate (y hf) (hy hf)
  have ht : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : U f), (y hf).IsAmalgamation (t f hf) := fun Y f hf =>
    (hB hf).isAmalgamation _
  have hT : t.Compatible := by
    rw [Presieve.compatible_iff_sieveCompatible]
    intro Z W f h hf
    apply (hB (U.downward_closed hf h)).isSeparatedFor.ext
    intro Y l hl
    apply (hB' hf (l ≫ h)).ext
    intro M m hm
    have : Sieve.bind U B (m ≫ l ≫ h ≫ f) := by simpa using (bind_comp f hf hm : Sieve.bind U B _)
    trans s (m ≫ l ≫ h ≫ f) this
    · have := ht (U.downward_closed hf h) _ ((B _).downward_closed hl m)
      simp only [op_comp, Functor.map_comp, comp_apply] at this
      grind
    · have h : s _ _ = _ := (ht hf _ hm).symm
      -- Porting note: this was done by `simp only [assoc] at`
      conv_lhs at h => congr; rw [assoc, assoc]
      simp [h]
  refine ⟨hU.amalgamate t hT, ?_, ?_⟩
  · rintro Z _ ⟨Y, f, g, hg, hf, rfl⟩
    rw [op_comp, Functor.map_comp, comp_apply, Presieve.IsSheafFor.valid_glue _ _ _ hg]
    apply ht hg _ hf
  · intro y hy
    apply hU.isSeparatedFor.ext
    intro Y f hf
    apply (hB hf).isSeparatedFor.ext
    intro Z g hg
    rw [← comp_apply, ← Functor.map_comp, ← op_comp, hy _ (Presieve.bind_comp _ _ hg),
      hU.valid_glue _ _ hf, ht hf _ hg]

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

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ η = γ

Tactic:
rw [sheafifyLift_unique J _ hQ _ h, ← h]

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
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ η) hQ = γ
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
suffices Epi f ↔ Epi ((forget TopCat).map f) by
    rw [this, CategoryTheory.ofHom_epi_iff_surjective]

Goal state after:
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ''
      range ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left })))
    (range
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
        ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }))))

Tactic:
← eq_compl_iff_isCompl

Goal state after:
case mp
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ''
      range ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left })) =
    (range
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) ∘
          ⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }))))ᶜ
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.refine_4
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ { app := fun X_1 ↦ Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY, naturality := ⋯ }.Equifibered

Tactic:
rintro i _ (_ | _ | _)
      · dsimp; simp_rw [Functor.map_id]
        exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩
      exacts [hf, hg]

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ hf f' = gf f' ∨ ⟨k', ⟨kf f', ⟨k'O, ⟨⋯, hf f'⟩⟩⟩⟩ ∈ {⟨k', ⟨kf f', ⟨k'O, ⟨⋯, hf f'⟩⟩⟩⟩}

Tactic:
Finset.mem_singleton,

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
O : Finset K := (Finset.univ.biUnion fun j ↦ Finset.univ.biUnion fun j' ↦ Finset.image kf Finset.univ) ∪ {k'}
kfO : ∀ {j j' : J} (f : j ⟶ j'), kf f ∈ O
k'O : k' ∈ O
H : Finset ((X : K) ×' (Y : K) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun j ↦
    Finset.univ.biUnion fun j' ↦
      Finset.univ.biUnion fun f ↦ {⟨k', ⟨kf f, ⟨k'O, ⟨⋯, gf f⟩⟩⟩⟩, ⟨k', ⟨kf f, ⟨k'O, ⟨⋯, hf f⟩⟩⟩⟩}
k'' : K
i' : {X : K} → X ∈ O → (X ⟶ k'')
s' : ∀ {X Y : K} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H → f ≫ i' mY = i' mX
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k'' := fun {j j'} f ↦ i' ⋯
j₁ j₂ j₃ j₄ : J
f : j₁ ⟶ j₂
f' : j₃ ⟶ j₄
⊢ hf f' = gf f' ∨ ⟨k', ⟨kf f', ⟨k'O, ⟨⋯, hf f'⟩⟩⟩⟩ = ⟨k', ⟨kf f', ⟨k'O, ⟨⋯, hf f'⟩⟩⟩⟩
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
refine e₁.trans (Eq.symm ?_)

Goal state after:
case mp.refine_2.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl = s.inl