ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j : J<VAR>U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ<GOAL>((opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (𝟙 j))).app U = ((opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j)) (𝟙 ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j))).app U
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<GOAL>{ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (f ≫ g) = { obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map f ≫ { obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map g
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<GOAL>(opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₁) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₃)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (f ≫ g)) = (opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₁) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₃)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map f ≫ { obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map g)
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ<GOAL>((opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₁) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₃)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map (f ≫ g))).app U = ((opEquiv ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₁) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.obj j₃)) ({ obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map f ≫ { obj := fun j => op ((pushforward C (colimit.ι (F ⋙ forget C) j)).obj (F.obj j).presheaf), map := fun {j j'} f => ((pushforward C (colimit.ι (F ⋙ forget C) j')).map (F.map f).c ≫ (Pushforward.comp ((F ⋙ forget C).map f) (colimit.ι (F ⋙ forget C) j') (F.obj j).presheaf).inv ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom).op }.map g)).app U
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ<GOAL>(F.map (f ≫ g)).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ 𝟙 ((F.obj j₁).presheaf.obj (op ((Opens.map (F.map (f ≫ g)).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U = ((F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ 𝟙 ((F.obj j₂).presheaf.obj (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₂).presheaf).hom.app U) ≫ (F.map f).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))) ≫ 𝟙 ((F.obj j₁).presheaf.obj (op ((Opens.map (F.map f).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ<VAR>this : op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) = op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))<GOAL>(F.map (f ≫ g)).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ 𝟙 ((F.obj j₁).presheaf.obj (op ((Opens.map (F.map (f ≫ g)).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U = ((F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ 𝟙 ((F.obj j₂).presheaf.obj (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₂).presheaf).hom.app U) ≫ (F.map f).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))) ≫ 𝟙 ((F.obj j₁).presheaf.obj (op ((Opens.map (F.map f).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))))) ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U
<VAR>J : Type u'<VAR>inst✝² : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimitsOfShape J TopCat<VAR>F : J ⥤ PresheafedSpace C<VAR>j₁ j₂ j₃ : J<VAR>f : j₁ ⟶ j₂<VAR>g : j₂ ⟶ j₃<VAR>U : (Opens ↑(colimit (F ⋙ forget C)))ᵒᵖ<VAR>this : op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) = op ((Opens.map (colimit.ι (F ⋙ forget C) j₂)).obj (unop U))<GOAL>(F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫ (F.obj j₁).presheaf.map (eqToHom ⋯) = (F.map g).c.app (op ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U))) ≫ (F.map f).c.app (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj (unop U)))) ≫ (F.obj j₁).presheaf.map ((Opens.map (F.map f).base).map (eqToHom ⋯)).op ≫ (F.obj j₁).presheaf.map (eqToHom ⋯)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : CompactSpace α<VAR>f g : C(α, 𝕜)<GOAL>⟪(ContinuousMap.toLp 2 μ 𝕜) f, (ContinuousMap.toLp 2 μ 𝕜) g⟫_𝕜 = ∫ (x : α), (starRingEnd 𝕜) (f x) * g x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : CompactSpace α<VAR>f g : C(α, 𝕜)<GOAL>(fun a => ⟪↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a, ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : CompactSpace α<VAR>f g : C(α, 𝕜)<VAR>hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<GOAL>(fun a => ⟪↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a, ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : CompactSpace α<VAR>f g : C(α, 𝕜)<VAR>hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<VAR>hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g<GOAL>(fun a => ⟪↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a, ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : CompactSpace α<VAR>f g : C(α, 𝕜)<VAR>hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<VAR>hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g<VAR>a✝ : α<VAR>hf : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝ = f a✝<VAR>hg : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a✝ = g a✝<GOAL>⟪↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝, ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a✝⟫_𝕜 = (starRingEnd 𝕜) (f a✝) * g a✝
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>r : R<VAR>n : ℕ<GOAL>(C r).coeff (n + 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R<VAR>ha : a ∈ I<GOAL>((Quotient.mk (map C I)).comp C) a = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R<VAR>ha : a ∈ I<GOAL>C a ∈ map C I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝² : (i : ι) → DecidableEq (γ i)<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → Zero (γ i)<VAR>f : (i : ι) → γ i → β i<VAR>x : (i : ι) → γ i<VAR>hf : ∀ (i : ι), f i 0 = 0<GOAL>(hammingNorm fun i => f i (x i)) ≤ hammingNorm x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>hf : Injective ⇑f<VAR>H K : Subgroup G<GOAL>map f H ≤ map f K ↔ H ≤ K
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<GOAL>((constantCommuteCompose J U).app (F.val.obj (op t))).hom ≫ (constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F) = (sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<GOAL>(presheafToSheaf J B).map ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app F) = (presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app F)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<GOAL>((presheafToSheaf J B).map ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app F) = (((presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t)))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app F)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<GOAL>(presheafToSheaf J B).map ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val = ((presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t)))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>(presheafToSheaf J B).map ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val = ((presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t)))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>(presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (presheafToSheaf J B).map { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val = (presheafToSheaf J B).map ((compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t))) ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F✝ F : Sheaf J A<VAR>this : (compConstIso Cᵒᵖ U).hom.app (F.val.obj (op t)) ≫ { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } = (constantPresheafAdj B ht).counit.app (F.val ⋙ U)<GOAL>(presheafToSheaf J B).map { app := fun Y => (F.val ⋙ U).map (ht.from (unop Y)).op, naturality := ⋯ } ≫ (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app F.val = (sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((const Cᵒᵖ).obj (F.val.obj (op t))) ≫ (sheafCompose J U).map ((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val))