[GOAL]
C : Type u_1
inst✝² : Category.{u_4, u_1} C
D : Type u_2
inst✝¹ : Category.{?u.745, u_2} D
E : Type u_3
inst✝ : Category.{?u.752, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
U✝ : C
S✝ : Sieve ((𝟭 C).obj U✝)
h : S✝ ∈ GrothendieckTopology.sieves J ((𝟭 C).obj U✝)
⊢ Sieve.functorPullback (𝟭 C) S✝ ∈ GrothendieckTopology.sieves J U✝
[PROOFSTEP]
simpa using h
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
⊢ X ⟶ ℱ.val.obj Y.right
[PROOFSTEP]
letI hom_sh := whiskerRight ((Ran.adjunction A G.op).counit.app ℱ.val) (coyoneda.obj (op X))
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
hom_sh : (ran G.op ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj ℱ.val ⋙ coyoneda.obj (op X) ⟶
  (𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X) :=
  whiskerRight (NatTrans.app (Ran.adjunction A G.op).counit ℱ.val) (coyoneda.obj (op X))
⊢ X ⟶ ℱ.val.obj Y.right
[PROOFSTEP]
haveI S' := K.pullback_stable Y.hom.unop hS
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
hom_sh : (ran G.op ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj ℱ.val ⋙ coyoneda.obj (op X) ⟶
  (𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X) :=
  whiskerRight (NatTrans.app (Ran.adjunction A G.op).counit ℱ.val) (coyoneda.obj (op X))
S' : Sieve.pullback Y.hom.unop S ∈ GrothendieckTopology.sieves K (G.op.obj Y.right).unop
⊢ X ⟶ ℱ.val.obj Y.right
[PROOFSTEP]
haveI hs' := ((hx.pullback Y.3.unop).functorPullback G).compPresheafMap hom_sh
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
hom_sh : (ran G.op ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj ℱ.val ⋙ coyoneda.obj (op X) ⟶
  (𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X) :=
  whiskerRight (NatTrans.app (Ran.adjunction A G.op).counit ℱ.val) (coyoneda.obj (op X))
S' : Sieve.pullback Y.hom.unop S ∈ GrothendieckTopology.sieves K (G.op.obj Y.right).unop
hs' : Compatible (compPresheafMap hom_sh (FamilyOfElements.functorPullback G (FamilyOfElements.pullback Y.hom.unop x)))
⊢ X ⟶ ℱ.val.obj Y.right
[PROOFSTEP]
exact (ℱ.2 X _ (hu.cover_lift S')).amalgamate _ hs'
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op Y.right.unop)
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ y = getSection hu ℱ hS hx Y
[PROOFSTEP]
apply IsSheafFor.isSeparatedFor _ (pulledbackFamily ℱ S x Y)
[GOAL]
case a
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op Y.right.unop)
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) y
[PROOFSTEP]
exact H
[GOAL]
case a
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op Y.right.unop)
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsAmalgamation (pulledbackFamily ℱ S x Y) (getSection hu ℱ hS hx Y)
[PROOFSTEP]
apply getSection_isAmalgamation
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y : StructuredArrow (op U) G.op
y : ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op Y.right.unop)
H : IsAmalgamation (pulledbackFamily ℱ S x Y) y
⊢ IsSheafFor ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X))
    (Presieve.functorPullback G (Sieve.pullback Y.hom.unop S).arrows)
[PROOFSTEP]
exact ℱ.2 X _ (hu.cover_lift (K.pullback_stable Y.hom.unop hS))
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
f : Y ⟶ Z
⊢ getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right = getSection hu ℱ hS hx Z
[PROOFSTEP]
apply getSection_is_unique
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
f : Y ⟶ Z
⊢ IsAmalgamation (pulledbackFamily ℱ S x Z) (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right)
[PROOFSTEP]
intro V' fV' hV'
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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 (op X)).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
[PROOFSTEP]
have eq : Z.hom = Y.hom ≫ (G.map f.right.unop).op := by
  convert f.w
  erw [Category.id_comp]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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
[PROOFSTEP]
convert f.w
[GOAL]
case h.e'_2.h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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 (op U)).obj Z.left ⟶ G.op.obj Z.right) =
    ((Functor.fromPUnit (op U)).obj Y.left ⟶ G.op.obj Z.right)
⊢ Z.hom = (Functor.fromPUnit (op U)).map f.left ≫ Z.hom
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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 (op X)).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'
[PROOFSTEP]
rw [eq] at hV' 
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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 (op X)).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    pulledbackFamily ℱ S x Z fV' hV'✝
[PROOFSTEP]
convert getSection_isAmalgamation hu ℱ hS hx Y (fV' ≫ f.right.unop) _ using 1
[GOAL]
case h.e'_2
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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 (op X)).map fV'.op (getSection hu ℱ hS hx Y ≫ ℱ.val.map f.right) =
    ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).map (fV' ≫ f.right.unop).op (getSection hu ℱ hS hx Y)
[PROOFSTEP]
aesop_cat
  -- porting note: the below proof was mildly rewritten because `simp` changed behaviour
    -- slightly (a rewrite which seemed to work in Lean 3, didn't work in Lean 4 because of
    -- motive is not type correct issues)
[GOAL]
case h.e'_3
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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
[PROOFSTEP]
rw [pulledbackFamily_apply, pulledbackFamily_apply]
[GOAL]
case h.e'_3
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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'✝ ≫ NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit ℱ.val) (op V') =
    x (G.map (fV' ≫ f.right.unop) ≫ Y.hom.unop) ?H ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit ℱ.val) (op V')
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_3.e_a.e_f
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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
[PROOFSTEP]
simp [eq]
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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)
[PROOFSTEP]
change S (G.map _ ≫ Y.hom.unop)
[GOAL]
case H
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
Y Z : StructuredArrow (op U) G.op
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)
[PROOFSTEP]
simpa only [Functor.map_comp, Category.assoc] using hV'
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W =
    NatTrans.app (gluedLimitCone hu ℱ hS hx).π ((StructuredArrow.map f.op).obj W)
[PROOFSTEP]
dsimp only [gluedLimitCone_π_app]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W = getSection hu ℱ hS hx ((StructuredArrow.map f.op).obj W)
[PROOFSTEP]
apply getSection_is_unique hu ℱ hS hx ((StructuredArrow.map f.op).obj W)
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
⊢ IsAmalgamation (pulledbackFamily ℱ S x ((StructuredArrow.map f.op).obj W))
    (y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W)
[PROOFSTEP]
intro V' fV' hV'
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV'.op (y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W) =
    pulledbackFamily ℱ S x ((StructuredArrow.map f.op).obj W) fV' hV'
[PROOFSTEP]
dsimp only [Ran.adjunction, Ran.equiv, pulledbackFamily_apply]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV'.op (y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W) =
    x (G.map fV' ≫ ((StructuredArrow.map f.op).obj W).hom.unop) hV' ≫
      NatTrans.app
        (NatTrans.app
          (Adjunction.adjunctionOfEquivRight
              (fun F G_1 =>
                {
                    toFun := fun f =>
                      NatTrans.mk fun x =>
                        NatTrans.app f (G.op.obj x) ≫
                          limit.π (Ran.diagram G.op G_1 (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))),
                    invFun := fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op G_1 x) (Ran.cone x f),
                    left_inv :=
                      (_ :
                        ∀ (x : F ⟶ Ran.loc G.op G_1),
                          (fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op G_1 x) (Ran.cone x f))
                              ((fun f =>
                                  NatTrans.mk fun x =>
                                    NatTrans.app f (G.op.obj x) ≫
                                      limit.π (Ran.diagram G.op G_1 (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                                x) =
                            x),
                    right_inv :=
                      (_ :
                        ∀ (x : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F ⟶ G_1),
                          (fun f =>
                                NatTrans.mk fun x =>
                                  NatTrans.app f (G.op.obj x) ≫
                                    limit.π (Ran.diagram G.op G_1 (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                              ((fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op G_1 x) (Ran.cone x f)) x) =
                            x) }.symm)
              (_ :
                ∀ (X' X : Dᵒᵖ ⥤ A) (Y : Cᵒᵖ ⥤ A) (f : X' ⟶ X) (g : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj X ⟶ Y),
                  ↑((fun F G_1 => (Ran.equiv G.op G_1 F).symm) X' Y) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map f ≫ g) =
                    f ≫ ↑((fun F G_1 => (Ran.equiv G.op G_1 F).symm) X Y) g)).counit
          ℱ.val)
        (op V')
[PROOFSTEP]
erw [Adjunction.adjunctionOfEquivRight_counit_app]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV'.op (y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W) =
    x (G.map fV' ≫ ((StructuredArrow.map f.op).obj W).hom.unop) hV' ≫
      NatTrans.app
        (↑{
                  toFun := fun f =>
                    NatTrans.mk fun x =>
                      NatTrans.app f (G.op.obj x) ≫
                        limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))),
                  invFun := fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f),
                  left_inv :=
                    (_ :
                      ∀ (x : Ran.loc G.op ℱ.val ⟶ Ran.loc G.op ℱ.val),
                        (fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f))
                            ((fun f =>
                                NatTrans.mk fun x =>
                                  NatTrans.app f (G.op.obj x) ≫
                                    limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                              x) =
                          x),
                  right_inv :=
                    (_ :
                      ∀ (x : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj (Ran.loc G.op ℱ.val) ⟶ ℱ.val),
                        (fun f =>
                              NatTrans.mk fun x =>
                                NatTrans.app f (G.op.obj x) ≫
                                  limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                            ((fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f)) x) =
                          x) }.symm.symm
          (𝟙 (Ran.loc G.op ℱ.val)))
        (op V')
[PROOFSTEP]
have :
  y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op =
    x (G.map fV' ≫ W.hom.unop ≫ f) (by simpa only using hV') :=
  by
  convert H (show S ((G.map fV' ≫ W.hom.unop) ≫ f) by simpa only [Category.assoc] using hV') using 2
  simp only [Category.assoc]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ S.arrows (G.map fV' ≫ W.hom.unop ≫ f)
[PROOFSTEP]
simpa only using hV'
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
[PROOFSTEP]
convert H (show S ((G.map fV' ≫ W.hom.unop) ≫ f) by simpa only [Category.assoc] using hV') using 2
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ S.arrows ((G.map fV' ≫ W.hom.unop) ≫ f)
[PROOFSTEP]
simpa only [Category.assoc] using hV'
[GOAL]
case h.e'_3.h.e'_2
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
⊢ G.map fV' ≫ W.hom.unop ≫ f = (G.map fV' ≫ W.hom.unop) ≫ f
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
⊢ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV'.op (y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W) =
    x (G.map fV' ≫ ((StructuredArrow.map f.op).obj W).hom.unop) hV' ≫
      NatTrans.app
        (↑{
                  toFun := fun f =>
                    NatTrans.mk fun x =>
                      NatTrans.app f (G.op.obj x) ≫
                        limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))),
                  invFun := fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f),
                  left_inv :=
                    (_ :
                      ∀ (x : Ran.loc G.op ℱ.val ⟶ Ran.loc G.op ℱ.val),
                        (fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f))
                            ((fun f =>
                                NatTrans.mk fun x =>
                                  NatTrans.app f (G.op.obj x) ≫
                                    limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                              x) =
                          x),
                  right_inv :=
                    (_ :
                      ∀ (x : ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj (Ran.loc G.op ℱ.val) ⟶ ℱ.val),
                        (fun f =>
                              NatTrans.mk fun x =>
                                NatTrans.app f (G.op.obj x) ≫
                                  limit.π (Ran.diagram G.op ℱ.val (G.op.obj x)) (StructuredArrow.mk (𝟙 (G.op.obj x))))
                            ((fun f => NatTrans.mk fun x => limit.lift (Ran.diagram G.op ℱ.val x) (Ran.cone x f)) x) =
                          x) }.symm.symm
          (𝟙 (Ran.loc G.op ℱ.val)))
        (op V')
[PROOFSTEP]
simp only [Quiver.Hom.unop_op, Equiv.symm_symm, StructuredArrow.map_obj_hom, unop_comp, Equiv.coe_fn_mk,
  Functor.comp_map, coyoneda_obj_map, Category.assoc, ← this, op_comp, ran_obj_map, NatTrans.id_app]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W ≫ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).map fV'.op =
    y ≫
      limit.pre (Ran.diagram G.op ℱ.val (op V)) (StructuredArrow.map (W.hom.unop.op ≫ (G.map fV').op)) ≫
        𝟙 ((Ran.loc G.op ℱ.val).obj (G.op.obj (op V'))) ≫
          limit.π (Ran.diagram G.op ℱ.val (G.op.obj (op V'))) (StructuredArrow.mk (𝟙 (G.op.obj (op V'))))
[PROOFSTEP]
erw [Category.id_comp, limit.pre_π]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W ≫ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).map fV'.op =
    y ≫
      limit.π (Ran.diagram G.op ℱ.val (op V))
        ((StructuredArrow.map (W.hom.unop.op ≫ (G.map fV').op)).obj (StructuredArrow.mk (𝟙 (G.op.obj (op V')))))
[PROOFSTEP]
congr
[GOAL]
case e_a
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
⊢ limit.π (Ran.diagram G.op ℱ.val (op V)) W ≫ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).map fV'.op =
    limit.π (Ran.diagram G.op ℱ.val (op V))
      ((StructuredArrow.map (W.hom.unop.op ≫ (G.map fV').op)).obj (StructuredArrow.mk (𝟙 (G.op.obj (op V')))))
[PROOFSTEP]
convert limit.w (Ran.diagram G.op ℱ.val (op V)) (StructuredArrow.homMk' W fV'.op)
[GOAL]
case h.e'_3.h.h.e'_7
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
e_1✝ :
  (((ran G.op).obj ℱ.val).obj (op V) ⟶ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).obj (op V')) =
    (limit (Ran.diagram G.op ℱ.val (op V)) ⟶
      (Ran.diagram G.op ℱ.val (op V)).obj (StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)))
⊢ (StructuredArrow.map (W.hom.unop.op ≫ (G.map fV').op)).obj (StructuredArrow.mk (𝟙 (G.op.obj (op V')))) =
    StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)
[PROOFSTEP]
rw [StructuredArrow.map_mk]
[GOAL]
case h.e'_3.h.h.e'_7
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
e_1✝ :
  (((ran G.op).obj ℱ.val).obj (op V) ⟶ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).obj (op V')) =
    (limit (Ran.diagram G.op ℱ.val (op V)) ⟶
      (Ran.diagram G.op ℱ.val (op V)).obj (StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)))
⊢ StructuredArrow.mk ((W.hom.unop.op ≫ (G.map fV').op) ≫ 𝟙 (G.op.obj (op V'))) =
    StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
case h.e'_3.h.h.e'_7
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
f : V ⟶ U
y : X ⟶ ((ran G.op).obj ℱ.val).obj (op V)
W : StructuredArrow (op V) G.op
H : ∀ {V' : C} {fV : G.obj V' ⟶ V} (hV : S.arrows (fV ≫ f)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ f) hV
V' : C
fV' : V' ⟶ ((StructuredArrow.map f.op).obj W).right.unop
hV' : Presieve.functorPullback G (Sieve.pullback ((StructuredArrow.map f.op).obj W).hom.unop S).arrows fV'
this : y ≫ ((ran G.op).obj ℱ.val).map (G.map fV' ≫ W.hom.unop).op = x (G.map fV' ≫ W.hom.unop ≫ f) hV'
e_1✝ :
  (((ran G.op).obj ℱ.val).obj (op V) ⟶ ((𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val).obj (op V')) =
    (limit (Ran.diagram G.op ℱ.val (op V)) ⟶
      (Ran.diagram G.op ℱ.val (op V)).obj (StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)))
⊢ StructuredArrow.mk (W.hom.unop.op ≫ (G.map fV').op) = StructuredArrow.mk (W.hom ≫ G.op.map fV'.op)
[PROOFSTEP]
simp only [Quiver.Hom.unop_op, Functor.op_map, Quiver.Hom.op_unop]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ IsAmalgamation x (gluedSection hu ℱ hS hx)
[PROOFSTEP]
intro V fV hV
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
⊢ ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV.op (gluedSection hu ℱ hS hx) = x fV hV
[PROOFSTEP]
refine limit.hom_ext (λ (W : StructuredArrow (op V) G.op) => ?_)
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
⊢ ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).map fV.op (gluedSection hu ℱ hS hx) ≫
      limit.π (Ran.diagram G.op ℱ.val (op V)) W =
    x fV hV ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W
[PROOFSTEP]
simp only [Functor.comp_map, limit.lift_pre, coyoneda_obj_map, ran_obj_map, gluedSection]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
⊢ limit.lift (StructuredArrow.map fV.op ⋙ Ran.diagram G.op ℱ.val (op U))
        (Cone.whisker (StructuredArrow.map fV.op) (gluedLimitCone hu ℱ hS hx)) ≫
      limit.π (Ran.diagram G.op ℱ.val (op V)) W =
    x fV hV ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W
[PROOFSTEP]
erw [limit.lift_π]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
⊢ NatTrans.app (Cone.whisker (StructuredArrow.map fV.op) (gluedLimitCone hu ℱ hS hx)).π W =
    x fV hV ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W
[PROOFSTEP]
symm
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
⊢ x fV hV ≫ limit.π (Ran.diagram G.op ℱ.val (op V)) W =
    NatTrans.app (Cone.whisker (StructuredArrow.map fV.op) (gluedLimitCone hu ℱ hS hx)).π W
[PROOFSTEP]
convert helper hu ℱ hS hx _ (x fV hV) _ _ using 1
[GOAL]
case convert_3
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
⊢ ∀ {V' : C} {fV_1 : G.obj V' ⟶ V} (hV_1 : S.arrows (fV_1 ≫ fV)),
    x fV hV ≫ ((ran G.op).obj ℱ.val).map fV_1.op = x (fV_1 ≫ fV) hV_1
[PROOFSTEP]
intro V' fV' hV'
[GOAL]
case convert_3
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
V' : C
fV' : G.obj V' ⟶ V
hV' : S.arrows (fV' ≫ fV)
⊢ x fV hV ≫ ((ran G.op).obj ℱ.val).map fV'.op = x (fV' ≫ fV) hV'
[PROOFSTEP]
convert hx fV' (𝟙 _) hV hV' (by rw [Category.id_comp])
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
V' : C
fV' : G.obj V' ⟶ V
hV' : S.arrows (fV' ≫ fV)
⊢ fV' ≫ fV = 𝟙 (G.obj V') ≫ fV' ≫ fV
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
case h.e'_3.h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
V : D
fV : V ⟶ U
hV : S.arrows fV
W : StructuredArrow (op V) G.op
V' : C
fV' : G.obj V' ⟶ V
hV' : S.arrows (fV' ≫ fV)
e_1✝ :
  (X ⟶ ((ran G.op).obj ℱ.val).obj (op (G.obj V'))) = ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op (G.obj V'))
⊢ x (fV' ≫ fV) hV' = ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).map (𝟙 (G.obj V')).op (x (fV' ≫ fV) hV')
[PROOFSTEP]
simp only [op_id, FunctorToTypes.map_id_apply]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
⊢ y = gluedSection hu ℱ hS hx
[PROOFSTEP]
unfold gluedSection limit.lift
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
⊢ y = IsLimit.lift (limit.isLimit (Ran.diagram G.op ℱ.val (op U))) (gluedLimitCone hu ℱ hS hx)
[PROOFSTEP]
refine limit.hom_ext (λ (W : StructuredArrow (op U) G.op) => ?_)
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op U)) W =
    IsLimit.lift (limit.isLimit (Ran.diagram G.op ℱ.val (op U))) (gluedLimitCone hu ℱ hS hx) ≫
      limit.π (Ran.diagram G.op ℱ.val (op U)) W
[PROOFSTEP]
erw [limit.lift_π]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
⊢ y ≫ limit.π (Ran.diagram G.op ℱ.val (op U)) W = NatTrans.app (gluedLimitCone hu ℱ hS hx).π W
[PROOFSTEP]
convert helper hu ℱ hS hx (𝟙 _) y W _
[GOAL]
case h.e'_3.h.h.e'_8
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
e_1✝ : ((op X).unop ⟶ (Ran.diagram G.op ℱ.val (op U)).obj W) = (X ⟶ (Ran.diagram G.op ℱ.val (op U)).obj W)
⊢ W = (StructuredArrow.map (𝟙 U).op).obj W
[PROOFSTEP]
simp only [op_id, StructuredArrow.map_id]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
⊢ ∀ {V' : C} {fV : G.obj V' ⟶ U} (hV : S.arrows (fV ≫ 𝟙 U)), y ≫ ((ran G.op).obj ℱ.val).map fV.op = x (fV ≫ 𝟙 U) hV
[PROOFSTEP]
intro V' fV' hV'
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
V' : C
fV' : G.obj V' ⟶ U
hV' : S.arrows (fV' ≫ 𝟙 U)
⊢ y ≫ ((ran G.op).obj ℱ.val).map fV'.op = x (fV' ≫ 𝟙 U) hV'
[PROOFSTEP]
convert hy fV' (by simpa only [Category.comp_id] using hV')
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
V' : C
fV' : G.obj V' ⟶ U
hV' : S.arrows (fV' ≫ 𝟙 U)
⊢ S.arrows fV'
[PROOFSTEP]
simpa only [Category.comp_id] using hV'
[GOAL]
case h.e'_3.h.h.e'_2
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} 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 G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
hy : IsAmalgamation x y
W : StructuredArrow (op U) G.op
V' : C
fV' : G.obj V' ⟶ U
hV' : S.arrows (fV' ≫ 𝟙 U)
e_1✝ :
  (X ⟶ ((ran G.op).obj ℱ.val).obj (op (G.obj V'))) = ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op (G.obj V'))
⊢ fV' ≫ 𝟙 U = fV'
[PROOFSTEP]
erw [Category.comp_id]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
⊢ Presheaf.IsSheaf K ((ran G.op).obj ℱ.val)
[PROOFSTEP]
intro X U S hS x hx
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ∃! t, IsAmalgamation x t
[PROOFSTEP]
constructor
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ (fun t => IsAmalgamation x t) ?w ∧
    ∀ (y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)), (fun t => IsAmalgamation x t) y → y = ?w
case w
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
[PROOFSTEP]
swap
[GOAL]
case w
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)
[PROOFSTEP]
apply RanIsSheafOfCoverLifting.gluedSection hG ℱ hS hx
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ (fun t => IsAmalgamation x t) (RanIsSheafOfCoverLifting.gluedSection hG ℱ hS hx) ∧
    ∀ (y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)),
      (fun t => IsAmalgamation x t) y → y = RanIsSheafOfCoverLifting.gluedSection hG ℱ hS hx
[PROOFSTEP]
constructor
[GOAL]
case h.left
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ (fun t => IsAmalgamation x t) (RanIsSheafOfCoverLifting.gluedSection hG ℱ hS hx)
[PROOFSTEP]
apply RanIsSheafOfCoverLifting.gluedSection_isAmalgamation
[GOAL]
case h.right
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
hG : CoverLifting J K G
ℱ : Sheaf J A
X : A
U : D
S : Sieve U
hS : S ∈ GrothendieckTopology.sieves K U
x : FamilyOfElements ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)) S.arrows
hx : Compatible x
⊢ ∀ (y : ((ran G.op).obj ℱ.val ⋙ coyoneda.obj (op X)).obj (op U)),
    (fun t => IsAmalgamation x t) y → y = RanIsSheafOfCoverLifting.gluedSection hG ℱ hS hx
[PROOFSTEP]
apply RanIsSheafOfCoverLifting.gluedSection_is_unique
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : (pullback A Hc Hp).obj X ⟶ Y
⊢ (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
      ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f) =
    f
[PROOFSTEP]
ext1
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : (pullback A Hc Hp).obj X ⟶ Y
⊢ ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
        ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f)).val =
    f.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : (pullback A Hc Hp).obj X ⟶ Y
⊢ ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm
      (↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val) =
    f.val
[PROOFSTEP]
rw [Equiv.symm_apply_apply]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : X ⟶ (copullback A Hl).obj Y
⊢ (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
      ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val }) f) =
    f
[PROOFSTEP]
ext1
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : X ⟶ (copullback A Hl).obj Y
⊢ ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
        ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val }) f)).val =
    f.val
[PROOFSTEP]
dsimp
[GOAL]
case h
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X : Sheaf K A
Y : Sheaf J A
f : X ⟶ (copullback A Hl).obj Y
⊢ ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val)
      (↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val) =
    f.val
[PROOFSTEP]
rw [Equiv.apply_symm_apply]
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
⊢ ∀ {X : Sheaf K A} {Y : Sheaf J A} {f : (pullback A Hc Hp).obj X ⟶ Y},
    ↑((fun X Y =>
              { toFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val },
                invFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val },
                left_inv :=
                  (_ :
                    ∀ (f : (pullback A Hc Hp).obj X ⟶ Y),
                      (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                          ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (copullback A Hl).obj Y),
                      (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
                          ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                            f) =
                        f) })
            X Y)
        f =
      NatTrans.app (NatTrans.mk fun X => { val := NatTrans.app (Ran.adjunction A G.op).unit X.val }) X ≫
        (copullback A Hl).map f
[PROOFSTEP]
refine Sheaf.Hom.ext _ _ ?_
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X✝ : Sheaf K A
Y✝ : Sheaf J A
f✝ : (pullback A Hc Hp).obj X✝ ⟶ Y✝
⊢ (↑((fun X Y =>
              { toFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val },
                invFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val },
                left_inv :=
                  (_ :
                    ∀ (f : (pullback A Hc Hp).obj X ⟶ Y),
                      (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                          ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ (copullback A Hl).obj Y),
                      (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
                          ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                            f) =
                        f) })
            X✝ Y✝)
        f✝).val =
    (NatTrans.app (NatTrans.mk fun X => { val := NatTrans.app (Ran.adjunction A G.op).unit X.val }) X✝ ≫
        (copullback A Hl).map f✝).val
[PROOFSTEP]
apply (Ran.adjunction A G.op).homEquiv_unit
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
⊢ ∀ {X : Sheaf K A} {Y : Sheaf J A} {g : X ⟶ (copullback A Hl).obj Y},
    ↑((fun X Y =>
                { toFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val },
                  invFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val },
                  left_inv :=
                    (_ :
                      ∀ (f : (pullback A Hc Hp).obj X ⟶ Y),
                        (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                            ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (copullback A Hl).obj Y),
                        (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
                            ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                              f) =
                          f) })
              X Y).symm
        g =
      (pullback A Hc Hp).map g ≫
        NatTrans.app (NatTrans.mk fun X => { val := NatTrans.app (Ran.adjunction A G.op).counit X.val }) Y
[PROOFSTEP]
refine Sheaf.Hom.ext _ _ ?_
[GOAL]
C D : Type u
inst✝³ : Category.{v, u} C
inst✝² : Category.{v, u} D
A : Type w
inst✝¹ : Category.{max u v, w} A
inst✝ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
X✝ : Sheaf K A
Y✝ : Sheaf J A
g✝ : X✝ ⟶ (copullback A Hl).obj Y✝
⊢ (↑((fun X Y =>
                { toFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val },
                  invFun := fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val },
                  left_inv :=
                    (_ :
                      ∀ (f : (pullback A Hc Hp).obj X ⟶ Y),
                        (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                            ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val }) f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ (copullback A Hl).obj Y),
                        (fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val) f.val })
                            ((fun f => { val := ↑(Adjunction.homEquiv (Ran.adjunction A G.op) X.val Y.val).symm f.val })
                              f) =
                          f) })
              X✝ Y✝).symm
        g✝).val =
    ((pullback A Hc Hp).map g✝ ≫
        NatTrans.app (NatTrans.mk fun X => { val := NatTrans.app (Ran.adjunction A G.op).counit X.val }) Y✝).val
[PROOFSTEP]
apply (Ran.adjunction A G.op).homEquiv_counit
[GOAL]
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
      (NatTrans.app (pullbackSheafificationCompatibility A Hp Hl Hc).hom F).val =
    whiskerLeft G.op (GrothendieckTopology.toSheafify K F)
[PROOFSTEP]
dsimp [pullbackSheafificationCompatibility, Adjunction.leftAdjointUniq]
[GOAL]
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
      (coyoneda.preimage
            (NatTrans.app
              (Adjunction.leftAdjointsCoyonedaEquiv
                  (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc))
                  (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A))).hom
              (op F))).unop.val =
    whiskerLeft G.op (GrothendieckTopology.toSheafify K F)
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
        (coyoneda.preimage
              (NatTrans.app
                (Adjunction.leftAdjointsCoyonedaEquiv
                    (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc))
                    (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A))).hom
                (op F))).unop.val).op =
    (whiskerLeft G.op (GrothendieckTopology.toSheafify K F)).op
[PROOFSTEP]
apply coyoneda.map_injective
[GOAL]
case a.a
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ coyoneda.map
      (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
          (coyoneda.preimage
                (NatTrans.app
                  (Adjunction.leftAdjointsCoyonedaEquiv
                      (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc))
                      (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A))).hom
                  (op F))).unop.val).op =
    coyoneda.map (whiskerLeft G.op (GrothendieckTopology.toSheafify K F)).op
[PROOFSTEP]
ext E : 2
[GOAL]
case a.a.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
⊢ NatTrans.app
      (coyoneda.map
        (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
            (coyoneda.preimage
                  (NatTrans.app
                    (Adjunction.leftAdjointsCoyonedaEquiv
                        (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc))
                        (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A))).hom
                    (op F))).unop.val).op)
      E =
    NatTrans.app (coyoneda.map (whiskerLeft G.op (GrothendieckTopology.toSheafify K F)).op) E
[PROOFSTEP]
dsimp [Functor.preimage, Full.preimage, coyoneda, Adjunction.leftAdjointsCoyonedaEquiv]
[GOAL]
case a.a.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
⊢ (fun g =>
      (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
          (↑(Adjunction.homEquiv (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A)) F
                    (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F))).symm
              (↑(Adjunction.homEquiv
                    (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc)) F
                    (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)))
                (𝟙 (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F))))).val) ≫
        g) =
    fun g => whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫ g
[PROOFSTEP]
erw [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]
[GOAL]
case a.a.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
⊢ (fun g =>
      (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
          (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⋙ presheafToSheaf J A).map
                (NatTrans.app
                    (Adjunction.comp (sheafificationAdjunction K A) (pullbackCopullbackAdjunction A Hp Hl Hc)).unit F ≫
                  (sheafToPresheaf J A ⋙ ran G.op).map (𝟙 (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)))) ≫
              NatTrans.app (Adjunction.comp (Ran.adjunction A G.op) (sheafificationAdjunction J A)).counit
                (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F))).val) ≫
        g) =
    fun g => whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫ g
[PROOFSTEP]
dsimp [Adjunction.comp]
[GOAL]
case a.a.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
⊢ (fun g =>
      (GrothendieckTopology.toSheafify J (G.op ⋙ F) ≫
          GrothendieckTopology.sheafifyMap J
              ((whiskerLeft G.op (NatTrans.app (sheafificationAdjunction K A).unit F) ≫
                  whiskerLeft G.op (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) ≫
                    𝟙 (G.op ⋙ ((copullback A Hl).obj (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F))).val)) ≫
                whiskerLeft G.op ((ran G.op).map (𝟙 (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val))) ≫
            𝟙
                (GrothendieckTopology.sheafify J
                  (G.op ⋙ (ran G.op).obj (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val)) ≫
              GrothendieckTopology.sheafifyMap J
                  (NatTrans.app (Ran.adjunction A G.op).counit
                    (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val) ≫
                GrothendieckTopology.sheafifyLift J (𝟙 (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val)
                  (_ : Presheaf.IsSheaf J (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val)) ≫
        g) =
    fun g => whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫ g
[PROOFSTEP]
simp only [sheafificationAdjunction_unit_app, Category.comp_id, Functor.map_id, whiskerLeft_id',
  GrothendieckTopology.sheafifyMap_comp, GrothendieckTopology.sheafifyMap_sheafifyLift, Category.id_comp,
  Category.assoc, GrothendieckTopology.toSheafify_sheafifyLift]
[GOAL]
case a.a.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
⊢ (fun g =>
      whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫
        whiskerLeft G.op (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) ≫
          NatTrans.app (Ran.adjunction A G.op).counit (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ≫ g) =
    fun g => whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫ g
[PROOFSTEP]
ext t s : 3
[GOAL]
case a.a.w.h.h.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
⊢ NatTrans.app
      (whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫
        whiskerLeft G.op (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) ≫
          NatTrans.app (Ran.adjunction A G.op).counit (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ≫ t)
      s =
    NatTrans.app (whiskerLeft G.op (GrothendieckTopology.toSheafify K F) ≫ t) s
[PROOFSTEP]
dsimp [pullbackSheaf]
[GOAL]
case a.a.w.h.h.w.h
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
⊢ NatTrans.app (GrothendieckTopology.toSheafify K F) (op (G.obj s.unop)) ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
        NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s ≫
          NatTrans.app t s =
    NatTrans.app (GrothendieckTopology.toSheafify K F) (op (G.obj s.unop)) ≫ NatTrans.app t s
[PROOFSTEP]
congr 1
[GOAL]
case a.a.w.h.h.w.h.e_a
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
⊢ NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s ≫
        NatTrans.app t s =
    NatTrans.app t s
[PROOFSTEP]
simp only [← Category.assoc]
[GOAL]
case a.a.w.h.h.w.h.e_a
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
⊢ (NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
        NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s) ≫
      NatTrans.app t s =
    NatTrans.app t s
[PROOFSTEP]
convert Category.id_comp (obj := A) _
[GOAL]
case h.e'_2.h.h.e'_6
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
⊢ NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s =
    𝟙 ((GrothendieckTopology.sheafify K F).obj (op (G.obj s.unop)))
[PROOFSTEP]
have := (Ran.adjunction A G.op).left_triangle
[GOAL]
case h.e'_2.h.h.e'_6
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
this :
  whiskerRight (Ran.adjunction A G.op).unit ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op) ≫
      whiskerLeft ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op) (Ran.adjunction A G.op).counit =
    𝟙 (𝟭 (Dᵒᵖ ⥤ A) ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op)
⊢ NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s =
    𝟙 ((GrothendieckTopology.sheafify K F).obj (op (G.obj s.unop)))
[PROOFSTEP]
apply_fun (fun e => (e.app (K.sheafify F)).app s) at this 
[GOAL]
case h.e'_2.h.h.e'_6
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
E : Cᵒᵖ ⥤ A
t : (pullbackSheaf Hc Hp ((presheafToSheaf K A).obj F)).val ⟶ E
s : Cᵒᵖ
this :
  NatTrans.app
      (NatTrans.app
        (whiskerRight (Ran.adjunction A G.op).unit ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op) ≫
          whiskerLeft ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op) (Ran.adjunction A G.op).counit)
        (GrothendieckTopology.sheafify K F))
      s =
    NatTrans.app
      (NatTrans.app (𝟙 (𝟭 (Dᵒᵖ ⥤ A) ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op)) (GrothendieckTopology.sheafify K F)) s
⊢ NatTrans.app (NatTrans.app (Ran.adjunction A G.op).unit (GrothendieckTopology.sheafify K F)) (op (G.obj s.unop)) ≫
      NatTrans.app (NatTrans.app (Ran.adjunction A G.op).counit (G.op ⋙ GrothendieckTopology.sheafify K F)) s =
    𝟙 ((GrothendieckTopology.sheafify K F).obj (op (G.obj s.unop)))
[PROOFSTEP]
exact this
[GOAL]
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ (NatTrans.app (pullbackSheafificationCompatibility A Hp Hl Hc).hom F).val =
    GrothendieckTopology.sheafifyLift J (whiskerLeft G.op (GrothendieckTopology.toSheafify K F))
      (_ : Presheaf.IsSheaf J ((presheafToSheaf K A ⋙ pullback A Hc Hp).obj F).val)
[PROOFSTEP]
apply J.sheafifyLift_unique
[GOAL]
case a
C D : Type u
inst✝¹⁰ : Category.{v, u} C
inst✝⁹ : Category.{v, u} D
A : Type w
inst✝⁸ : Category.{max u v, w} A
inst✝⁷ : HasLimits A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁶ : ConcreteCategory A
inst✝⁵ : PreservesLimits (forget A)
inst✝⁴ : ReflectsIsomorphisms (forget A)
inst✝³ : (X : C) → PreservesColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ (forget A)
inst✝² : ∀ (X : C), HasColimitsOfShape (GrothendieckTopology.Cover J X)ᵒᵖ A
inst✝¹ : (X : D) → PreservesColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ (forget A)
inst✝ : ∀ (X : D), HasColimitsOfShape (GrothendieckTopology.Cover K X)ᵒᵖ A
G : C ⥤ D
Hp : CoverPreserving J K G
Hl : CoverLifting J K G
Hc : CompatiblePreserving K G
F : Dᵒᵖ ⥤ A
⊢ GrothendieckTopology.toSheafify J (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
      (NatTrans.app (pullbackSheafificationCompatibility A Hp Hl Hc).hom F).val =
    whiskerLeft G.op (GrothendieckTopology.toSheafify K F)
[PROOFSTEP]
apply toSheafify_pullbackSheafificationCompatibility
