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

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
⊢ x.IsAmalgamation (hS.amalgamate (FamilyOfElements.restrict h x) ⋯)

Tactic:
intro W

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
⊢ ∀ (f : W ⟶ X) (h_1 : R f),
    (ConcreteCategory.hom (P.map f.op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) = x f h_1
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ (ConcreteCategory.hom (P.map (f ≫ j).op)) (hS.amalgamate (FamilyOfElements.restrict h x) ⋯) =
    (ConcreteCategory.hom (P.map f.op)) (x j hj)

Tactic:
hS.valid_glue (hx.restrict h) _ hf,

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
hx : x.Compatible
W : C
j : W ⟶ X
hj : R j
Y : C
f : Y ⟶ W
hf : (Sieve.pullback j S).arrows f
⊢ FamilyOfElements.restrict h x (f ≫ j) hf = (ConcreteCategory.hom (P.map f.op)) (x j hj)
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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    (𝟙
          { obj := fun X ↦ colimit (J.diagram P (unop X)),
            map := fun {X Y} f ↦
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }).app
      x✝

Tactic:
NatTrans.id_app

Goal state after:
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)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ colimMap (𝟙 (J.diagram P (unop x✝))) =
    𝟙
      ({ obj := fun X ↦ colimit (J.diagram P (unop X)),
            map := fun {X Y} f ↦
              colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op,
            map_id := ⋯, map_comp := ⋯ }.obj
        x✝)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
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✝ : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
⊢ ∃ a, Arrows.toCompatible P π a = ⟨y, hy⟩

Tactic:
obtain ⟨x, hx, _⟩ := h y hy
    exact ⟨x, by ext; apply hx⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
i : C
x : F'.obj i
⊢ ↑((ConcreteCategory.hom ((toRange p).app i)) x) = (ConcreteCategory.hom (p.app i)) x

Tactic:
by
  simp [toRange]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

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

Tactic:
NatTrans.isIso_iff_isIso_app

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
⊢ ∀ (X : C), IsIso ((toRange p).app X)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₁ →
        ((FamilyOfElements.singletonEquiv P f).symm b).IsAmalgamation t₂ → t₁ = t₂) ↔
    Function.Injective ⇑(ConcreteCategory.hom (P.map f.op))

Tactic:
simp_rw [FamilyOfElements.isAmalgamation_singleton_iff,
    FamilyOfElements.singletonEquiv_symm_apply_self, Function.Injective]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
⊢ (∀ (b : P.obj (op X)) (t₁ t₂ : P.obj (op Y)),
      (ConcreteCategory.hom (P.map f.op)) t₁ = b → (ConcreteCategory.hom (P.map f.op)) t₂ = b → t₁ = t₂) ↔
    ∀ ⦃a₁ a₂ : P.obj (op Y)⦄, (ConcreteCategory.hom (P.map f.op)) a₁ = (ConcreteCategory.hom (P.map f.op)) a₂ → a₁ = a₂
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'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop V⦄,
    (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows f_1 →
      (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom
                ((sheafify J G).toFunctor.map i ≫
                  ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
            s) =
        (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun
            s)

Tactic:
intro W

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 V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
⊢ ∀ ⦃f_1 : W ⟶ unop V⦄,
    (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows f_1 →
      (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom
                ((sheafify J G).toFunctor.map i ≫
                  ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯)).toFun
            s) =
        (ConcreteCategory.hom (F'.map f_1.op))
          ((ConcreteCategory.hom ((↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i)).toFun
            s)
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
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        (J.plusObj P ⋙ F).map f ≫
          ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop Y) ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
          (J.plusObj (P ⋙ F)).map f

Tactic:
intro W

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.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      (J.plusObj P ⋙ F).map f ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop Y) ⋙ F)) ≪≫
            HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
              (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
            HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
        (J.plusObj (P ⋙ F)).map f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S)).arrows g → (Sieve.pullback f R).arrows g

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f R).arrows g → (Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S)).arrows g

Tactic:
· rintro ⟨W, k, l, hl, _, comm⟩
        rw [pullback_apply, ← comm]
        simp [hl]

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f R).arrows g → (Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S)).arrows g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f R).arrows g → (Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S)).arrows g

Tactic:
intro a
        refine ⟨Z, 𝟙 Z, _, a, ?_⟩
        simp [hf]

Goal state after:
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
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusObj P).whiskerLeft η ≫ (J.plusCompIso G P).hom).app X =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusCompIso F P).hom ≫ J.plusMap (P.whiskerLeft η)).app X

Tactic:
intro W

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
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      ((J.plusObj P).whiskerLeft η ≫ (J.plusCompIso G P).hom).app X =
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      ((J.plusCompIso F P).hom ≫ J.plusMap (P.whiskerLeft η)).app X
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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X

Tactic:
intro W

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
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app W ≫
      ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X
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
⊢ ((sheafifyCocone E).ι.app k).hom = E.ι.app k ≫ toSheafify J E.pt

Tactic:
rw [← cancel_epi ((sheafToPresheaf _ _).map
    ((sheafificationAdjunction J D).counit.app (F.obj k)))]

Goal state after:
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
⊢ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app (F.obj k)) ≫ ((sheafifyCocone E).ι.app k).hom =
    (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app (F.obj k)) ≫ E.ι.app k ≫ toSheafify J E.pt
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
⊢ ((𝟙 (sheafToPresheaf J D ⋙ presheafToSheaf J D)).app (F.obj k)).hom ≫ ((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:
NatTrans.id_app

Goal state after:
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
⊢ (𝟙 ((sheafToPresheaf J D ⋙ presheafToSheaf J D).obj (F.obj k))).hom ≫ ((presheafToSheaf J D).map (E.ι.app k)).hom =
    ((sheafificationAdjunction J D).counit.app (F.obj k)).hom ≫ E.ι.app k ≫ toSheafify J E.pt
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h✝ :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
h :
  ∀ (j : J),
    ∃ k f g,
      (ConcreteCategory.hom (((curry.obj F).obj j).map f))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
        (ConcreteCategory.hom (((curry.obj F).obj j).map g))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
k : J → K := fun j ↦ ⋯.choose
f : (j : J) → kx ⟶ k j := fun j ↦ ⋯.choose
g : (j : J) → ky ⟶ k j := fun j ↦ ⋯.choose
⊢ (ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x =
    (ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y

Tactic:
have w :
      ∀ j, F.map (𝟙 j ×ₘ f j) (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j x) =
          F.map (𝟙 j ×ₘ g j) (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j y) :=
      fun j => (h j).choose_spec.choose_spec.choose_spec

Goal state after:
case intro
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h✝ :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
h :
  ∀ (j : J),
    ∃ k f g,
      (ConcreteCategory.hom (((curry.obj F).obj j).map f))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
        (ConcreteCategory.hom (((curry.obj F).obj j).map g))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
k : J → K := fun j ↦ ⋯.choose
f : (j : J) → kx ⟶ k j := fun j ↦ ⋯.choose
g : (j : J) → ky ⟶ k j := fun j ↦ ⋯.choose
w :
  ∀ (j : J),
    (ConcreteCategory.hom (F.map (𝟙 j ×ₘ f j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
      (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
⊢ (ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x =
    (ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case mpr.refine_1
X Y : TopCat
c : BinaryCofan X Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl)
h₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : ↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left })),
    x ∈ range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ range ⇑(ConcreteCategory.hom c.inr)
⊢ {T : TopCat} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)

Tactic:
intro T f g
        refine ofHom (ContinuousMap.mk ?_ ?_)
        · exact fun x =>
            if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁.injective).symm ⟨x, h⟩)
            else g ((Equiv.ofInjective _ h₂.injective).symm ⟨x, (this x).resolve_left h⟩)
        rw [continuous_iff_continuousAt]
        intro x
        by_cases h : x ∈ Set.range c.inl
        · revert h x
          apply (IsOpen.continuousOn_iff _).mp
          · rw [continuousOn_iff_continuous_domRestrict]
            convert_to Continuous (f ∘ h₁.isEmbedding.toHomeomorph.symm)
            · ext ⟨x, hx⟩
              exact dif_pos hx
            fun_prop
          · exact h₁.isOpen_range
        · revert h x
          simp only [← mem_compl_iff]
          apply (IsOpen.continuousOn_iff _).mp
          · rw [continuousOn_iff_continuous_domRestrict]
            have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr := by
              rintro a (h : a ∈ (Set.range c.inl)ᶜ)
              rwa [eq_compl_iff_isCompl.mpr h₃.symm]
            convert_to! Continuous
                (g ∘ h₂.isEmbedding.toHomeomorph.symm ∘ Subtype.map _ this)
            · ext ⟨x, hx⟩
              exact dif_neg hx
            apply Continuous.comp
            · exact g.hom.continuous_toFun
            · apply Continuous.comp (by fun_prop)
              rw [IsEmbedding.subtypeVal.isInducing.continuous_iff]
              exact continuous_subtype_val
          · change IsOpen (Set.range c.inl)ᶜ
            rw [← eq_compl_iff_isCompl.mpr h₃.symm]
            exact h₂.isOpen_range

Goal state after: