ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>S : IntermediateField K L'<VAR>h : S ≤ f.fieldRange<GOAL>IntermediateField.map f (IntermediateField.comap f S) = S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>hf : Function.Surjective ⇑f<VAR>S : IntermediateField K L'<GOAL>IntermediateField.map f (IntermediateField.comap f S) = S
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>Field K<VAR>Field L<VAR>Field L'<VAR>Algebra K L<VAR>Algebra K L'<VAR>f : L →ₐ[K] L'<VAR>S : IntermediateField K L<GOAL>IntermediateField.comap f (IntermediateField.map f S) = S
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>self : G.LocallyCoverDense 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_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.LocallyCoverDense K<VAR>G.Full<VAR>G.Faithful<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>K.sieves (G.obj X) (CategoryTheory.Sieve.functorPushforward G S) ↔ ∃ T, CategoryTheory.Sieve.functorPullback G ↑T = S
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.LocallyCoverDense K<VAR>G.IsLocallyFull K<VAR>G.IsLocallyFaithful K<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(G.inducedTopology K).sieves X S = K.sieves (G.obj X) (CategoryTheory.Sieve.functorPushforward G S)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>G : CategoryTheory.Functor C D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G.LocallyCoverDense K<VAR>G.IsLocallyFull K<VAR>G.IsLocallyFaithful K<GOAL>CategoryTheory.CoverPreserving (G.inducedTopology K) K G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : C ⥤ D<VAR>self : CategoryTheory.CoverPreserving J K G<VAR>U : C<VAR>S : CategoryTheory.Sieve U<GOAL>S ∈ J.sieves U → CategoryTheory.Sieve.functorPushforward G S ∈ K.sieves (G.obj U)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>CategoryTheory.CoverPreserving J J (𝟭 C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>A : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>L : CategoryTheory.GrothendieckTopology A<VAR>F : C ⥤ D<VAR>hF : CategoryTheory.CoverPreserving J K F<VAR>G : D ⥤ A<VAR>hG : CategoryTheory.CoverPreserving K L G<GOAL>CategoryTheory.CoverPreserving J L (F ⋙ G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : C ⥤ D<VAR>self : CategoryTheory.CompatiblePreserving K G<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>Z : C<VAR>T : CategoryTheory.Presieve Z<VAR>x : CategoryTheory.Presieve.FamilyOfElements (G.op ⋙ ℱ.val) T<GOAL>x.Compatible → ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂), f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : C ⥤ D<VAR>hG : CategoryTheory.CompatiblePreserving K G<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>Z : C<VAR>T : CategoryTheory.Presieve Z<VAR>x : CategoryTheory.Presieve.FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<GOAL>(CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x).Compatible
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : C ⥤ D<VAR>hG : CategoryTheory.CompatiblePreserving K G<VAR>ℱ : CategoryTheory.SheafOfTypes K<VAR>Z : C<VAR>T : CategoryTheory.Presieve Z<VAR>x : CategoryTheory.Presieve.FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>h : x.Compatible<VAR>Y : C<VAR>f : Y ⟶ Z<VAR>hf : T f<GOAL>CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>G : C ⥤ D<VAR>CategoryTheory.RepresentablyFlat G<GOAL>CategoryTheory.CompatiblePreserving K G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>F : C ⥤ D<VAR>F.Full<VAR>F.Faithful<VAR>hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)<GOAL>CategoryTheory.CompatiblePreserving K F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>hF₁ : CategoryTheory.CompatiblePreserving K F<VAR>hF₂ : CategoryTheory.CoverPreserving J K F<GOAL>F.IsContinuous J K
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S : C<VAR>self : CategoryTheory.PreOneHypercover S<VAR>i₁ i₂ : self.I₀<VAR>j : self.I₁ i₁ i₂<GOAL>CategoryTheory.CategoryStruct.comp (self.p₁ j) (self.f i₁) = CategoryTheory.CategoryStruct.comp (self.p₂ j) (self.f i₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>W : C<VAR>p₁ : W ⟶ E.X i₁<VAR>p₂ : W ⟶ E.X i₂<VAR>Z : C<VAR>g : Z ⟶ W<GOAL>(E.sieve₁ p₁ p₂).arrows g = ∃ j h, CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (E.p₁ j) ∧ CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (E.p₂ j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)<VAR>W : C<VAR>p₁ : W ⟶ E.X i₁<VAR>p₂ : W ⟶ E.X i₂<VAR>w : CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂)<GOAL>E.sieve₁ p₁ p₂ = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)<GOAL>E.sieve₁' i₁ i₂ = E.sieve₁ (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂)) (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>j : E.I₁'<GOAL>(E.multicospanIndex F).right j = F.obj (Opposite.op (E.Y j.snd))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>j : E.I₁'<GOAL>(E.multicospanIndex F).fst j = F.map (E.p₁ j.snd).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>j : E.I₁'<GOAL>(E.multicospanIndex F).snd j = F.map (E.p₂ j.snd).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>j : E.I₁'<GOAL>(E.multicospanIndex F).sndTo j = j.fst.2
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>(E.multicospanIndex F).L = E.I₀
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>i : E.I₀<GOAL>(E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>j : E.I₁'<GOAL>(E.multicospanIndex F).fstTo j = j.fst.1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} A<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>(E.multicospanIndex F).R = E.I₁'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : C<VAR>self : J.OneHypercover S<GOAL>self.sieve₀ ∈ J.sieves S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : C<VAR>self : J.OneHypercover S<VAR>i₁ i₂ : self.I₀<VAR>W : C<VAR>p₁ : W ⟶ self.X i₁<VAR>p₂ : W ⟶ self.X i₂<VAR>w : CategoryTheory.CategoryStruct.comp p₁ (self.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (self.f i₂)<GOAL>self.sieve₁ p₁ p₂ ∈ J.sieves W
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : C<VAR>E : J.OneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)<GOAL>E.sieve₁' i₁ i₂ ∈ J.sieves (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : C<VAR>E : CategoryTheory.PreOneHypercover S<VAR>E.HasPullbacks<VAR>mem₀ : E.sieve₀ ∈ J.sieves S<VAR>mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J.sieves (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))<GOAL>(CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁').toPreOneHypercover = E
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>S : C<VAR>E : J.OneHypercover S<VAR>F : CategoryTheory.Sheaf J A<VAR>c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.val)<VAR>i₀ : E.I₀<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c) (F.val.map (E.f i₀).op) = c.ι i₀
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>∀ (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.Y r = r.Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>S.preOneHypercover.I₀ = S.Arrow
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>∀ (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.p₂ r = r.g₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>f₁ f₂ : S.Arrow<GOAL>S.preOneHypercover.I₁ f₁ f₂ = f₁.Relation f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>∀ (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.p₁ r = r.g₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>f : S.Arrow<GOAL>S.preOneHypercover.X f = f.Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>f : S.Arrow<GOAL>S.preOneHypercover.f f = f.f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>S.preOneHypercover.sieve₀ = ↑S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<VAR>f₁ f₂ : S.Arrow<VAR>W : C<VAR>p₁ : W ⟶ f₁.Y<VAR>p₂ : W ⟶ f₂.Y<VAR>w : CategoryTheory.CategoryStruct.comp p₁ f₁.f = CategoryTheory.CategoryStruct.comp p₂ f₂.f<GOAL>S.preOneHypercover.sieve₁ p₁ p₂ = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : J.Cover X<GOAL>S.oneHypercover.toPreOneHypercover = S.preOneHypercover
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>self : CategoryTheory.HasSheafify J A<GOAL>CategoryTheory.HasWeakSheafify J A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>self : CategoryTheory.HasSheafify J A<GOAL>Nonempty (CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>F : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj : F ⊣ CategoryTheory.sheafToPresheaf J A<VAR>CategoryTheory.Limits.PreservesFiniteLimits F<GOAL>CategoryTheory.HasSheafify J A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(CategoryTheory.sheafificationAdjunction J D).unit.app P = CategoryTheory.toSheafify J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafify J P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<GOAL>CategoryTheory.sheafifyMap J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyMap J γ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp η (CategoryTheory.toSheafify J Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyMap J η)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(CategoryTheory.sheafification J D).obj P = CategoryTheory.sheafify J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<GOAL>(CategoryTheory.sheafification J D).map η = CategoryTheory.sheafifyMap J η
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<GOAL>(CategoryTheory.toSheafification J D).app P = CategoryTheory.toSheafify J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>CategoryTheory.IsIso (CategoryTheory.toSheafify J P)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(CategoryTheory.isoSheafify J hP).hom = CategoryTheory.toSheafify J P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.sheafificationAdjunction J D).counit.app P).val = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P.val) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) (CategoryTheory.sheafifyLift J η hQ) = η
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>γ : CategoryTheory.sheafify J P ⟶ Q<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ = η → γ = CategoryTheory.sheafifyLift J η hQ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>(CategoryTheory.isoSheafify J hP).inv = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id P) hP
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q : CategoryTheory.Functor Cᵒᵖ D<VAR>η γ : CategoryTheory.sheafify J P ⟶ Q<VAR>hQ : CategoryTheory.Presheaf.IsSheaf J Q<VAR>h : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) γ<GOAL>η = γ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P Q R : CategoryTheory.Functor Cᵒᵖ D<VAR>η : P ⟶ Q<VAR>γ : Q ⟶ R<VAR>hR : CategoryTheory.Presheaf.IsSheaf J R<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafifyMap J η) (CategoryTheory.sheafifyLift J γ hR) = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.comp η γ) hR
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Sheaf J D<GOAL>(CategoryTheory.sheafificationIso P).hom.val = (CategoryTheory.isoSheafify J ⋯).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>P : CategoryTheory.Sheaf J D<GOAL>(CategoryTheory.sheafificationIso P).inv.val = (CategoryTheory.isoSheafify J ⋯).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>X : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.sheafificationNatIso J D).hom.app X).val = CategoryTheory.toSheafify J X.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>X : CategoryTheory.Sheaf J D<GOAL>((CategoryTheory.sheafificationNatIso J D).inv.app X).val = CategoryTheory.sheafifyLift J (CategoryTheory.CategoryStruct.id X.val) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X ⟶ Y<GOAL>(α.homCongr β) f = CategoryTheory.CategoryStruct.comp α.inv (CategoryTheory.CategoryStruct.comp f β.hom)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X₁ ⟶ Y₁<GOAL>(α.homCongr β).symm f = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp f β.inv)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z X₁ Y₁ Z₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>γ : Z ≅ Z₁<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(α.homCongr γ) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((α.homCongr β) f) ((β.homCongr γ) g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>((CategoryTheory.Iso.refl X).homCongr (CategoryTheory.Iso.refl Y)) f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ Y₁ X₂ Y₂ X₃ Y₃ : C<VAR>α₁ : X₁ ≅ X₂<VAR>β₁ : Y₁ ≅ Y₂<VAR>α₂ : X₂ ≅ X₃<VAR>β₂ : Y₂ ≅ Y₃<VAR>f : X₁ ⟶ Y₁<GOAL>((α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂)) f = ((α₁.homCongr β₁).trans (α₂.homCongr β₂)) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>α : X₁ ≅ X₂<VAR>β : Y₁ ≅ Y₂<GOAL>(α.homCongr β).symm = α.symm.homCongr β.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ≅ X₂<VAR>g : Y₁ ≅ Y₂<VAR>h : X₁ ≅ Y₁<GOAL>(f.isoCongr g) h = f.symm ≪≫ h ≪≫ g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ≅ X₂<VAR>g : Y₁ ≅ Y₂<VAR>h : X₂ ≅ Y₂<GOAL>(f.isoCongr g).symm h = f ≪≫ h ≪≫ g.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X ⟶ Y<GOAL>F.map ((α.homCongr β) f) = ((F.mapIso α).homCongr (F.mapIso β)) (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X ≅ Y<GOAL>F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w₁<VAR>CategoryTheory.Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>CategoryTheory.Category.{max v u, w₂} E<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) D<VAR>∀ (α β : Type (max v u)) (fst snd : β → α), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan fst snd) E<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>F : CategoryTheory.Functor D E<VAR>(F : CategoryTheory.Functor D E) → (X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>(F : CategoryTheory.Functor D E) → (X : C) → (W : J.Cover X) → (P : CategoryTheory.Functor Cᵒᵖ D) → CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F<GOAL>(J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom