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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ≤ (pullback g (ofArrows X f)).arrows

Tactic:
]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Presieve.ofArrows P p₁ ≤ (pullback g (ofArrows X f)).arrows
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (y : FirstObj P X),
      (ConcreteCategory.hom (firstMap P X π)) y = (ConcreteCategory.hom (secondMap P X π)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P X π)) x = y

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (y : FirstObj P X),
      (ConcreteCategory.hom (firstMap P X π)) y = (ConcreteCategory.hom (secondMap P X π)) y →
        ∃! x, (ConcreteCategory.hom (forkMap P X π)) x = y
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (b : S.functor ⟶ P), ∃! a, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a = S.shrinkFunctorIsoFunctor.homFromEquiv.symm b) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
⊢ (∀ (b : S.functor ⟶ P), ∃! a, (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ a = S.shrinkFunctorIsoFunctor.homFromEquiv.symm b) ↔
    ∀ (f : S.functor ⟶ P), ∃! g, S.functorInclusion ≫ g = f
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
]

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op), a = b
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! b,
      (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (shrinkYonedaIsoYoneda.app X).homFromEquiv.symm b =
        S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
⊢ (∃! b,
      (shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (shrinkYonedaIsoYoneda.app X).homFromEquiv.symm b =
        S.shrinkFunctorIsoFunctor.homFromEquiv.symm a) ↔
    ∃! g, S.functorInclusion ≫ g = a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ULift.{w', w} ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ (hom ((shrinkYoneda.{max w w', v₁, u₁}.obj X).map f.unop.op))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down)) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
inst✝¹ : LocallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{max w' w, v₁, u₁} C
U V : Cᵒᵖ
f : U ⟶ V
x✝ : ULift.{w', w} ↑{f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ (hom ((shrinkYoneda.{max w w', v₁, u₁}.obj X).map f.unop.op))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down)) =
    (hom ((shrinkYoneda.{max w' w, v₁, u₁}.obj X).map f))
      (shrinkYonedaObjObjEquiv.symm (shrinkYonedaObjObjEquiv ↑x✝.down))
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      (ConcreteCategory.hom (firstMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) =
          (ConcreteCategory.hom (secondMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            ((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∀ (a : (j : I) → P.obj (op (X j))),
      (ConcreteCategory.hom (firstMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) =
          (ConcreteCategory.hom (secondMap P X π))
            (((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a) →
        ∃! x,
          (ConcreteCategory.hom (forkMap P X π)) x =
            ((equivShrink ((j : I) → P.obj (op (X j)))).trans
                (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm)
              a
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
⊢ ∀ (a b : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op), a = b

Tactic:
intro f₁ f₂

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
⊢ f₁ = f₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
⊢ (∀ (x : Cᵒᵖ),
      ((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
          x =
        (S.shrinkFunctorIsoFunctor.hom ≫ a).app x) ↔
    ∀ (x : Cᵒᵖ), (S.functorInclusion ≫ b).app x = a.app x

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
⊢ (∀ (x : Cᵒᵖ),
      ((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫ (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
          x =
        (S.shrinkFunctorIsoFunctor.hom ≫ a).app x) ↔
    ∀ (x : Cᵒᵖ), (S.functorInclusion ≫ b).app x = a.app x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } :=
  conesEquivSieveCompatibleFamily P S (op E)
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := homEquivAmalgamation ⋯
⊢ f₁ = f₂

Tactic:
apply eqv'.injective

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
h : ∀ (E : Aᵒᵖ), IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows
E : A
π : (Functor.const S.arrows.categoryᵒᵖ).obj E ⟶ S.arrows.diagram.op ⋙ P
eqv : (S.arrows.diagram.op ⋙ P).cones.obj (op E) ≃ { x // x.SieveCompatible } := ⋯
f₁ f₂ : { pt := E, π := eqv.invFun (eqv.toFun π) } ⟶ P.mapCone S.arrows.cocone.op
eqv' : (⋯.cone ⟶ P.mapCone S.arrows.cocone.op) ≃ { t // (↑(eqv π)).IsAmalgamation t } := ⋯
⊢ eqv' f₁ = eqv' f₂
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
S : Presieve X
⊢ map F S ≤ map F S

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a✝),
      (ConcreteCategory.hom
            (((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫
                  (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
              a✝))
          x =
        (ConcreteCategory.hom ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝)) x) ↔
    ∀ (x : S.functor.obj a✝),
      (ConcreteCategory.hom ((S.functorInclusion ≫ b).app a✝)) x = (ConcreteCategory.hom (a.app a✝)) x

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
P : Cᵒᵖ ⥤ Type v₁
a : S.functor ⟶ P
b : yoneda.obj X ⟶ P
a✝ : Cᵒᵖ
⊢ (∀ (x : (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.obj a✝),
      (ConcreteCategory.hom
            (((shrinkFunctor.{v₁, v₁, u₁} S).ι ≫
                  (NatIso.ofComponents (fun Y ↦ shrinkYonedaObjObjEquiv.toIso) ⋯).hom ≫ b).app
              a✝))
          x =
        (ConcreteCategory.hom ((S.shrinkFunctorIsoFunctor.hom ≫ a).app a✝)) x) ↔
    ∀ (x : S.functor.obj a✝),
      (ConcreteCategory.hom ((S.functorInclusion ≫ b).app a✝)) x = (ConcreteCategory.hom (a.app a✝)) x
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
T W : C
v : T ⟶ W
v' : W ⟶ X
hv' : (Sieve.ofArrows Z f).arrows v'
S : C
u : T ⟶ S
u' : S ⟶ Z (Sieve.ofArrows.i hv')
h : R (Sieve.ofArrows.i hv') u'
hu : u ≫ u' = v ≫ Sieve.ofArrows.h hv'
⊢ (Sieve.generate (bindOfArrows Z f R)).arrows (u ≫ u' ≫ f (Sieve.ofArrows.i hv'))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R),
      (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
        (x.Compatible → ∃ t, x.IsAmalgamation t)) ↔
    IsSheafFor P R

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R),
      (∀ (t₁ t₂ : P.obj (op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂) ∧
        (x.Compatible → ∃ t, x.IsAmalgamation t)) ↔
    IsSheafFor P R
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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ ((unop W).index P).snd i ≫ η.app (op i.r.Z) =
    Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ P.map i.r.g₂.op ≫ η.app (op i.r.Z)

Tactic:
]

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✝ P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : C
W : (J.Cover X)ᵒᵖ
i : (unop W).shape.R
⊢ Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ ((unop W).index P).snd i ≫ η.app (op i.r.Z) =
    Multiequalizer.ι ((unop W).index P) ((unop W).shape.snd i) ≫ P.map i.r.g₂.op ≫ η.app (op i.r.Z)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
        ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
      x

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
        ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
      x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
t : IsSeparatedFor P R
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSheafFor P (generate R).arrows

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSheafFor P (generate R).arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ (Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop X)).map e.inv.op) ≫
      colimit.ι (J.diagram P (unop X)) (op (unop S)) =
    colimit.ι (J.diagram P (unop X)) S

Tactic:
]

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 : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ (Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
          (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
        (J.diagram P (unop X)).map e.inv.op) ≫
      colimit.ι (J.diagram P (unop X)) (op (unop S)) =
    colimit.ι (J.diagram P (unop X)) S
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
I : Type u_1
S : C
X : I → C
f : (i : I) → X i ⟶ S
hf : ofArrows X f ∈ J S
E : A
x y : E ⟶ P.obj (op S)
h : ∀ (i : I), x ≫ P.map (f i).op = y ≫ P.map (f i).op
Z Y : C
i : I
g : Z ⟶ X i
⊢ y ≫ P.map (f i).op ≫ P.map g.op = y ≫ P.map (f i).op ≫ P.map g.op

Tactic:
]

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
    x
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t =
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) i

Tactic:
]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
q :
  (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
    x
i : I
⊢ (ConcreteCategory.hom (P.map (π i).op)) t =
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
      ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) i
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ Presheaf.IsSheaf J P → Presieve.IsSheaf J P

Tactic:
intro hP

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presheaf.IsSheaf J P
⊢ Presieve.IsSheaf J P
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf J P → Presheaf.IsSheaf J P

Tactic:
intro hP

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
⊢ Presheaf.IsSheaf J P
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (generate (singleton (𝟙 X))).arrows
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor P (singleton (𝟙 X))
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H : (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ (ConcreteCategory.hom (F.map (PullbackCone.IsLimit.lift hc p₁ p₂ h).op)) ((ConcreteCategory.hom (F.map c.snd.op)) x) =
    (ConcreteCategory.hom (F.map p₂.op)) x

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
x : F.obj (op X)
H : (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
Z : C
p₁ p₂ : Z ⟶ X
h : p₁ ≫ f = p₂ ≫ f
⊢ (ConcreteCategory.hom (F.map (PullbackCone.IsLimit.lift hc p₁ p₂ h).op)) ((ConcreteCategory.hom (F.map c.snd.op)) x) =
    (ConcreteCategory.hom (F.map p₂.op)) x