ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>X : D<VAR>S : K.Cover X<VAR>s : CategoryTheory.Limits.Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<GOAL>CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f ≫ F.map g.op = s.ι i ≫ R.map h.op ≫ α.app (Opposite.op W)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>X : D<VAR>S : K.Cover X<VAR>s : CategoryTheory.Limits.Multifork (S.index R)<VAR>Y Y' : C<VAR>f : G.obj Y ⟶ X<VAR>f' : G.obj Y' ⟶ X<VAR>W : C<VAR>a : W ⟶ Y<VAR>b : W ⟶ Y'<VAR>w : G.map a ≫ f = G.map b ≫ f'<GOAL>CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f ≫ F.map a.op = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s f' ≫ F.map b.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : CategoryTheory.Limits.Multifork (S.index R)<VAR>j : CategoryTheory.StructuredArrow (Opposite.op X) G.op<GOAL>CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s ≫ R.map j.hom ≫ α.app j.right = CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux hF α s j.hom.unop
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : CategoryTheory.Limits.Multifork (S.index R)<VAR>i : S.Arrow<GOAL>CategoryTheory.RanIsSheafOfIsCocontinuous.lift hF hR s ≫ R.map i.f.op = s.ι i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>W : A<VAR>f g : W ⟶ R.obj (Opposite.op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<GOAL>f = g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>ℱ : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Presheaf.IsSheaf K (G.op.ran.obj ℱ.val)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<GOAL>(G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom = 𝟙 (G.sheafPushforwardCocontinuous A J K ⋙ CategoryTheory.sheafToPresheaf K A)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCocontinuous J K<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<GOAL>(G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv = 𝟙 (G.sheafPushforwardCocontinuous A J K ⋙ CategoryTheory.sheafToPresheaf K A)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>G.IsCocontinuous J K<VAR>G.IsContinuous J K<VAR>F : CategoryTheory.Sheaf K A<GOAL>((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>G.IsCocontinuous J K<VAR>G.IsContinuous J K<VAR>F : CategoryTheory.Sheaf J A<GOAL>((G.sheafAdjunctionCocontinuous A J K).counit.app F).val = (G.op.ranAdjunction A).counit.app F.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>G.IsCocontinuous J K<VAR>G.IsContinuous J K<VAR>F : CategoryTheory.Sheaf K A<VAR>H : CategoryTheory.Sheaf J A<VAR>f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H<GOAL>(((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).val = ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify K A<VAR>G.IsCocontinuous J K<VAR>G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<GOAL>CategoryTheory.toSheafify J (G.op ⋙ F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>CategoryTheory.Category.{w', w} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>CategoryTheory.HasWeakSheafify J A<VAR>CategoryTheory.HasWeakSheafify K A<VAR>G.IsCocontinuous J K<VAR>G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<GOAL>((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = CategoryTheory.sheafifyLift J (CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)) ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>V U : D<VAR>f : V ⟶ U<VAR>self : CategoryTheory.Presieve.CoverByImageStructure G f<GOAL>CategoryTheory.CategoryStruct.comp self.lift self.map = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>X : D<VAR>Y : C<VAR>f : G.obj Y ⟶ X<GOAL>CategoryTheory.Presieve.coverByImage G X f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : G.IsCoverDense K<VAR>U : D<GOAL>CategoryTheory.Sieve.coverByImage G U ∈ K.sieves U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.IsCoverDense K<VAR>U : D<GOAL>CategoryTheory.Sieve.coverByImage G U ∈ K.sieves U
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>h : ∀ (B : D), ∃ X f, CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) ∈ K.sieves B<GOAL>G.IsCoverDense K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>X : D<VAR>s t : ℱ.val.obj (Opposite.op X)<VAR>h : ∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X), ℱ.val.map f.op s = ℱ.val.map f.op t<GOAL>s = t
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<GOAL>CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K.sieves (G.obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ A<VAR>ℱ' : CategoryTheory.Sheaf K A<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : A<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((G.op.comp ℱ).obj X_1)), (CategoryTheory.Functor.IsCoverDense.homOver α X).app X_1 a = CategoryTheory.CategoryStruct.comp a (α.app X_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>α : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : A<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((G.op.comp ℱ'.val).obj X_1)), (CategoryTheory.Functor.IsCoverDense.isoOver α X).inv.app X_1 a = CategoryTheory.CategoryStruct.comp a (α.inv.app X_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>α : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : A<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.coyoneda.obj (Opposite.op X)).obj ((G.op.comp ℱ.val).obj X_1)), (CategoryTheory.Functor.IsCoverDense.isoOver α X).hom.app X_1 a = CategoryTheory.CategoryStruct.comp a (α.hom.app X_1)
<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_6, u_4} A<VAR>ℱ : CategoryTheory.Sheaf K A<VAR>X : A<VAR>U : D<VAR>T : CategoryTheory.Sieve U<VAR>hT : T ∈ K.sieves U<VAR>x : CategoryTheory.Presieve.FamilyOfElements (ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) T.arrows<VAR>hx : x.Compatible<VAR>t : (ℱ.val.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).obj (Opposite.op U)<VAR>h : x.IsAmalgamation t<GOAL>t = ⋯.amalgamate x hx
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<VAR>x : (G.op.comp ℱ).obj (Opposite.op Y)<GOAL>ℱ'.val.map i.op (α.app (Opposite.op Y) x) = α.app (Opposite.op X) (ℱ.map i.op x)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X Y : C<VAR>i : G.obj X ⟶ G.obj Y<GOAL>CategoryTheory.CategoryStruct.comp (α.app (Opposite.op Y)) (ℱ'.val.map i.op) = CategoryTheory.CategoryStruct.comp (ℱ.map i.op) (α.app (Opposite.op X))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (Opposite.op X)<GOAL>CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x = fun x_1 x_2 hf => ℱ'.val.map (Nonempty.some hf).lift.op (α.app (Opposite.op (Nonempty.some hf).1) (ℱ.map (Nonempty.some hf).map.op x))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (Opposite.op X)<GOAL>(CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x).Compatible
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : D<VAR>x : ℱ.obj (Opposite.op X)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<GOAL>CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x f ⋯ = α.app (Opposite.op Y) (ℱ.map f.op x)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : D<VAR>Y : C<VAR>f : Opposite.op X ⟶ Opposite.op (G.obj Y)<VAR>x : ℱ.obj (Opposite.op X)<GOAL>ℱ'.val.map f (CategoryTheory.Functor.IsCoverDense.Types.appHom α X x) = α.app (Opposite.op Y) (ℱ.map f x)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : D<VAR>Y : C<VAR>f : Opposite.op X ⟶ Opposite.op (G.obj Y)<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.Types.appHom α X) (ℱ'.val.map f) = CategoryTheory.CategoryStruct.comp (ℱ.map f) (α.app (Opposite.op Y))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : D<GOAL>∀ (a : ℱ'.val.obj (Opposite.op X)), (CategoryTheory.Functor.IsCoverDense.Types.appIso i X).inv a = CategoryTheory.Functor.IsCoverDense.Types.appHom i.inv X a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : D<GOAL>∀ (a : ℱ.val.obj (Opposite.op X)), (CategoryTheory.Functor.IsCoverDense.Types.appIso i X).hom a = CategoryTheory.Functor.IsCoverDense.Types.appHom i.hom X a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)<VAR>ℱ' : CategoryTheory.SheafOfTypes K<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : Dᵒᵖ<GOAL>∀ (a : ℱ.obj (Opposite.op (Opposite.unop X))), (CategoryTheory.Functor.IsCoverDense.Types.presheafHom α).app X a = CategoryTheory.Functor.IsCoverDense.Types.appHom α (Opposite.unop X) a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : Dᵒᵖ<GOAL>∀ (a : ℱ.val.obj X), (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).hom.app X a = CategoryTheory.Functor.IsCoverDense.Types.appHom i.hom (Opposite.unop X) a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : Dᵒᵖ<GOAL>∀ (a : ℱ'.val.obj X), (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).inv.app X a = CategoryTheory.Functor.IsCoverDense.Types.appHom i.inv (Opposite.unop X) a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<GOAL>(CategoryTheory.Functor.IsCoverDense.Types.sheafIso i).hom.val = (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.SheafOfTypes K<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<GOAL>(CategoryTheory.Functor.IsCoverDense.Types.sheafIso i).inv.val = (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ A<VAR>ℱ' : CategoryTheory.Sheaf K A<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<VAR>X : Aᵒᵖ<GOAL>(CategoryTheory.Functor.IsCoverDense.sheafCoyonedaHom α).app X = CategoryTheory.Functor.IsCoverDense.Types.presheafHom (CategoryTheory.Functor.IsCoverDense.homOver α (Opposite.unop X))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<VAR>X : Dᵒᵖ<GOAL>(CategoryTheory.Functor.IsCoverDense.presheafIso i).hom.app X = CategoryTheory.yoneda.preimage ((CategoryTheory.Functor.IsCoverDense.sheafYonedaHom i.hom).app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<GOAL>(CategoryTheory.Functor.IsCoverDense.presheafIso i).inv = CategoryTheory.inv (CategoryTheory.Functor.IsCoverDense.sheafHom i.hom)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<GOAL>(CategoryTheory.Functor.IsCoverDense.sheafIso i).inv.val = (CategoryTheory.Functor.IsCoverDense.presheafIso i).inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_7, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>i : G.op.comp ℱ.val ≅ G.op.comp ℱ'.val<GOAL>(CategoryTheory.Functor.IsCoverDense.sheafIso i).hom.val = (CategoryTheory.Functor.IsCoverDense.presheafIso i).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ A<VAR>ℱ' : CategoryTheory.Sheaf K A<VAR>α : G.op.comp ℱ ⟶ G.op.comp ℱ'.val<GOAL>CategoryTheory.whiskerLeft G.op (CategoryTheory.Functor.IsCoverDense.sheafHom α) = α
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ : CategoryTheory.Functor Dᵒᵖ A<VAR>ℱ' : CategoryTheory.Sheaf K A<VAR>α : ℱ ⟶ ℱ'.val<GOAL>CategoryTheory.Functor.IsCoverDense.sheafHom (CategoryTheory.whiskerLeft G.op α) = α
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_7, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>A : Type u_4<VAR>CategoryTheory.Category.{u_6, u_4} A<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>ℱ ℱ' : CategoryTheory.Sheaf K A<VAR>α : ℱ ⟶ ℱ'<VAR>i : CategoryTheory.IsIso (CategoryTheory.whiskerLeft G.op α.val)<GOAL>CategoryTheory.IsIso α
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsCoverDense K<VAR>G.IsLocallyFull K<VAR>G.IsLocallyFaithful K<GOAL>CategoryTheory.CompatiblePreserving K G