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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ F.obj.map I.f.op ≫ f.hom.app (op I.Y) ≫ inv (f.hom.app (op I.Y)) = F.obj.map I.f.op

Tactic:
simp

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
invMap : G.obj.obj (op (unop W)) ⟶ F.obj.obj (op (unop W)) :=
  ⋯.amalgamate S (fun I ↦ G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ⋯
I : S.Arrow
⊢ (G.obj.map I.f.op ≫ inv (f.hom.app (op I.Y))) ≫ f.hom.app (op I.Y) = G.obj.map I.f.op

Tactic:
simp

Goal state after:
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 Y : C
g : Y ⟶ X
α : (presheafHom F G).obj (op X)
⊢ 𝟙 Y ≫ g = g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ D₁.hom (p ≫ q) (p ≫ f₁) (g ≫ p' j) ⋯ ⋯ ≫
      pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₁) ⋯ ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      ((F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₁) ≫
          D₁.hom (p ≫ q) (p ≫ f₁) (p ≫ f₂) ⋯ ⋯ ≫
            (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₂)) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (D₁.hom (p ≫ q) (p ≫ f₂) (g ≫ p' j) ⋯ ⋯ ≫
                pullHom (φ.hom j) g (g ≫ p' j) (g ≫ p' j) ⋯ ⋯ ≫ D₂.hom (p ≫ q) (g ≫ p' j) (p ≫ f₂) ⋯ ⋯) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) ≫
              D₂.hom (p ≫ q) (p ≫ f₂) (p ≫ f₁) ⋯ ⋯ ≫
                (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₁)) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
simp

Goal state after:
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
⊢ 𝟙 W.left ≫ W.hom ≫ g = W.hom ≫ g

Tactic:
simp

Goal state after:
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
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
H : x (W.hom ≫ g) ⋯ = (ConcreteCategory.hom ((presheafHom F G).map W.hom.op)) (x g hg)
⊢ 𝟙 W.left ≫ W.hom = W.hom

Tactic:
simp

Goal state after:
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)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
⊢ Over.Hom.left f ≫ Z₁.hom ≫ g = 𝟙 Z₂.left ≫ Z₂.hom ≫ g

Tactic:
simp

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'
j : ι'
g : Y ⟶ X' j
hg : g ≫ f' j = q
⊢ (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j)) ≫
      𝟙 ((F.map (g ≫ p' j).op.toLoc).toFunctor.obj (D.obj (α j))) ≫
        (F.mapComp' (p' j).op.toLoc g.op.toLoc (g ≫ p' j).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j)) =
    𝟙 ((F.map g.op.toLoc).toFunctor.obj ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))))

Tactic:
simp

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'
j₁ j₂ j₃ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
f₃ : Y ⟶ X' j₃
hf₁ : f₁ ≫ f' j₁ = q
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₃)) =
    (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:
simp

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
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j j' : (Over (unop (op X)))ᵒᵖ
φ : j ⟶ j'
⊢ ((Under.mk (unop j).hom.op).hom ≫ (Over.Hom.left φ.unop).op).unop = (Under.mk (unop j').hom.op).hom.unop

Tactic:
simp

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
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ ((Under.Hom.right φ).unop ≫ (Over.mk j.hom.unop).hom).op = (Over.mk j'.hom.unop).hom.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ : OneCochain G U
x✝⁴ x✝³ : I
x✝² : C
x✝¹ : x✝² ⟶ U x✝⁴
x✝ : x✝² ⟶ U x✝³
⊢ (ConcreteCategory.hom (G.map x✝¹.op)) (1 x✝⁴) * γ.ev x✝⁴ x✝³ x✝¹ x✝ =
    γ.ev x✝⁴ x✝³ x✝¹ x✝ * (ConcreteCategory.hom (G.map x✝.op)) (1 x✝³)

Tactic:
simp

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
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
⊢ (fun g ↦ end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯)
      ((fun f ↦
          {
            app := fun j ↦
              uncurry
                (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
            naturality := ⋯ })
        f) =
    f

Tactic:
by
    dsimp
    ext j
    dsimp
    simp only [curry_uncurry, end_.lift_π]
    rfl

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

Goal state before:
pp: case e_a
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₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ Z.hom ≫ Y₂.hom = (Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom

Tactic:
simp

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

Goal state before:
pp: case h
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
Φ : K.Point
F : C ⥤ D
inst✝¹ : RepresentablyFlat F
J : GrothendieckTopology C
hF : CoverPreserving J K F
inst✝ : InitiallySmall (F ⋙ Φ.fiber).Elements
X : C
R : Sieve X
hR : R ∈ J X
Y : D
W : C
g : W ⟶ X
h : Y ⟶ F.obj W
hg : R.arrows g
y : Φ.fiber.obj Y
⊢ (ConcreteCategory.hom ((F ⋙ Φ.fiber).map g)) ((ConcreteCategory.hom (Φ.fiber.map h)) y) =
    (ConcreteCategory.hom (Φ.fiber.map (h ≫ F.map g))) y

Tactic:
simp

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
⊢ Presieve.IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

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.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)
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)))
⊢ 𝟙 Y ≫ g = g

Tactic:
simp

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
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc) ⋯).inv.toNatTrans.app M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M ≫
          (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc ⋯).hom.toNatTrans.app
              ((F.map p.op.toLoc).toFunctor.obj M) ≫
            (F.mapComp' (f' i₂).op.toLoc f₂.op.toLoc q.op.toLoc
                      (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_1 C inst✝ S' ι'
                        X' f' Y q i₂ f₂ hf₂)).inv.toNatTrans.app
              ((F.map p.op.toLoc).toFunctor.obj M) =
    (F.map f₁.op.toLoc).toFunctor.map
        ((F.mapComp' (f (α i₁)).op.toLoc (p' i₁).op.toLoc (p.op.toLoc ≫ (f' i₁).op.toLoc)
                  (@CategoryTheory.Pseudofunctor.DescentData.toDescentDataCompPullFunctorIso._proof_6 C inst✝ ι S X f S'
                    p ι' X' f' α p' w i₁)).inv.toNatTrans.app
          M) ≫
      (F.mapComp' (p.op.toLoc ≫ (f' i₁).op.toLoc) f₁.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).inv.toNatTrans.app M ≫
        (F.mapComp' (f (α i₂)).op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app
            M ≫
          (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
              ((F.map (f (α i₂)).op.toLoc).toFunctor.obj M) ≫
            (F.mapComp' (p' i₂).op.toLoc f₂.op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) ⋯).inv.toNatTrans.app
                ((F.map (f (α i₂)).op.toLoc).toFunctor.obj M) ≫
              (F.mapComp' (f (α i₂)).op.toLoc ((p' i₂).op.toLoc ≫ f₂.op.toLoc) (p.op.toLoc ≫ q.op.toLoc)
                          ⋯).inv.toNatTrans.app
                  M ≫
                (F.mapComp' p.op.toLoc q.op.toLoc (p.op.toLoc ≫ q.op.toLoc) ⋯).hom.toNatTrans.app M

Tactic:
simp

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:
simp

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:
simp

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 U : C
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
hR : ⊤ ∈ ⊥ U
⊢ ⊤.arrows (𝟙 U)

Tactic:
simp

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 U : C
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
hR : ⊤ ∈ ⊥ U
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.flip.obj (op X)).map (𝟙 U))) x = x

Tactic:
simp

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
J : GrothendieckTopology C
U V : N
f : U ⟶ V
⊢ (hom ((fiber p).map (p.map f))) ((fiber p).elementsMk (p.obj U) (fiberMk (𝟙 (p.obj U)))).snd =
    ((fiber p).elementsMk (p.obj V) (fiberMk (𝟙 (p.obj V)))).snd

Tactic:
simp

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
J : GrothendieckTopology C
inst✝ : IsCofiltered N
X : C
U : N
f : p.obj U ⟶ X
⊢ (hom ((fiber p).map f)) ((functor p).obj U).snd = ⟨X, fiberMk f⟩.snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
⊢ (fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) (𝟙 (Opposite.unop (Opposite.op X))) = t₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
ht₁' : t₁ ∈ Q.obj (Opposite.op X)
⊢ (fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂) (𝟙 (Opposite.unop (Opposite.op X))) = t₂

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := ⋯
t : (X : C) → ι X → F.obj (Opposite.op X) := ⋯
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ ↑x = ↑y

Tactic:
apply Option.some_injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := ⋯
t : (X : C) → ι X → F.obj (Opposite.op X) := ⋯
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ some ↑x = some ↑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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (p' j ≫ q' (α j)) ≫ f' (β (α j)) = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
simp

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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ 𝟙 (X (α j)) = p' j

Tactic:
simp

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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ q' (α j) ≫ p' (β (α j)) = p' j ≫ q' (α j) ≫ p' (β (α j))

Tactic:
simp

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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ p' j ≫ f (α j) = p' j ≫ f (α j)

Tactic:
simp

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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X (α j)) ≫ f (α j) = f (α j)

Tactic:
simp

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

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
⊢ discretePresieve α f →
    (ConcreteCategory.hom (S.map f.op)) (typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s))) =
      (ConcreteCategory.hom (S.map f.op)) s

Tactic:
hf

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
⊢ (ConcreteCategory.hom (S.map f.op)) (typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s))) =
    (ConcreteCategory.hom (S.map f.op)) s