mathlib-initiative/mathlib-tactics huggingface dataset:
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
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ x✝¹ ⊗ₘ x✝ = x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
X✝ : Cᵒᵖ
⊢ (x✝¹ ⊗ₘ x✝).app X✝ = (x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝).app X✝
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
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ 𝟙 x✝¹ ⊗ₘ 𝟙 x✝ = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (𝟙 x✝¹ ⊗ₘ 𝟙 x✝).app X✝ = (𝟙 (x✝¹ ⊗ x✝)).app X✝
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
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ (x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝) = x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
X✝ : Cᵒᵖ
⊢ ((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝
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
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
⊢ ((x✝² ⊗ₘ x✝¹) ⊗ₘ x✝) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom = (α_ X₁✝ X₂✝ X₃✝).hom ≫ (x✝² ⊗ₘ x✝¹ ⊗ₘ x✝)

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : X₃✝ ⟶ Y₃✝
X✝ : Cᵒᵖ
⊢ (((x✝² ⊗ₘ x✝¹) ⊗ₘ x✝) ≫ (α_ Y₁✝ Y₂✝ Y₃✝).hom).app X✝ = ((α_ X₁✝ X₂✝ X₃✝).hom ≫ (x✝² ⊗ₘ x✝¹ ⊗ₘ x✝)).app X✝
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
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom = (λ_ X✝).hom ≫ x✝

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ◁ x✝ ≫ (λ_ Y✝).hom).app X✝ = ((λ_ X✝¹).hom ≫ x✝).app X✝
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
X✝ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝ ⟶ Y✝
⊢ x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom = (ρ_ X✝).hom ≫ x✝

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X✝¹ Y✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝ : X✝¹ ⟶ Y✝
X✝ : Cᵒᵖ
⊢ (x✝ ▷ 𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)) ≫ (ρ_ Y✝).hom).app X✝ = ((ρ_ X✝¹).hom ≫ x✝).app X✝
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
x✝³ x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom =
    (α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝³ x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom).app X✝ =
    ((α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom).app X✝
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
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝¹ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom = (ρ_ x✝¹).hom ▷ x✝

Tactic:
ext1

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((α_ x✝¹ (𝟙_ (PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat))) x✝).hom ≫ x✝¹ ◁ (λ_ x✝).hom).app X✝ =
    ((ρ_ x✝¹).hom ▷ x✝).app X✝
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (f.app (op X) ≫ Q.map g.op)) t = (ConcreteCategory.hom (f.app (op Y))) (x g hg)

Tactic:
← f.naturality,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (P.map g.op ≫ f.app (op Y))) t = (ConcreteCategory.hom (f.app (op Y))) (x g hg)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f

Tactic:
ext Y ⟨u, hu⟩

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
S : Sieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
h :
  ∀ ⦃Y : C⦄ (f_1 : Y ⟶ X) (h : S.arrows f_1),
    (ConcreteCategory.hom (F.map f_1.op)) (shrinkYonedaEquiv g) =
      (ConcreteCategory.hom (f.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f_1, ⋯⟩
Y : Cᵒᵖ
u : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hu : u ∈ (shrinkFunctor.{w, v₁, u₁} S).obj Y
⊢ (ConcreteCategory.hom (((shrinkFunctor.{w, v₁, u₁} S).ι ≫ g).app Y)).toFun ⟨u, hu⟩ =
    (ConcreteCategory.hom (f.app Y)).toFun ⟨u, hu⟩
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
⊢ ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
    colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op

Tactic:
intro X Y Z f g

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)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ colimMap (J.diagramPullback P (f ≫ g).unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback (f ≫ g).unop).op =
    (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
      colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: 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
x : P.obj (op B)
hx : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) x = y i
right✝ :
  ∀ (y_1 : (fun X ↦ X) (P.obj (op B))),
    (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = y i) y_1 → y_1 = x
⊢ Arrows.toCompatible P π x = ⟨y, hy⟩

Tactic:
ext; apply hx

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _),
      ← isIso_iff_of_reflects_iso _ ((whiskeringRight Cᵒᵖ A B).obj F)]
    change IsIso ((sheafToPresheaf _ _).map ((sheafCompose J F).map f))
    infer_instance

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
s : FamilyOfElements P (Sieve.bind U.arrows B).arrows
hs : s.Compatible
y : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → (hf : U.arrows f) → FamilyOfElements P (B hf).arrows := fun Y f hf Z g hg ↦ s (g ≫ f) ⋯
hy : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).Compatible
t : FamilyOfElements P U.arrows := fun Y f hf ↦ ⋯.amalgamate (y hf) ⋯
ht : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), (y hf).IsAmalgamation (t f hf)
Z W : C
f : Z ⟶ X
h : W ⟶ Z
hf : U.arrows f
Y : C
l : Y ⟶ W
hl : (B ⋯).arrows l
M : C
m : M ⟶ Y
hm : (Sieve.pullback (l ≫ h) (B hf)).arrows m
⊢ (Sieve.bind U.arrows B).arrows (m ≫ l ≫ h ≫ f)

Tactic:
simpa using (bind_comp f hf hm : Sieve.bind U B _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImage f ≫ imageι f = f

Tactic:
ext1

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImage f ≫ imageι f).hom = f.hom
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 (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ { hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) } ≫ I.m = (imageMonoFactorization f).m

Tactic:
ext1

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 (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ ({ hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) } ≫ I.m).hom = (imageMonoFactorization f).m.hom
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ { hom := (isoSheafify J ⋯).hom } ≫ { hom := (isoSheafify J ⋯).inv } = 𝟙 P

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ({ hom := (isoSheafify J ⋯).hom } ≫ { hom := (isoSheafify J ⋯).inv }).hom = (𝟙 P).hom
Module: Mathlib.CategoryTheory.Sites.Sheafification

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ { hom := (isoSheafify J ⋯).inv } ≫ { hom := (isoSheafify J ⋯).hom } = 𝟙 ((presheafToSheaf J D).obj P.obj)

Tactic:
ext1

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
inst✝ : HasWeakSheafify J D
P : Sheaf J D
⊢ ({ hom := (isoSheafify J ⋯).inv } ≫ { hom := (isoSheafify J ⋯).hom }).hom = (𝟙 ((presheafToSheaf J D).obj P.obj)).hom
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✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
W : J.Cover X
⊢ ∀ (E_1 : Multifork (W.index E.pt)) (i : W.shape.L),
    (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).lift (multiforkEvaluationCone F E X W E_1) ≫
        (W.multifork E.pt).ι i =
      E_1.ι i

Tactic:
intro S i
      apply (isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op i.Y)) hE).hom_ext
      intro k
      dsimp [Multifork.ofι]
      erw [Category.assoc, (E.π.app k).naturality]
      dsimp
      rw [← Category.assoc]
      erw [(isLimitOfPreserves ((evaluation Cᵒᵖ D).obj (op X)) hE).fac
        (multiforkEvaluationCone F E X W S)]
      dsimp [multiforkEvaluationCone, Presheaf.isLimitOfIsSheaf]
      rw [Presheaf.IsSheaf.amalgamate_map]

Goal state after:
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
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
      { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) } =
    S.ι.app j

Tactic:
ext1

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
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
j : K
⊢ ({ pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
        { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) }).hom =
    (S.ι.app j).hom
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
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.pt ⟶ S.pt
hm :
  ∀ (j : K),
    { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
        m =
      S.ι.app j
⊢ m = { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) }

Tactic:
ext1

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
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
S : Cocone F
m : { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.pt ⟶ S.pt
hm :
  ∀ (j : K),
    { pt := { obj := E.pt, property := ⋯ }, ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }.ι.app j ≫
        m =
      S.ι.app j
⊢ m.hom = { hom := hE.desc ((sheafToPresheaf J D).mapCocone S) }.hom
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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ { toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
          right_inv := ⋯ }.symm
      (η ≫ γ) =
    (plusPlusSheaf J D).map η ≫
      { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        γ

Tactic:
ext1

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✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
P Q : Cᵒᵖ ⥤ D
R : Sheaf J D
η : P ⟶ Q
γ : Q ⟶ (sheafToPresheaf J D).obj R
⊢ ({ toFun := fun e ↦ J.toSheafify P ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }.symm
        (η ≫ γ)).hom =
    ((plusPlusSheaf J D).map η ≫
        { toFun := fun e ↦ J.toSheafify Q ≫ e.hom, invFun := fun e ↦ { hom := J.sheafifyLift e ⋯ }, left_inv := ⋯,
              right_inv := ⋯ }.symm
          γ).hom
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
        (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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

Goal state before:
pp: case mp.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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ CommSq (F'.map WalkingSpan.Hom.fst) (F'.map WalkingSpan.Hom.snd) (c'.ι.app WalkingSpan.left)
    (c'.ι.app WalkingSpan.right)

pp: case mp.refine_5
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)

Tactic:
· exact ⟨by simp⟩

Goal state after:
case mp.refine_5
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 : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
⊢ IsPullback (c'.ι.app WalkingSpan.left) (α.app WalkingSpan.left) fα h ∧
      IsPullback (c'.ι.app WalkingSpan.right) (α.app WalkingSpan.right) fα i ↔
    ∀ (j : WalkingSpan), IsPullback (c'.ι.app j) (α.app j) fα ((PushoutCocone.mk h i ⋯).ι.app j)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.mpr
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' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
inst✝ : HasPullback αX f
⊢ (∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i') →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
· intro ⟨W', f', g', αW, hf, hg, H''⟩
      rwa [← H' f' g' h' i' αW αX αY αZ hf hg sq_h sq_i H''.toCommSq]

Goal state after: