mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ⊤)))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯)) (↑x I)) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))

Tactic:
rw [← colimit.w _ e.op, ConcreteCategory.comp_apply]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj (unop (op S))))))
      ((ConcreteCategory.hom ((J.diagram P I.Y).map e.op))
        ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯))
          (↑x I))) =
    (ConcreteCategory.hom (colimit.ι (J.diagram P I.Y) (op ((J.pullback I.f).obj S))))
      ((ConcreteCategory.hom ((J.diagramPullback P I.f).app (op S))) ((Meq.equiv P S).symm x))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x : FamilyOfElements P (ofArrows X π)
hx : x.Compatible
⊢ ∃! t, x.IsAmalgamation t

Tactic:
obtain ⟨t, hA, ht⟩ := h (fun i ↦ x (π i) (ofArrows.mk _))
      (fun i j Z gi gj ↦ hx gi gj (ofArrows.mk _) (ofArrows.mk _))
    exact ⟨t, fun Y f ⟨i⟩ ↦ hA i, fun y hy ↦ ht y (fun i ↦ hy (π i) (ofArrows.mk _))⟩

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

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

Tactic:
obtain ⟨S, y, h⟩ := Concrete.colimit_exists_rep (J.diagram P X) x

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
x : ToType ((J.plusObj P).obj (op X))
S : (J.Cover X)ᵒᵖ
y : ToType ((J.diagram P X).obj S)
h : (ConcreteCategory.hom (colimit.ι (J.diagram P X) S)) y = x
⊢ ∃ S y, x = mk y
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ ∀ (j : WalkingMulticospan S.shape),
    (limit.cone (S.index P).multicospan).π.app j = (asIso (S.toMultiequalizer P)).symm.hom ≫ (S.multifork P).π.app j

Tactic:
· intro a
      symm
      simp

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
⊢ G ≤ sheafify J G

Tactic:
intro U

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
U : Cᵒᵖ
⊢ G.obj U ⊆ (sheafify J G).obj U
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
⊢ sheafify J G ≤ G

Tactic:
intro U

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ᵒᵖ
⊢ (sheafify J G).obj U ⊆ G.obj U
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((sheafify J G).toFunctor.map f_1 ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
      (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map f_1

Tactic:
intro U

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
⊢ ∀ ⦃Y : Cᵒᵖ⦄ (f_1 : U ⟶ Y),
    ((sheafify J G).toFunctor.map f_1 ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
      (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map f_1
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
⊢ sheafify J G ≤ G'

Tactic:
intro U

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ᵒᵖ
⊢ (sheafify J G).obj U ⊆ G'.obj U
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
⊢ (ConcreteCategory.hom (G'.obj.map i.op)) ((ConcreteCategory.hom (g₁.hom.app U)).toFun ⟨s, hx⟩) =
    (ConcreteCategory.hom (G'.obj.map i.op)) ((ConcreteCategory.hom (g₂.hom.app U)).toFun ⟨s, hx⟩)

Tactic:
change (g₁.hom.app _ ≫ G'.obj.map _) _ = (g₂.hom.app _ ≫ G'.obj.map _) _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G'✝ : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj.obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj.obj (op V)
e' : (ConcreteCategory.hom (f.hom.app (op V))) y = (ConcreteCategory.hom (F'.obj.map i.op)) s
⊢ (ConcreteCategory.hom (g₁.hom.app (op (unop U)) ≫ G'.obj.map i.op)) ⟨s, hx⟩ =
    (ConcreteCategory.hom (g₂.hom.app (op (unop U)) ≫ G'.obj.map i.op)) ⟨s, hx⟩
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
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
X : C
W : J.Cover X
S : Multifork (W.index E.pt)
⊢ ∀ ⦃X_1 Y : K⦄ (f : X_1 ⟶ Y),
    ((Functor.const K).obj S.pt).map f ≫
        (Presheaf.isLimitOfIsSheaf J (F.obj Y).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj Y).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app Y).app (op i.Y)) ⋯) =
      (Presheaf.isLimitOfIsSheaf J (F.obj X_1).obj W ⋯).lift
          (Multifork.ofι (W.index (F.obj X_1).obj) S.pt (fun i ↦ S.ι i ≫ (E.π.app X_1).app (op i.Y)) ⋯) ≫
        (F ⋙ sheafToPresheaf J D ⋙ (evaluation Cᵒᵖ D).obj (op X)).map f

Tactic:
by
        intro i j f
        dsimp [Presheaf.isLimitOfIsSheaf]
        rw [Category.id_comp]
        apply Presheaf.IsSheaf.hom_ext (F.obj j).2 W
        intro ii
        rw [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← (F.map f).hom.naturality, ←
          Category.assoc, Presheaf.IsSheaf.amalgamate_map]
        erw [Category.assoc, ← E.w f]
        cat_disch

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

Goal state before:
pp: case left
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
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P))))

Tactic:
intro x y h
    apply sep P S _ _
    intro I
    apply_fun Meq.equiv (J.plusObj P) S at h
    apply_fun fun e => e I at h
    dsimp only [ConcreteCategory.forget_map_eq_ofHom] at h
    simpa [Meq.equiv_apply, ← comp_apply] using! h

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

Goal state before:
pp: case h
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
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
⊢ (Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t) =
    Meq.mk S t

Tactic:
ext i

Goal state after:
case h
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
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
x : ToType (multiequalizer (S.index (J.plusObj P)))
t : ToType ((J.plusObj P).obj (op X))
ht : Meq.mk S t = (Meq.equiv (J.plusObj P) S) x
i : S.Arrow
⊢ ↑((Meq.equiv (J.plusObj P) S) ((ConcreteCategory.hom ((forget D).map (S.toMultiequalizer (J.plusObj P)))) t)) i =
    ↑(Meq.mk S t) i
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
⊢ coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.1 j).str ≤ topologicalSpaceCoconePtOfCoconeForget c

Tactic:
dsimp [topologicalSpaceCoconePtOfCoconeForget]

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
⊢ coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.1 j).str ≤
    ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
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:
dsimp [topologicalSpaceCoconePtOfCoconeForget]

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.Pullbacks

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackFst f g ≫ f = pullbackSnd f g ≫ g

Tactic:
dsimp [pullbackFst, pullbackSnd, Function.comp_def]
      ext ⟨x, h⟩
      simpa

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

Goal state before:
pp: X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
⊢ IsOpen U ↔ IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)

Tactic:
by
  rw [isOpen_iff_of_isColimit _ hc]
  constructor
  · intro h
    exact h .one
  · rintro h (_ | _)
    · rw [← c.w .left]
      exact Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h
    · exact h

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'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') k')) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') k')) ((ConcreteCategory.hom (F.map (f ×ₘ g j))) (y j))

Tactic:
← Bifunctor.diagonal'

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'
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') k')) ((ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j'))) (y j')) =
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j') k'))
      ((ConcreteCategory.hom (F.map (f ×ₘ 𝟙 (k j)) ≫ F.map (𝟙 j' ×ₘ g j))) (y j))
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
i j : J
g : i ⟶ j
⊢ Gr.map (F'.map g ≫ α.app j ≫ adj.counit.app (F.obj j)) ≫ c.ι.app j =
    Gr.map (α.app i ≫ adj.counit.app (F.obj i)) ≫ c.ι.app i

Tactic:
rw [α.naturality_assoc]
        dsimp
        rw [adj.counit_naturality, ← Category.assoc, Gr.map_comp_assoc]
        congr 1
        exact c.w _

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
⊢ (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl

Tactic:
rw [Category.assoc, pullback.lift_snd, hg.w]

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

Goal state before:
pp: case e_a
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))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ colimit.ι (J.diagram (F.obj k) X) j ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).inv =
    (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k

Tactic:
erw [colimit.ι_desc]

Goal state after:
case e_a
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))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ (((evaluation K D).obj k).mapCocone (colimit.cocone (F ⋙ J.diagramFunctor D X).flip)).ι.app j =
    (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k
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
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ : Cᵒᵖ ⥤ A
⊢ ∀ ⦃Y : Cᵒᵖ ⥤ A⦄ (f : P₁ ⟶ Y), J.W f → IsIso (((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B).map f)

Tactic:
P₂

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
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
P₁ P₂ : Cᵒᵖ ⥤ A
⊢ ∀ (f : P₁ ⟶ P₂), J.W f → IsIso (((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B).map f)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
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
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ : Cᵒᵖ ⥤ A
⊢ ∀ ⦃Y : Cᵒᵖ ⥤ A⦄ (f : P₁ ⟶ Y), J.W f → J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
P₂

Goal state after:
case mpr
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
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
⊢ ∀ (f : P₁ ⟶ P₂), J.W f → J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f