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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)
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✝¹ Y✝ : Cᵒᵖ ⥤ A
x✝² : X✝¹ ⟶ Y✝
x✝¹ : Cᵒᵖ ⥤ A
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ (X✝¹ ⊗ x✝¹) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x X✝¹ ⊗ₘ Φ.toPresheafFiber X x x✝¹) ⋯ ≫
        Φ.presheafFiber.map x✝² ▷ Φ.presheafFiber.obj x✝¹ =
    Φ.toPresheafFiber X✝ x✝ (X✝¹ ⊗ x✝¹) ≫
      Φ.presheafFiber.map (x✝² ▷ x✝¹) ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x Y✝ ⊗ₘ Φ.toPresheafFiber X x x✝¹) ⋯

Tactic:
simp [tensorHom_def', ← comp_whiskerRight, ← whisker_exchange_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
inst✝⁶ : MonoidalCategory A
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
inst✝⁴ : G.IsCoverDense J
inst✝³ : G.Full
inst✝² : G.IsContinuous K J
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.W.IsMonoidal
⊢ (K.W.inverseImage ((Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op)).IsMonoidal

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
inst✝⁶ : MonoidalCategory A
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
inst✝⁴ : G.IsCoverDense J
inst✝³ : G.Full
inst✝² : G.IsContinuous K J
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.W.IsMonoidal
⊢ (K.W.inverseImage ((Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op)).IsMonoidal
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 ↦ g ≫ g_1
⊢ Function.Bijective (curry ∘ fun g_1 ↦ F ◁ g ≫ g_1)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 ↦ g ≫ g_1
⊢ Function.Bijective (curry ∘ fun g_1 ↦ F ◁ g ≫ g_1)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
⊢ Function.Bijective (curry ∘ fun g_1 ↦ F ◁ g ≫ g_1)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
⊢ Function.Bijective (curry ∘ fun g_1 ↦ F ◁ g ≫ g_1)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case hex
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 : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
]

Goal state after:
case hex
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 : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: case e'_3
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
e_2✝ : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ g ≫ curry α = g ≫ curry α

Tactic:
]

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₁ = y₂

Tactic:
]

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₁ = y₂
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 ⋯
⊢ ((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)))

Tactic:
]

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
⊢ Presieve.IsSheaf J (presheafHom F G)

Tactic:
]

Goal state after:
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
⊢ Presieve.IsSheaf J (presheafHom F G)
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 : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
hg : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map g)
Φ : P.FullSubcategory
⊢ IsIso
    (Functor.OplaxMonoidal.δ Φ.obj.presheafFiber X₁✝ Y₁✝ ≫
      (Φ.obj.presheafFiber.map f ⊗ₘ Φ.obj.presheafFiber.map g) ≫ Functor.LaxMonoidal.μ Φ.obj.presheafFiber X₂✝ Y₂✝)

Tactic:
]

Goal state after:
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 : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
hg : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map g)
Φ : P.FullSubcategory
⊢ IsIso
    (Functor.OplaxMonoidal.δ Φ.obj.presheafFiber X₁✝ Y₁✝ ≫
      (Φ.obj.presheafFiber.map f ⊗ₘ Φ.obj.presheafFiber.map g) ≫ Functor.LaxMonoidal.μ Φ.obj.presheafFiber X₂✝ Y₂✝)
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
⊢ q ≫ p = q ≫ p

Tactic:
]

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.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p'' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (β j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p'' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p'' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p'' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (β j₂))

Tactic:
]

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
U : Over X
R : Sieve U.left
hR : R ∈ J U.left
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu : (ConcreteCategory.hom (Φ.fiber.map U.hom)) ((ConcreteCategory.hom (Φ.fiber.map f)) v) = x
⊢ (ConcreteCategory.hom (Φ.fiber.map (Over.mk (f ≫ U.hom)).hom)) v = x

Tactic:
]

Goal state after:
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
U : Over X
R : Sieve U.left
hR : R ∈ J U.left
Y : C
f : Y ⟶ U.left
hf : R.arrows f
v : Φ.fiber.obj Y
hu : (ConcreteCategory.hom (Φ.fiber.map U.hom)) ((ConcreteCategory.hom (Φ.fiber.map f)) v) = x
⊢ (ConcreteCategory.hom (Φ.fiber.map (Over.mk (f ≫ U.hom)).hom)) v = x
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
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm S).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ J (Over.mk f).left

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm S).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ J (Over.mk f).left
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
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f).left),
    ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y = x

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f).left),
    ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y = x
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
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ (ConcreteCategory.hom (⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber.map (Over.mk f).hom)) y =
    ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd
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
inst✝² : LocallySmall.{w, v', u'} D
A : Type u''
inst✝¹ : Category.{v'', u''} A
inst✝ : HasColimitsOfSize.{w, w, v'', u''} A
P : Dᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
⊢ Φ.toPresheafFiber X x (F.op ⋙ P) ≫ (Φ.presheafFiberMapObjIso F K P).inv = Φ.toPresheafFiberMap F K P X x

Tactic:
by
  simpa [-toPresheafFiberMap_presheafFiberMapObjIso_hom] using
    (Φ.toPresheafFiberMap_presheafFiberMapObjIso_hom F K ..).symm =≫
      (Φ.presheafFiberMapObjIso F K P).inv

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ ∀ (X_1 : Cᵒᵖ ⥤ A), IsIso (((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).app X_1)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
X : C
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : HasColimitsOfSize.{w, w, u_2, u_1} A
⊢ ∀ (X_1 : Cᵒᵖ ⥤ A), IsIso (((pointBot X).toPresheafFiberNatTrans X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).app X_1)
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : Small.{w, u} C
⊢ ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} (pointsBot C)

Tactic:
dsimp [pointsBot]
  infer_instance

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
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 ((F.mapId { as := op (X i₁) }).hom.toNatTrans.app (D.obj i₁)) ≫ D.hom q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (𝟙 (X i₁)).op.toLoc f₁.op.toLoc f₁.op.toLoc ⋯).inv.toNatTrans.app (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        (F.mapComp' (𝟙 (X i₂)).op.toLoc f₂.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (D.obj i₂) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₂) }).hom.toNatTrans.app (D.obj i₂))

Tactic:
]

Goal state after:
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
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 ((F.mapId { as := op (X i₁) }).hom.toNatTrans.app (D.obj i₁)) ≫ D.hom q f₁ f₂ ⋯ ⋯ =
    (F.mapComp' (𝟙 (X i₁)).op.toLoc f₁.op.toLoc f₁.op.toLoc ⋯).inv.toNatTrans.app (D.obj i₁) ≫
      D.hom q f₁ f₂ ⋯ ⋯ ≫
        (F.mapComp' (𝟙 (X i₂)).op.toLoc f₂.op.toLoc f₂.op.toLoc ⋯).hom.toNatTrans.app (D.obj i₂) ≫
          (F.map f₂.op.toLoc).toFunctor.map ((F.mapId { as := op (X i₂) }).hom.toNatTrans.app (D.obj i₂))
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b) =
    shrinkYonedaObjObjEquiv.symm (𝟙 X)
⊢ shrinkYonedaObjObjEquiv.symm (b ≫ a) = shrinkYonedaObjObjEquiv.symm (b ≫ a)

Tactic:
]

Goal state after: