mathlib-initiative/mathlib-tactics huggingface dataset:
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 : C
f : X ⟶ Y
S : Sieve (F.obj Y)
⊢ functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)

Tactic:
by

Goal state after:
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
h : ∃ t, x.IsAmalgamation t
⊢ x.Compatible

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))

Tactic:
by

Goal state after:
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
R : Presieve X
Y : D
X' : C
f' : Y ⟶ F.obj X'
X'' : C
g' : X' ⟶ X''
f'' : X'' ⟶ X
h₁ : R f''
⊢ f' ≫ F.map (g' ≫ f'') = (f' ≫ F.map g') ≫ F.map f''

Tactic:
by

Goal state after:
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
R : Presieve X
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R

Tactic:
by

Goal state after:
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 : P.obj (op X)
ht : x.IsAmalgamation t
⊢ x.sieveExtend.IsAmalgamation t

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : X ⟶ Y
x : FamilyOfElements P (singleton f)
y : P.obj (op Y)
⊢ x.IsAmalgamation y ↔ (ConcreteCategory.hom (P.map f.op)) y = x f ⋯

Tactic:
by

Goal state after:
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✝
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X✝
Y✝ Z✝ : D
g : Z✝ ⟶ Y✝
X : C
α : X ⟶ X✝
β : Y✝ ⟶ F.obj X
hα : R.arrows α
⊢ g ≫ β ≫ F.map α = (g ≫ β) ≫ F.map α

Tactic:
by

Goal state after:
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ ∀ {Y Z : D} {f : Y ⟶ F.obj X},
    Presieve.functorPushforward F R.arrows f → ∀ (g : Z ⟶ Y), Presieve.functorPushforward F R.arrows (g ≫ f)

Tactic:
by

Goal state after:
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
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)

Tactic:
by

Goal state after:
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
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ functorPushforward F (ofArrows Y f) = ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ : C
R : Sieve X✝
X : C
f : X ⟶ (𝟭 C).obj X✝
hf : R.arrows f
⊢ f = 𝟙 X ≫ (𝟭 C).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPushforward (𝟭 C) R = R

Tactic:
by

Goal state after:
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
⊢ Presieve.FamilyOfElements.Compatible ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x) ↔
    (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x

Tactic:
by

Goal state after:
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
⊢ GaloisConnection (functorPushforward F) (functorPullback F)

Tactic:
by

Goal state after:
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
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)

Tactic:
by

Goal state after:
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
⊢ functorPushforward F ⊤ = ⊤

Tactic:
by

Goal state after:
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
R : Sieve X
V : C
f : V ⟶ X
h : R.arrows f
⊢ F.map f = 𝟙 (F.obj V) ≫ F.map f

Tactic:
by

Goal state after:
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 ↔ IsSeparatedFor P (generate R).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ ⊤ (𝟙 X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
q₁ : (ConcreteCategory.hom (P.map (𝟙 X).op)) t₁ = x (𝟙 X) trivial
⊢ ⊤ (𝟙 X)

Tactic:
by

Goal state after:
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 : C
f : Y ⟶ X
S : Sieve X
⊢ functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P ⊤
t₁ t₂ : P.obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ shrinkYonedaObjObjEquiv.symm f ∈ (shrinkFunctor.{w, v₁, u₁} S).obj (op Y)

Tactic:
by

Goal state after:
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✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.EssSurj
inst✝ : F.Full
X : C
⊢ GaloisInsertion (functorPushforward F) (functorPullback F)

Tactic:
by

Goal state after:
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
X✝ : C
S : Sieve X✝
R : Presieve X✝
E : Aᵒᵖ
π : (S.arrows.diagram.op ⋙ P).cones.obj E
X Y : C
f : X ⟶ X✝
g : Y ⟶ X
hf : S.arrows f
⊢ (fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) Y (g ≫ f) ⋯ =
    (ConcreteCategory.hom ((P ⋙ coyoneda.obj E).map g.op))
      ((fun x f h ↦ π.app (op { obj := Over.mk f, property := h })) X f hf)

Tactic:
by

Goal state after:
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
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : { x // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
⊢ (unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).map g ≫ ↑x (unop f').obj.hom ⋯ =
    ↑x (unop f).obj.hom ⋯ ≫ (S.arrows.diagram.op ⋙ P).map g

Tactic:
by

Goal state after:
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✝
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ GaloisCoinsertion (functorPushforward F) (functorPullback F)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
⊢ FamilyOfElements.Compatible fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩

Tactic:
by

Goal state after:
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
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
⊢ Presieve.IsSheafFor P R ↔ Nonempty (IsLimit (Fork.ofι (forkMap P R) ⋯))

Tactic:
by

Goal state after:
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
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ iYX = e.counitInv.app Y ≫ e.functor.map (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
by

Goal state after:
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
X : C
S : Sieve X
e : C ≌ D
⊢ functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)

Tactic:
by

Goal state after:
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
e : C ≌ D
U : C
S : Sieve U
⊢ functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type t
inst✝ : Small.{w, t} I
X : I → C
z₁ z₂ : FirstObj P X
h :
  ∀ (i : I),
    (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun i ↦ P.obj (op (X i))) i)) z₂
⊢ z₁ = z₂

Tactic:
by

Goal state after:
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
e : C ≌ D
X : C
S : Sieve X
⊢ pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y✝ : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : { x // x.Compatible }
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ ((shrinkFunctor.{w, v₁, u₁} S).toFunctor.map g ≫ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯) =
    (↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯) ≫ F.map g

Tactic:
by

Goal state after:
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
z₁ z₂ : SecondObj P X π
h :
  ∀ (ij : I × I),
    (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun ij ↦ P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij)) z₂
⊢ z₁ = z₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
⊢ (fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ })
      ((fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩) t) =
    t

Tactic:
by

Goal state after:
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
⊢ forkMap P X π ≫ firstMap P X π = forkMap P X π ≫ secondMap P X π

Tactic:
by

Goal state after:
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
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
by

Goal state after:
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
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

Tactic:
by

Goal state after:
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
I : Type u_1
X : I → C
Y : C
⊢ functorPushforward F (ofObjects X Y) ≤ ofObjects (F.obj ∘ X) (F.obj Y)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
x : { x // x.Compatible }
⊢ (fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩)
      ((fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ }) x) =
    x

Tactic:
by

Goal state after:
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
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
Y : Cᵒᵖ
y : Z✝.obj Y
⊢ (hom (f.app Y)).toFun y = (hom (g.app Y)).toFun y

Tactic:
simpa [Subtype.ext_iff] using congr_hom (NatTrans.congr_app h Y) y

Goal state after:
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
Z✝ : Cᵒᵖ ⥤ Type v₁
f g : Z✝ ⟶ S.functor
h : f ≫ S.functorInclusion = g ≫ S.functorInclusion
⊢ f = g

Tactic:
by

Goal state after:
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
R : Cᵒᵖ ⥤ Type v₁
f : R ⟶ yoneda.obj X
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ X},
    (∃ t, (hom (f.app (Opposite.op Y))) t = f_1) → ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = g ≫ f_1

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ sieveOfSubfunctor S.functorInclusion = S

Tactic:
by

Goal state after:
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 w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
by

Goal state after:
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
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔ ∀ (E : Aᵒᵖ), IsSheafFor (P ⋙ coyoneda.obj E) S.arrows

Tactic:
by

Goal state after:
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 S : Sieve X
Z✝ : Cᵒᵖ ⥤ Type (max w v₁)
x✝¹ x✝ : Z✝ ⟶ S.uliftFunctor
h : x✝¹ ≫ S.uliftFunctorInclusion = x✝ ≫ S.uliftFunctorInclusion
⊢ x✝¹ = x✝

Tactic:
by

Goal state after:
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
R : Cᵒᵖ ⥤ Type (max w v₁)
f : R ⟶ uliftYoneda.{w, v₁, u₁}.obj X
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ X},
    (∃ t, (hom (f.app (Opposite.op Y))) t = { down := f_1 }) →
      ∀ (g : Z ⟶ Y), ∃ t, (hom (f.app (Opposite.op Z))) t = { down := g ≫ f_1 }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ sieveOfUliftSubfunctor S.uliftFunctorInclusion = S

Tactic:
by

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
E : Aᵒᵖ
x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows
t₁ t₂ : (P ⋙ coyoneda.obj E).obj (op X)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
hx : x.SieveCompatible
hs : ∀ (a b : hx.cone ⟶ P.mapCone S.arrows.cocone.op), a = b
⊢ t₁ = t₂

Tactic:
simpa only [Subtype.mk.injEq] using (show Subtype.mk t₁ h₁ = ⟨t₂, h₂⟩ from
      (homEquivAmalgamation hx).symm.injective (hs _ _))

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
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
f : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g = f ↔ (↑(shrinkFunctorHomEquiv f)).IsAmalgamation (shrinkYonedaEquiv g)

Tactic:
by

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

Goal state before:
pp: 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)
⊢ ofArrows P p₁ = pullback g (ofArrows X f)

Tactic:
by

Goal state after:
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 : FirstObj P X
⊢ Arrows.Compatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
F : Cᵒᵖ ⥤ Type w
x : FamilyOfElements F S.arrows
hx : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔
    ∃! a, (↑(shrinkFunctorHomEquiv (shrinkFunctorHomEquiv.symm ⟨x, hx⟩))).IsAmalgamation (shrinkYonedaEquiv a)

Tactic:
by

Goal state after:
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
X : C
S : Sieve X
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ {f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ f ∈ ⇑(hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g)) ⁻¹' {f | S.arrows (shrinkYonedaObjObjEquiv f)}

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
F : Cᵒᵖ ⥤ Type w
⊢ IsSheafFor F S.arrows ↔ Function.Bijective fun g ↦ (shrinkFunctor.{w, v₁, u₁} S).ι ≫ g

Tactic:
by

Goal state after:
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
X : Cᵒᵖ
a : (shrinkYoneda.{w, v₁, u₁}.obj X✝).obj X
⊢ a ∈ (shrinkFunctor.{w, v₁, u₁} S).obj X ↔
    (shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm) a ∈ (shrinkFunctor.{max w' w, v₁, u₁} S).obj X

Tactic:
by

Goal state after:
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
⊢ ((shrinkFunctor.{w, v₁, u₁} S).toFunctor ⋙ CategoryTheory.uliftFunctor.{w', w}).map f ≫
      (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom =
    (Equiv.ulift.trans ((shrinkYonedaObjObjEquiv.trans shrinkYonedaObjObjEquiv.symm).subtypeEquiv ⋯)).toIso.hom ≫
      (shrinkFunctor.{max w' w, v₁, u₁} S).toFunctor.map f

Tactic:
by

Goal state after:
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
Y : Cᵒᵖ
⊢ ∀ (a : (shrinkYoneda.{v₁, v₁, u₁}.obj X).obj Y),
    a ∈ (shrinkFunctor.{v₁, v₁, u₁} S).obj Y ↔ S.arrows (shrinkYonedaObjObjEquiv a)

Tactic:
by

Goal state after:
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
U V : Cᵒᵖ
f : U ⟶ V
⊢ (shrinkFunctor.{v₁, v₁, u₁} S).toFunctor.map f ≫ (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom =
    (shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom ≫ S.functor.map f

Tactic:
by

Goal state after: