case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
⊢ IsAmalgamation (pulledbackFamily ℱ S x Z) (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right)
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
⊢ getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right = getSection hu ℱ hS hx Z
apply getSection_is_unique
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
⊢ IsAmalgamation (pulledbackFamily ℱ S x Z) (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right)
intro V' fV' hV'
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
have eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op := by
  convert f.w
  erw [Category.id_comp]
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'✝
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
rw [eq] at hV'
case h.e'_2
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map (fV' ≫ f.right.unop).op (getSection hu ℱ hS hx Y)

case h.e'_3
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ pulledbackFamily ℱ S x Z fV' hV'✝ = pulledbackFamily ℱ S x Y (fV' ≫ f.right.unop) ?H

case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows (fV' ≫ f.right.unop)
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'✝
convert getSection_isAmalgamation hu ℱ hS hx Y (fV' ≫ f.right.unop) _ using 1
case h.e'_2.h
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
e_1✝ :
  ((Functor.fromPUnit U.op).obj Z.left ⟶ (Functor.op G).obj Z.right) =
    ((Functor.fromPUnit U.op).obj Y.left ⟶ (Functor.op G).obj Z.right)
⊢ Z.hom = (Functor.fromPUnit U.op).map f.left ≫ Z.hom
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
⊢ Z.hom = Y.hom ≫ (G.map f.right.unop).op
convert f.w
no goals
case h.e'_2.h
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV' : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
e_1✝ :
  ((Functor.fromPUnit U.op).obj Z.left ⟶ (Functor.op G).obj Z.right) =
    ((Functor.fromPUnit U.op).obj Y.left ⟶ (Functor.op G).obj Z.right)
⊢ Z.hom = (Functor.fromPUnit U.op).map f.left ≫ Z.hom
erw [Category.id_comp]
no goals
case h.e'_2
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj X.op).map (fV' ≫ f.right.unop).op (getSection hu ℱ hS hx Y)
aesop_cat
case h.e'_3
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ x (G.map fV' ≫ Z.hom.unop) hV'✝ ≫ ((Ran.adjunction A (Functor.op G)).counit.app ℱ.val).app V'.op =
    x (G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop) ?H ≫ ((Ran.adjunction A (Functor.op G)).counit.app ℱ.val).app V'.op

case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows (fV' ≫ f.right.unop)

case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows (fV' ≫ f.right.unop)
case h.e'_3
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ pulledbackFamily ℱ S x Z fV' hV'✝ = pulledbackFamily ℱ S x Y (fV' ≫ f.right.unop) ?H
rw [pulledbackFamily_apply, pulledbackFamily_apply]
case h.e'_3.e_a.e_f
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ G.map fV' ≫ Z.hom.unop = G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop
case h.e'_3
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ x (G.map fV' ≫ Z.hom.unop) hV'✝ ≫ ((Ran.adjunction A (Functor.op G)).counit.app ℱ.val).app V'.op =
    x (G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop) ?H ≫ ((Ran.adjunction A (Functor.op G)).counit.app ℱ.val).app V'.op
congr 2
no goals
case h.e'_3.e_a.e_f
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ G.map fV' ≫ Z.hom.unop = G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop
simp [eq]
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ S.arrows (G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop)
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows (fV' ≫ f.right.unop)
change S (G.map _ ≫ Y.hom.unop)
no goals
case H
C D : Type u
inst✝³ : Category C
inst✝² : Category D
A : Type w
inst✝¹ : Category A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hu : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran (Functor.op G)).obj ℱ.val ⋙ coyoneda.obj X.op) S.arrows
hx : Compatible x
Y Z : StructuredArrow U.op (Functor.op G)
f : Y ⟶ Z
V' : C
fV' : V' ⟶ Z.right.unop
hV'✝ : Presieve.functorPullback G (Sieve.pullback Z.hom.unop S).arrows fV'
hV' : Presieve.functorPullback G (Sieve.pullback (Y.hom ≫ (G.map f.right.unop).op).unop S).arrows fV'
eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op
⊢ S.arrows (G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop)
simpa only [Functor.map_comp, Category.assoc] using hV'