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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (G.map ((Prod.braiding K J).counitInv.app (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).hom.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          colimit.ι (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k))) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
dsimp [Equivalence.counitInv]

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✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (G.map (Prod.mkHom (𝟙 j) (𝟙 k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

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

Tactic:
by
  obtain ⟨U, ⟨a, x₁, x₂⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM'))) ⟨r, m₁, m₂⟩
  rw [Prod.ext_iff, Prod.ext_iff] at h
  obtain ⟨rfl, rfl, rfl⟩ := h
  exact ⟨U, a, x₁, x₂, rfl, rfl, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)

Tactic:
by
  refine @IsGLB.of_image _ _ _ _ sieves ?_ _ _ ?_
  · rfl
  · exact _root_.isGLB_sInf _

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (b : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor ⟶ P), ∃! a, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a = b) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f

Tactic:
Equiv.forall_congr_left S.shrinkFunctorIsoFunctor.homFromEquiv

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (b : S.functor ⟶ P), ∃! a, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a = S.shrinkFunctorIsoFunctor.homFromEquiv.symm b) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
A✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} A✝
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
ℱ : Sheaf J A
E : A
⊢ Presheaf.IsSheaf J (ℱ.obj ⋙ coyoneda.obj (op E))

Tactic:
rw [isSheaf_iff_isSheaf_of_type]
    exact ℱ.property E

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
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection s).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
        (ConcreteCategory.hom (F.map f.op)) s

Tactic:
intro V i hi

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
h : Presieve.IsSheaf J F
hG : Presieve.IsSheaf J G.toFunctor
U : Cᵒᵖ
s : F.obj U
hs : s ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection s).arrows i
⊢ (ConcreteCategory.hom (F.map i.op)) ↑(⋯.amalgamate (G.familyOfElementsOfSection s) ⋯) =
    (ConcreteCategory.hom (F.map i.op)) s
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 Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ mk x = mk y

Tactic:
rw [eq_mk_iff_exists]

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)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S Sx : J.Cover X
x : Meq P Sx
Sy : J.Cover X
y : Meq P Sy
h : ∀ (I : S.Arrow), mk (x.pullback I.f) = mk (y.pullback I.f)
W : (I : S.Arrow) → J.Cover I.Y
h1 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sx
h2 : (I : S.Arrow) → W I ⟶ (J.pullback I.f).obj Sy
hh : ∀ (I : S.Arrow), (x.pullback I.f).refine (h1 I) = (y.pullback I.f).refine (h2 I)
⊢ ∃ W h1 h2, x.refine h1 = y.refine h2
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
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
⊢ (Sieve.bind S.arrows fun V i hi ↦ G.sieveOfSection ↑(x i hi)) ≤ G.sieveOfSection t

Tactic:
intro V i hi

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
this : x''.Compatible
t : F.obj (op U)
ht : x''.IsAmalgamation t
ht' : ∀ (y : F.obj (op U)), (fun t ↦ x''.IsAmalgamation t) y → y = t
V : C
i : V ⟶ unop (op U)
hi : (Sieve.bind S.arrows fun V i hi ↦ G.sieveOfSection ↑(x i hi)).arrows i
⊢ (G.sieveOfSection t).arrows i
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
    (G.sieveOfSection ↑((ConcreteCategory.hom ((homOfLe ⋯).app U)) s)).arrows f_1 →
      (ConcreteCategory.hom (F'.map f_1.op)) ((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) =
        (ConcreteCategory.hom (F'.map f_1.op)) ((ConcreteCategory.hom (f.app U)).toFun s)

Tactic:
intro V i hi

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((ConcreteCategory.hom ((homOfLe ⋯).app U)) s)).arrows i
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (f.app U)).toFun s)
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 G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection x).arrows f →
      (ConcreteCategory.hom (F.map f.op)) x =
        (ConcreteCategory.hom (F.map f.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩)

Tactic:
intro V i hi

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
⊢ (ConcreteCategory.hom (F.map i.op)) x =
    (ConcreteCategory.hom (F.map i.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩)
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ F.map (colimit.ι (J.diagram P (unop X)) W) ≫
      F.map (colimMap (J.diagramPullback P f.unop)) ≫
        F.map (colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
          ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom ≫
            (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (((colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom) ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop)) ≫
      colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op

Tactic:
slice_lhs 1 3 =>
        simp only [← F.map_comp]
        dsimp [colimMap, IsColimit.map, colimit.pre]
        simp only [colimit.ι_desc_assoc, colimit.ι_desc]
        dsimp [Cocone.precompose]
        simp only [Category.assoc, colimit.ι_desc]
        dsimp [Cocone.whisker]
        rw [F.map_comp]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
W : (J.Cover (unop X))ᵒᵖ
⊢ ((F.map
            (Multiequalizer.lift (((unop W).pullback f.unop).index P) (multiequalizer ((unop W).index P))
              (fun I ↦ Multiequalizer.ι ((unop W).index P) I.base) ⋯) ≫
          F.map (colimit.ι (J.diagram P (unop Y)) (op ((unop W).pullback f.unop)))) ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop Y) ⋙ F))).hom) ≫
      (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (((colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
          (HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom) ≫
        colimMap (J.diagramPullback (P ⋙ F) f.unop)) ≫
      colimit.pre (J.diagram (P ⋙ F) (unop Y)) (J.pullback f.unop).op
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.refine_2
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set ↑X
x : ↑Y
y : ↑X
hy : y ∈ U
eq : (ConcreteCategory.hom f) y = (ConcreteCategory.hom g) x
⊢ (ConcreteCategory.hom (pullback.snd f g)) ((ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) ⟨(y, x), eq⟩) = x

Tactic:
· rw [pullbackIsoProdSubtype_inv_snd_apply]

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
⊢ IsVanKampenColimit c'

Tactic:
by
  intro F' c'' α f h hα
  have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by
    ext j
    exact e.inv.2 j
  rw [H c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα]
  apply forall_congr'
  intro j
  conv_lhs => rw [← Category.comp_id (α.app j)]
  have : IsIso e.inv.hom := Functor.map_isIso (Cocone.forget _) e.inv
  exact (IsPullback.of_vert_isIso ⟨by simp⟩).paste_vert_iff (NatTrans.congr_app h j).symm

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

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

Tactic:
simp [← Functor.map_comp]

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 := IsFiltered.sup (Finset.image k Finset.univ) ∅
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x

Tactic:
have g : ∀ j, k j ⟶ k' := fun j => IsFiltered.toSup (Finset.univ.image k) ∅ (by simp)

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 := IsFiltered.sup (Finset.image k Finset.univ) ∅
g : (j : J) → k j ⟶ k'
⊢ ∃ a, (ConcreteCategory.hom (colimitLimitToLimitColimit F)) a = x
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case refine_2
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
            (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)).inr)

Tactic:
refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩
    convert! f.hom.2.1 _ isOpen_range_inr

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

Goal state before:
pp: case h₁
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
c'' : Cocone (F' ⋙ Gr) :=
  { pt := pullback (Gr.map f) (adj.unit.app c.pt),
    ι := { app := fun j ↦ pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }
j : J
⊢ ((adj.counit.app (F'.obj j) ≫ 𝟙 (F'.obj j)) ≫ c'.ι.app j) ≫ f = adj.counit.app (F'.1 j) ≫ c'.ι.app j ≫ f

Tactic:
rw [Category.comp_id, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)} (hc : IsColimit c), IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)

Tactic:
apply FinitaryExtensive.van_kampen'
      exact coprodIsCoprod _ _

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

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type s
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
F' : K ⥤ (J.Cover X)ᵒᵖ ⥤ D := F ⋙ J.diagramFunctor D X
e : colimit (limit (F ⋙ J.diagramFunctor D X)) ≅ limit (colimit (F ⋙ J.diagramFunctor D X).flip) :=
  colimitLimitIso (F ⋙ J.diagramFunctor D X)
t : J.diagram (limit F) X ≅ limit (F ⋙ J.diagramFunctor D X) :=
  (isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
    (limit.isLimit (F ⋙ J.diagramFunctor D X))
p : (J.plusObj (limit F)).obj (op X) ≅ colimit (limit (F ⋙ J.diagramFunctor D X)) := HasColimit.isoOfNatIso t
⊢ ∀ {X_1 Y : K} (f : X_1 ⟶ Y),
    (colimit (F ⋙ J.diagramFunctor D X).flip).map f ≫
        (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip Y).hom =
      (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip X_1).hom ≫
        (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
by
        intro i j f
        rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq]
        refine colimit.hom_ext (fun w => ?_)
        dsimp [plusMap]
        erw [colimit.ι_map_assoc,
          colimitObjIsoColimitCompEvaluation_ι_inv (F ⋙ J.diagramFunctor D X).flip w j,
          colimitObjIsoColimitCompEvaluation_ι_inv_assoc (F ⋙ J.diagramFunctor D X).flip w i]
        rw [← (colimit.ι (F ⋙ J.diagramFunctor D X).flip w).naturality]
        rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ G₂.map (whiskerRight f F) ≫
      (adj₂.homEquiv (Q ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm (whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))).symm (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f)

Tactic:
← adj₂.homEquiv_naturality_left_symm,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj Q))).symm
      (whiskerRight f F ≫ whiskerRight (adj₁.unit.app Q) F) =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))).symm (whiskerRight (adj₁.unit.app P) F) ≫
      (sheafCompose J F).map (G₁.map f)