ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>x : PrimeSpectrum R<VAR>m : M<VAR>hm : ∀ r ∉ x.asIdeal, r • m ≠ 0<GOAL>∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0
<VAR>R : Type u_1<VAR>l : ℕ<VAR>hl : Squarefree l<GOAL>|μ l| = 1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>m n : ℤ<GOAL>a ^ (m + n) = a ^ m * a ^ n
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>m : ℤ<GOAL>a ^ (m + 0) = a ^ m * a ^ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n<GOAL>a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a b c : G₀<VAR>ha : a ≠ 0<VAR>m : ℤ<VAR>n : ℕ<VAR>ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)<GOAL>a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>F : A → C ⥤ C<VAR>zero : F 0 ≅ 𝟭 C<VAR>add : (n m : A) → F (n + m) ≅ F n ⋙ F m<VAR>m₁ m₂ m₃ : A<VAR>X : C<GOAL>(F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>F : A → C ⥤ C<VAR>zero : F 0 ≅ 𝟭 C<VAR>add : (n m : A) → F (n + m) ≅ F n ⋙ F m<VAR>assoc_hom_app : autoParam (∀ (m₁ m₂ m₃ : A) (X : C), (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) = eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)) _auto✝<VAR>n : A<VAR>X : C<GOAL>(F (0 + n)).obj X = (F n).obj X
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : AddMonoid A<VAR>F : A → C ⥤ C<VAR>zero : F 0 ≅ 𝟭 C<VAR>add : (n m : A) → F (n + m) ≅ F n ⋙ F m<VAR>assoc_hom_app : autoParam (∀ (m₁ m₂ m₃ : A) (X : C), (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) = eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)) _auto✝<VAR>zero_add_hom_app : autoParam (∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)) _auto✝<VAR>n : A<VAR>X : C<GOAL>(F (n + 0)).obj X = (F n).obj X
<VAR>n : ℕ<GOAL>Ico 0 n = range n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l m : Language α<VAR>a b x✝ x : List α<GOAL>x ∈ 1 ↔ x = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>s : Set α<GOAL>f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X ≫ (λ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X ≫ F.ε ▷ F.obj X ≫ F.μ (𝟙_ C) X ≫ F.map (λ_ X).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ (𝟙 (F.obj (𝟙_ C) ⊗ F.obj X) ≫ F.μ (𝟙_ C) X) ≫ F.map (λ_ X).hom
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<GOAL>(conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A))) = (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<GOAL>(conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A))) = (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>({ toFun := fun α => whiskerLeft (F ⋙ prod.functor.obj (F.obj A)) h.unit ≫ whiskerRight (whiskerLeft F α) F ≫ whiskerRight h.counit (prod.functor.obj A ⋙ F), invFun := fun β => whiskerRight h.unit (prod.functor.obj (F.obj A) ⋙ L) ≫ whiskerRight (whiskerLeft L β) L ≫ whiskerLeft (L ⋙ prod.functor.obj A) h.counit, left_inv := ⋯, right_inv := ⋯ } (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))).app B = (prodComparisonNatIso F A).inv.app B
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>h.unit.app (F.obj A ⨯ F.obj B) ≫ F.map (prodComparison L (F.obj A) (F.obj B)) ≫ F.map (prod.map (h.counit.app A) (𝟙 (L.obj (F.obj B)))) ≫ F.map (prod.map (𝟙 A) (h.counit.app B)) = inv (prodComparison F A B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>h.unit.app (F.obj A ⨯ F.obj B) ≫ F.map (prodComparison L (F.obj A) (F.obj B) ≫ prod.map (h.counit.app A) (𝟙 (L.obj (F.obj B))) ≫ prod.map (𝟙 A) (h.counit.app B)) = inv (prodComparison F A B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>h.unit.app (F.obj A ⨯ F.obj B) ≫ F.map (prodComparison L (F.obj A) (F.obj B) ≫ prod.map (h.counit.app A) (h.counit.app B)) = inv (prodComparison F A B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>(h.unit.app (F.obj A ⨯ F.obj B) ≫ F.map (prodComparison L (F.obj A) (F.obj B) ≫ prod.map (h.counit.app A) (h.counit.app B))) ≫ prodComparison F A B = 𝟙 (F.obj A ⨯ F.obj B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>h.unit.app (F.obj A ⨯ F.obj B) ≫ F.map (prodComparison L (F.obj A) (F.obj B)) ≫ prodComparison F (L.obj (F.obj A)) (L.obj (F.obj B)) ≫ prod.map (F.map (h.counit.app A)) (F.map (h.counit.app B)) = 𝟙 (F.obj A ⨯ F.obj B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>h.unit.app (F.obj A ⨯ F.obj B) ≫ prodComparison (L ⋙ F) (F.obj A) (F.obj B) ≫ prod.map (F.map (h.counit.app A)) (F.map (h.counit.app B)) = 𝟙 (F.obj A ⨯ F.obj B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<GOAL>(h.unit.app (F.obj A ⨯ F.obj B) ≫ prodComparison (L ⋙ F) (F.obj A) (F.obj B)) ≫ prod.map (F.map (h.counit.app A)) (F.map (h.counit.app B)) = 𝟙 (F.obj A ⨯ F.obj B)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>conjeq : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) ((mateEquiv h h) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))) = (conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft L (prod.functor.map (h.counit.app A)))<VAR>B : C<VAR>ηlemma : h.unit.app (F.obj A ⨯ F.obj B) ≫ prod.lift ((L ⋙ F).map prod.fst) ((L ⋙ F).map prod.snd) = prod.map (h.unit.app (F.obj A)) (h.unit.app (F.obj B))<GOAL>prod.map (h.unit.app (F.obj A)) (h.unit.app (F.obj B)) ≫ prod.map (F.map (h.counit.app A)) (F.map (h.counit.app B)) = 𝟙 (F.obj A ⨯ F.obj B)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<GOAL>f = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : X ≅ 0<VAR>h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f<GOAL>f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : HasFiniteIntegral f μ<VAR>hν : HasFiniteIntegral f ν<GOAL>HasFiniteIntegral f (μ + ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤<VAR>hν : ∫⁻ (a : α), ↑‖f a‖₊ ∂ν < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ∂μ + ∫⁻ (a : α), ↑‖f a‖₊ ∂ν < ⊤
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>x₀ : X<GOAL>EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>hu : u ∈ 𝓤 (β × β')<GOAL>∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p', ∀ x ∈ s ×ˢ s', ((fun i => Prod.map (F i.1) (F' i.2)) m.1 x, (fun i => Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>hu : ∃ t₁ ∈ 𝓤 β, ∃ t₂ ∈ 𝓤 β', t₁ ×ˢ t₂ ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u<GOAL>∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p', ∀ x ∈ s ×ˢ s', ((fun i => Prod.map (F i.1) (F' i.2)) m.1 x, (fun i => Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>v : Set (β × β)<VAR>hv : v ∈ 𝓤 β<VAR>w : Set (β' × β')<VAR>hw : w ∈ 𝓤 β'<VAR>hvw : v ×ˢ w ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u<GOAL>∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p', ∀ x ∈ s ×ˢ s', ((fun i => Prod.map (F i.1) (F' i.2)) m.1 x, (fun i => Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>v : Set (β × β)<VAR>hv : v ∈ 𝓤 β<VAR>w : Set (β' × β')<VAR>hw : w ∈ 𝓤 β'<VAR>hvw : v ×ˢ w ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u<GOAL>∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p', ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>v : Set (β × β)<VAR>hv : v ∈ 𝓤 β<VAR>w : Set (β' × β')<VAR>hw : w ∈ 𝓤 β'<VAR>hvw : (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u<GOAL>∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p', ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>v : Set (β × β)<VAR>hv : v ∈ 𝓤 β<VAR>w : Set (β' × β')<VAR>hw : w ∈ 𝓤 β'<VAR>hvw : (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u<GOAL>∀ (x : (ι × ι') × ι × ι'), ((∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧ ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w) → ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s'✝ : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p'✝ : Filter α<VAR>g : ι → α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>inst✝ : UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : UniformCauchySeqOn F p s<VAR>h' : UniformCauchySeqOn F' p' s'<VAR>u : Set ((β × β') × β × β')<VAR>v : Set (β × β)<VAR>hv : v ∈ 𝓤 β<VAR>w : Set (β' × β')<VAR>hw : w ∈ 𝓤 β'<VAR>hvw : (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u<VAR>x : (ι × ι') × ι × ι'<VAR>hx : (∀ x_1 ∈ s, (F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 x_1, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.2 x_1) ∈ v) ∧ ∀ x_1 ∈ s', (F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 x_1, F' ((x.1.1, x.2.1), x.1.2, x.2.2).2.2 x_1) ∈ w<VAR>a : α<VAR>b : α'<VAR>ha : a ∈ s<VAR>hb : b ∈ s'<GOAL>((F x.1.1 a, F' x.1.2 b), F x.2.1 a, F' x.2.2 b) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>Pairwise (fun a b => b ≠ a) l ↔ l.Nodup
<VAR>num : ℕ<VAR>den : ℤ<VAR>n : ℕ<GOAL>(↑num /. den) ^ n = ↑num ^ n /. den ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : CompleteSpace α<VAR>f : β → α<GOAL>Multipliable f ↔ CauchySeq fun s => ∏ b ∈ s, f b
<VAR>N✝ N : ℕ<VAR>γ : SL(2, ℤ)<GOAL>γ ∈ Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
<VAR>N✝ N : ℕ<VAR>γ : SL(2, ℤ)<GOAL>(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ s} ∂ν a = (κ a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ ∅} ∂ν a = (κ a) ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∀ t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}, ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set (β × ℝ)<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set (β × ℝ)), MeasurableSet t → ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ t} ∂ν a = (κ a) t → ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ tᶜ} ∂ν a = (κ a) tᶜ