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

Goal state before:
pp: case h.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)

Tactic:
·

Goal state after:
case h.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case mp
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ mk x = mk y → ∃ W h1 h2, x.refine h1 = y.refine h2

pp: case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ (∃ W h1 h2, x.refine h1 = y.refine h2) → mk x = mk y

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ mk x = mk y → ∃ W h1 h2, x.refine h1 = y.refine h2
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork P)) → IsIso (S.toMultiequalizer P)

pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork P)) → IsIso (S.toMultiequalizer P)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
⊢ IsIso (S.toMultiequalizer P) → Nonempty (IsLimit (S.multifork P))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt

pp: case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ ∀ (j : WalkingMulticospan S.shape),
    (limit.cone (S.index P).multicospan).π.app j = Iso.hom ?refine_2.refine_1 ≫ (S.multifork P).π.app j

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ (limit.cone (S.index P).multicospan).pt ≅ (S.multifork P).pt
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ ∀ (j : WalkingMulticospan S.shape),
    (limit.cone (S.index P).multicospan).π.app j = (asIso (S.toMultiequalizer P)).symm.hom ≫ (S.multifork P).π.app j

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
S : J.Cover X
h : IsIso (S.toMultiequalizer P)
⊢ ∀ (j : WalkingMulticospan S.shape),
    (limit.cone (S.index P).multicospan).π.app j = (asIso (S.toMultiequalizer P)).symm.hom ≫ (S.multifork P).π.app j
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Injective ⇑(ConcreteCategory.hom ((toRange p).app i))

pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((toRange p).app i))

Tactic:
·

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Injective ⇑(ConcreteCategory.hom ((toRange p).app i))
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((toRange p).app i))

Tactic:
·

Goal state after:
case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((toRange p).app i))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ ((parallelPair (s.map (firstMap R P)) (s.map (secondMap R P))).map WalkingParallelPairHom.right ≫
        (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))).hom) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
    ((PreservesProduct.iso s fun f ↦ P.obj (op f.fst)).hom ≫
        (parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R)).map
          WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁶ : Category.{v₂, u₂} A
A' : Type u₂
inst✝⁵ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U✝ : C
R✝ : Presieve U✝
P✝ : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
inst✝³ : HasProducts A
inst✝² : HasProducts A'
inst✝¹ : HasPullbacks C
P : Cᵒᵖ ⥤ A
s : A ⥤ Type (max v₁ u₁)
inst✝ : ∀ (J : Type (max v₁ u₁)), PreservesLimitsOfShape (Discrete J) s
U : C
R : Presieve U
j : Discrete (((Y : C) × { f // R f }) × (Z : C) × { g // R g })
⊢ ((parallelPair (s.map (firstMap R P)) (s.map (secondMap R P))).map WalkingParallelPairHom.right ≫
        (PreservesProduct.iso s fun fg ↦ P.obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))).hom) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j =
    ((PreservesProduct.iso s fun f ↦ P.obj (op f.fst)).hom ≫
        (parallelPair (Equalizer.Presieve.firstMap (P ⋙ s) R) (Equalizer.Presieve.secondMap (P ⋙ s) R)).map
          WalkingParallelPairHom.right) ≫
      limit.π (Discrete.functor fun fg ↦ (P ⋙ s).obj (op (Limits.pullback ↑fg.1.snd ↑fg.2.snd))) j
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G

pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ (G.preimage p).image p ≤ G
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p

Tactic:
·

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
p : F' ⟶ F
hp : Epi p
⊢ G ≤ (G.preimage p).image p
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))

pp: case e'_2.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)

Tactic:
·

Goal state after:
case e'_2.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g) ≤
    generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i))
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2.refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom

pp: case e'_2.refine_1.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) ?e'_2.refine_1.refine_1 ≫ (Over.map p).map (g i) =
    a ≫ (Over.map p).map (b ≫ g i)

Tactic:
·

Goal state after:
case e'_2.refine_1.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ (Over.Hom.left a ≫ Over.Hom.left b) ≫ ((Over.map p).obj (Z i)).hom = W.hom
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2.refine_1.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) ⋯ ≫ (Over.map p).map (g i) = a ≫ (Over.map p).map (b ≫ g i)

Tactic:
·

Goal state after:
case e'_2.refine_1.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) ⋯ ≫ (Over.map p).map (g i) = a ≫ (Over.map p).map (b ≫ g i)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case e'_2.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)

Tactic:
·

Goal state after:
case e'_2.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
⊢ generate (ofArrows (fun i ↦ (Over.map p).obj (Z i)) fun i ↦ (Over.map p).map (g i)) ≤
    Sieve.functorPushforward (Over.map p) (Sieve.ofArrows Z g)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ (∃ W h1 h2, x.refine h1 = y.refine h2) → mk x = mk y

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
⊢ (∃ W h1 h2, x.refine h1 = y.refine h2) → mk x = mk y
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op)) (x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op)) (x j)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map gi.op)) (x i) = (ConcreteCategory.hom (P.map gj.op)) (x j)

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : Compatible P π x
i j : I
⊢ (ConcreteCategory.hom (P.map (pullback.fst (π i) (π j)).op)) (x i) =
    (ConcreteCategory.hom (P.map (pullback.snd (π i) (π j)).op)) (x j)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf J P' → IsSheaf' J P'

pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf' J P' → IsSheaf J P'

Tactic:
·

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf J P' → IsSheaf' J P'
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map gi.op)) (x i) = (ConcreteCategory.hom (P.map gj.op)) (x j)

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
t : PullbackCompatible P π x
i j : I
Z : C
gi : Z ⟶ X i
gj : Z ⟶ X j
comm : gi ≫ π i = gj ≫ π j
⊢ (ConcreteCategory.hom (P.map gi.op)) (x i) = (ConcreteCategory.hom (P.map gj.op)) (x j)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf' J P' → IsSheaf J P'

Tactic:
·

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
⊢ IsSheaf' J P' → IsSheaf J P'
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
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : ReflectsLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J (P ⋙ s)
⊢ IsSheaf J P

Tactic:
by
  rw [isSheaf_iff_isLimit] at h ⊢
  exact fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfReflects s t

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : Presheaf.IsSheaf J P
⊢ Presheaf.IsSheaf J (P ⋙ F)

Tactic:
rw [Presheaf.isSheaf_iff_multifork] at hP ⊢

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F✝ G H : A ⥤ B
η : F✝ ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F✝
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
F : A ⥤ B
inst✝ : ∀ (X : C) (S : J.Cover X) (P : Cᵒᵖ ⥤ A), PreservesLimit (S.index P).multicospan F
P : Cᵒᵖ ⥤ A
hP : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork (P ⋙ F)))