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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
⊢ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x (P₁ ⊗ P₂) ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯ ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂) ⋯ ▷ Φ.presheafFiber.obj P₃ ≫
        (α_ (Φ.presheafFiber.obj P₁) (Φ.presheafFiber.obj P₂) (Φ.presheafFiber.obj P₃)).hom =
    Φ.presheafFiber.map (α_ P₁ P₂ P₃).hom ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x (P₂ ⊗ P₃)) ⋯ ≫
        Φ.presheafFiber.obj P₁ ◁ Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (p.op.toLoc ≫ (f' i₂).op.toLoc) ≫ f₂.op.toLoc = p.op.toLoc ≫ q.op.toLoc

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
x✝ : Cᵒᵖ ⥤ A
⊢ (λ_ (Φ.presheafFiber.obj x✝)).inv =
    Φ.presheafFiber.map (λ_ x✝).inv ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A)) ⊗ₘ Φ.toPresheafFiber X x x✝) ⋯ ≫
        Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯ ▷ Φ.presheafFiber.obj x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₁)).op.toLoc ≫ (p' i₁).op.toLoc = p.op.toLoc ≫ (f' i₁).op.toLoc

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (f (α i₂)).op.toLoc ≫ (p' i₂).op.toLoc = p.op.toLoc ≫ (f' i₂).op.toLoc

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
x✝ : Cᵒᵖ ⥤ A
⊢ (ρ_ (Φ.presheafFiber.obj x✝)).inv =
    Φ.presheafFiber.map (ρ_ x✝).inv ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x x✝ ⊗ₘ Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A))) ⋯ ≫
        Φ.presheafFiber.obj x✝ ◁ Φ.presheafFiberDesc (fun x x_1 ↦ 𝟙 ((𝟙_ (Cᵒᵖ ⥤ A)).obj (Opposite.op x))) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : MonoidalCategory A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
X : C
x : Φ.fiber.obj X
⊢ LaxMonoidal.ε Φ.presheafFiber = Φ.toPresheafFiber X x (𝟙_ (Cᵒᵖ ⥤ A))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝⁵ : Category.{v', u'} A
inst✝⁴ : MonoidalCategory A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
X : C
x : Φ.fiber.obj X
G₁ G₂ : Cᵒᵖ ⥤ A
⊢ (Φ.toPresheafFiber X x G₁ ⊗ₘ Φ.toPresheafFiber X x G₂) ≫ LaxMonoidal.μ Φ.presheafFiber G₁ G₂ =
    Φ.toPresheafFiber X x (G₁ ⊗ G₂)

Tactic:
by

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

Goal state before:
pp: case hunique
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ y₁.app (op Y) ≫ G.map Z.hom.op = y₂.app (op Y) ≫ G.map Z.hom.op

Tactic:
refine (y₁.naturality φ.op).symm.trans (Eq.trans ?_ (y₂.naturality φ.op))

Goal state after:
case hunique
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y₁ y₂ : (presheafHom F G).obj (op X)
hy₁ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₁.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
hy₂ : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y₂.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : Over X
Z : Over Y.left
hZ : (Sieve.pullback Y.hom S).arrows Z.hom
φ : Over.mk (Z.hom ≫ Y.hom) ⟶ Y := Over.homMk Z.hom ⋯
⊢ ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₁.app (op (Over.mk (Z.hom ≫ Y.hom))) =
    ((Over.forget (unop (op X))).op ⋙ F).map φ.op ≫ y₂.app (op (Over.mk (Z.hom ≫ Y.hom)))
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
⊢ Presieve.IsSheafFor (presheafHom F G) S.arrows

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
M : ↑(F.obj { as := op S })
Y : C
q : Y ⟶ S'
i₁ i₂ : ι'
f₁ : Y ⟶ X' i₁
f₂ : Y ⟶ X' i₂
hf₁ : f₁ ≫ f' i₁ = q
hf₂ : f₂ ≫ f' i₂ = q
⊢ (F.map f₁.op.toLoc).toFunctor.map ((Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M).hom ≫
      (((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').obj M).hom q f₁ f₂ ⋯ ⋯ =
    ((F.toDescentData f ⋙ pullFunctor F w).obj M).hom q f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map ((Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app M).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X : Cᵒᵖ
⊢ ↾(J.overMapPullback A (𝟙 X).unop).map = 𝟙 ((J.overPullback A (unop X)).obj F ⟶ (J.overPullback A (unop X)).obj G)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F✝ G✝ : Cᵒᵖ ⥤ A
F G : Sheaf J A
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾(J.overMapPullback A (f ≫ g).unop).map = ↾(J.overMapPullback A f.unop).map ≫ ↾(J.overMapPullback A g.unop).map

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f✝ : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f✝ (α j) = f' j ≫ p
X✝ Y✝ : ↑(F.obj { as := op S })
f : X✝ ⟶ Y✝
⊢ (F.toDescentData f✝ ⋙ pullFunctor F w).map f ≫
      (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app Y✝) ⋯).hom =
    (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app X✝) ⋯).hom ≫
      ((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
inst✝¹² : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹¹ : Category.{v', u'} A
inst✝¹⁰ : MonoidalCategory A
inst✝⁹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁸ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁷ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁶ : ConcreteCategory A FC
inst✝⁵ : HasWeakSheafify J A
inst✝⁴ : (forget A).ReflectsIsomorphisms
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝ : J.HasSheafCompose (forget A)
X₁✝ X₂✝ Y₁✝ Y₂✝ : Cᵒᵖ ⥤ A
f : X₁✝ ⟶ X₂✝
g : Y₁✝ ⟶ Y₂✝
hf : J.W f
hg : J.W g
⊢ J.W (f ⊗ₘ g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.IsMonoidalW

Goal state before:
pp: C : Type u
inst✝¹⁴ : Category.{v, u} C
inst✝¹³ : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹² : Category.{v', u'} A
inst✝¹¹ : MonoidalCategory A
inst✝¹⁰ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁹ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁸ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁷ : ConcreteCategory A FC
inst✝⁶ : HasWeakSheafify J A
inst✝⁵ : (forget A).ReflectsIsomorphisms
inst✝⁴ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝³ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : J.HasEnoughPoints
⊢ J.W.IsMonoidal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₂ ≫ f' j₂ = f₁ ≫ f' j₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ (f₁ ≫ f' j₁) ≫ p = q ≫ p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₁ ≫ p' j₁ = f₁ ≫ p' j₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₁ ≫ p'' j₁ = f₁ ≫ p'' j₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₂ ≫ p' j₂ = f₂ ≫ p' j₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₂ ≫ p'' j₂ = f₂ ≫ p'' j₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₁ ≫ p' j₁ ≫ f (α j₁) = q ≫ p

Tactic:
by rw [w, reassoc_of% hf₁]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ p'' j₁ ≫ f (β j₁) = p' j₁ ≫ f (α j₁)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
⊢ p'' j₂ ≫ f (β j₂) = p' j₂ ≫ f (α j₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q : Y ⟶ S') ⦃i₁ i₂ : ι'⦄ (f₁ : Y ⟶ X' i₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' i₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' i₁ ≫ f (α i₁)) (p' i₁) (p'' i₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
⊢ ∀ {X_1 : Over X},
    ∀ R ∈ (J.over X) X_1,
      ∀ (x_1 : (FunctorToTypes.fromOverFunctor Φ.fiber x).obj X_1),
        ∃ Y f,
          ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = x_1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
N : Type u'
inst✝¹ : Category.{v', u'} N
p : N ⥤ C
inst✝ : InitiallySmall N
X : C
x : (fiber p).obj X
⊢ ∃ U f, fiberMk f = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X✝ Y✝ : F.DescentData f
φ : X✝ ⟶ Y✝
j : ι'
⊢ p'' j ≫ f (β j) = p' j ≫ f (α j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X✝ Y✝ : F.DescentData f
φ : X✝ ⟶ Y✝
⊢ (pullFunctor F w).map φ ≫ (isoMk (fun j ↦ Y✝.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯).hom =
    (isoMk (fun j ↦ X✝.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯).hom ≫ (pullFunctor F w').map φ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
U : C
f : F.obj U ⟶ X
V : C
g : V ⟶ U
hg : (Sieve.functorPullback F (Sieve.pullback f R)).arrows g
v : Φ.fiber.obj V
⊢ 𝟙 (F.obj (Φ.fiber.elementsMk V v).fst) ≫ F.map g ≫ f = F.map ↑⟨g, ⋯⟩ ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
⊢ ∀ (j : ι), 𝟙 (X j) ≫ f j = f j ≫ 𝟙 S

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Map

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
J : GrothendieckTopology C
Φ : J.Point
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsCocontinuous J K
X : D
R : Sieve X
hR : R ∈ K X
u : Φ.fiber.Elements
f : (CategoryOfElements.π Φ.fiber ⋙ F).obj u ⟶ X
⊢ ∃ Y g, ∃ (_ : R.arrows g), ∃ v q a, a ≫ g = F.map ↑q ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
N : Type u'
inst✝² : Category.{v', u'} N
p : N ⥤ C
inst✝¹ : InitiallySmall N
inst✝ : IsCofiltered N
U : N
X : C
f₁ f₂ : p.obj U ⟶ X
hf : fiberMk f₁ = fiberMk f₂
⊢ ∃ V g, p.map g ≫ f₁ = p.map g ≫ f₂

Tactic:
by

Goal state after: