ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<VAR>K_compact : IsCompact K<GOAL>Integrable (K.indicator fun x => ↑C * ‖v‖ * ‖g x‖) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<VAR>K_compact : IsCompact K<GOAL>∀ᵐ (a : E) ∂μ, Tendsto (fun n => n⁻¹ • (f (a + n • v) - f a) * g a) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f a v * g a))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>toDual (s.min' hs) = (image (⇑toDual) s).max' ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>↑(toDual (s.min' hs)) = ↑((image (⇑toDual) s).max' ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s.sup (WithBot.some ∘ fun x => toDual x) = s.sup ((WithBot.some ∘ fun x => x) ∘ ⇑toDual)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Norm α<VAR>inst✝ : Norm β<VAR>f : WithLp 0 (α × β)<GOAL>‖f‖ = (if ‖f.1‖ = 0 then 0 else 1) + if ‖f.2‖ = 0 then 0 else 1
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ o.oangle y x = ↑π
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Ioc a b ↔ a < x ∧ x ≤ b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>hf : Surjective ⇑f<GOAL>f.FiniteType
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>hf : Surjective ⇑f<GOAL>(f.comp (RingHom.id A)).FiniteType
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<GOAL>count p 0 = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hϖ : Irreducible ϖ<GOAL>(addVal R) ϖ = 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G<VAR>f : Fin n → G<VAR>a b : k<GOAL>mapDomain (actionDiagonalSucc G n).inv.hom ((lcongr (Equiv.refl (G × (Fin n → G))) (TensorProduct.lid k k)) ((finsuppTensorFinsupp k k k k G (Fin n → G)) (single g a ⊗ₜ[k] single f b))) = single (g • partialProd f) (a * b)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>g : G<VAR>f : Fin n → G<VAR>a b : k<GOAL>single (g • partialProd f) ((TensorProduct.lid k k) (a ⊗ₜ[k] b)) = single (g • partialProd f) (a * b)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : Limits.IsInitial A<GOAL>F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : ListBlank Γ<VAR>n : ℕ<GOAL>l.nth (n + 1) = l.tail.nth n
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : ListBlank Γ<VAR>n : ℕ<GOAL>(cons l.head l.tail).nth (n + 1) = l.tail.nth n
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<GOAL>AntitoneOn (fun x => dist x y) (Iic y)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>y₁ : ι → ℝ<VAR>hy₁ : y₁ ∈ Iic y<VAR>y₂ : ι → ℝ<VAR>hy₂ : y₂ ∈ Iic y<VAR>hy : y₁ ≤ y₂<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>y₁ : ι → ℝ<VAR>hy₁ : y₁ ∈ Iic y<VAR>y₂ : ι → ℝ<VAR>hy₂ : y₂ ∈ Iic y<VAR>hy : y₁ ≤ y₂<VAR>i : ι<VAR>x✝ : i ∈ Finset.univ<GOAL>(y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>W✝ X✝ Y✝ Z✝ : Dial C<VAR>f : W✝ ⟶ X✝<VAR>g : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<GOAL>(f ≫ g) ≫ h = f ≫ g ≫ h
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>W✝ X✝ Y✝ Z✝ : Dial C<VAR>f : W✝ ⟶ X✝<VAR>g : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<GOAL>π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z✝.tgt) ≫ h.F) ≫ π(π₁, prod.map f.f (𝟙 Y✝.tgt) ≫ g.F) ≫ f.F = π(π₁, prod.map f.f (𝟙 Z✝.tgt) ≫ π(π₁, prod.map g.f (𝟙 Z✝.tgt) ≫ h.F) ≫ g.F) ≫ f.F
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>W✝ X✝ Y✝ Z✝ : Dial C<VAR>f : W✝ ⟶ X✝<VAR>g : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<GOAL>(π(π₁, prod.map (f.f ≫ g.f) (𝟙 Z✝.tgt) ≫ h.F) ≫ π(π₁, prod.map f.f (𝟙 Y✝.tgt) ≫ g.F)) ≫ f.F = π(π₁, (prod.map f.f (𝟙 Z✝.tgt) ≫ π(π₁, prod.map g.f (𝟙 Z✝.tgt) ≫ h.F)) ≫ g.F) ≫ f.F
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y)) = Multiset.map Associates.out (Multiset.map Associates.mk (normalizedFactors (x * y)))
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>Multiset.map Associates.mk (normalizedFactors x + normalizedFactors y) = Multiset.map Associates.mk (normalizedFactors (x * y))
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>Multiset.Rel Setoid.r (normalizedFactors x + normalizedFactors y) (normalizedFactors (x * y))
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>∀ x_1 ∈ normalizedFactors x + normalizedFactors y, Irreducible x_1
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>∀ x_1 ∈ normalizedFactors (x * y), Irreducible x_1
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ⇑normalize = Associates.out ∘ Associates.mk<GOAL>(normalizedFactors x + normalizedFactors y).prod ~ᵤ (normalizedFactors (x * y)).prod
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = sum g fun a b => (f * single a b) x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(sum g fun a b => (f * single a b) x) = sum g fun a b => f (x * a⁻¹) * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝ : Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>i : ι<VAR>x : αs i<GOAL>(comapDomain (Sigma.mk i) l ⋯) x = l ⟨i, x⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>f : β → Set α<VAR>hf : Pairwise (Disjoint on f)<VAR>s : Set α<VAR>h'f : ∀ (t : β), f t ⊆ s<VAR>hs : s.Countable<GOAL>{t | (f t).Nonempty}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>f : β → Set α<VAR>hf : Pairwise (Disjoint on f)<VAR>s : Set α<VAR>h'f : ∀ (t : β), f t ⊆ s<VAR>hs : Countable ↑s<GOAL>Countable ↑{t | (f t).Nonempty}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>f : β → Set α<VAR>hf : Pairwise (Disjoint on f)<VAR>s : Set α<VAR>h'f : ∀ (t : β), f t ⊆ s<VAR>hs : Countable ↑s<VAR>F : { t // (f t).Nonempty } → ↑s<VAR>hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t<GOAL>Countable ↑{t | (f t).Nonempty}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>f : β → Set α<VAR>hf : Pairwise (Disjoint on f)<VAR>s : Set α<VAR>h'f : ∀ (t : β), f t ⊆ s<VAR>hs : Countable ↑s<VAR>F : { t // (f t).Nonempty } → ↑s<VAR>hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t<VAR>A : Injective F<GOAL>Countable ↑{t | (f t).Nonempty}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>a : α<VAR>h : a ∈ map (Embedding.subtype fun x => p x) s<GOAL>p a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<VAR>s : Finset { x // p x }<VAR>x : { x // p x }<VAR>left✝ : x ∈ s<VAR>h : (Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s<GOAL>p ((Embedding.subtype fun x => p x) x)
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>x : β<GOAL>x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>τ : Type u_2<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>(eval (⇑(eval g) ∘ f)) p = (eval g) (eval₂ C f p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>τ : Type u_2<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>(eval (⇑(eval g) ∘ f)) p = eval₂ ((eval g).comp C) (⇑(eval g) ∘ f) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>τ : Type u_2<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>(eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p = eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>τ : Type u_2<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → R<VAR>p : MvPolynomial σ R<GOAL>eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p = eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (eval₂ (RingHom.id R) g ∘ f) p
<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 Y Z : C<GOAL>inv (F.μ (X ⊗ Y) Z) ≫ inv (F.μ X Y) ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = F.map (α_ X Y Z).hom ≫ inv (F.μ X (Y ⊗ Z)) ≫ F.obj X ◁ inv (F.μ Y Z)
<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 Y Z : C<GOAL>(α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = F.μ X Y ▷ F.obj Z ≫ F.μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom ≫ inv (F.μ X (Y ⊗ Z)) ≫ F.obj X ◁ inv (F.μ Y Z)
<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 Y Z : C<GOAL>(α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = (((α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ F.μ Y Z ≫ F.μ X (Y ⊗ Z)) ≫ inv (F.μ X (Y ⊗ Z))) ≫ F.obj X ◁ inv (F.μ Y Z)
<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.obj X)).inv = F.map (λ_ X).inv ≫ inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj 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.obj X)).hom ≫ F.map (λ_ X).inv ≫ inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X = 𝟙 (𝟙_ D ⊗ F.obj 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.ε ▷ F.obj X ≫ F.μ (𝟙_ C) X ≫ F.map (λ_ X).hom) ≫ F.map (λ_ X).inv ≫ inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X = 𝟙 (𝟙_ D ⊗ F.obj 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.ε ▷ F.obj X ≫ F.μ (𝟙_ C) X ≫ (𝟙 (F.obj (𝟙_ C ⊗ X)) ≫ inv (F.μ (𝟙_ C) X)) ≫ inv F.ε ▷ F.obj X = 𝟙 (𝟙_ D ⊗ F.obj 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.obj X)).inv = F.map (ρ_ X).inv ≫ inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε
<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.obj X)).hom ≫ F.map (ρ_ X).inv ≫ inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε = 𝟙 (F.obj X ⊗ 𝟙_ D)
<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.obj X ◁ F.ε ≫ F.μ X (𝟙_ C) ≫ F.map (ρ_ X).hom) ≫ F.map (ρ_ X).inv ≫ inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε = 𝟙 (F.obj X ⊗ 𝟙_ D)
<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.obj X ◁ F.ε ≫ F.μ X (𝟙_ C) ≫ (𝟙 (F.obj (X ⊗ 𝟙_ C)) ≫ inv (F.μ X (𝟙_ C))) ≫ F.obj X ◁ inv F.ε = 𝟙 (F.obj X ⊗ 𝟙_ D)
<VAR>m n : ℕ+<GOAL>m ∣ n ↔ m.gcd n = m
<VAR>m n : ℕ+<GOAL>↑m ∣ ↑n ↔ m.gcd n = m
<VAR>m n : ℕ+<GOAL>(↑m).gcd ↑n = ↑m ↔ m.gcd n = m
<VAR>m n : ℕ+<GOAL>(↑m).gcd ↑n = ↑m ↔ ↑(m.gcd n) = ↑m
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>h : ¬p i<GOAL>(filter p f) i = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x y L : R<GOAL>C (W.addPolynomial x y L) - (Y - C (linePolynomial x y L)) * (W.negPolynomial - C (linePolynomial x y L)) = W.polynomial * 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>h0 : 0 < sSupNormIm f 0<VAR>h1 : 0 < sSupNormIm f 1<GOAL>interpStrip f z = ↑(sSupNormIm f 0) ^ (1 - z) * ↑(sSupNormIm f 1) ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a x : α<VAR>s : Set α<GOAL>s ⩿ insert x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>a x : α<VAR>s t : Set α<VAR>hst : s ≤ t<VAR>h2t : t ≤ insert x s<GOAL>t = s ∨ t = insert x s
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute a b<GOAL>a * ⅟b = ⅟b * (b * a * ⅟b)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute a b<GOAL>⅟b * (b * a * ⅟b) = ⅟b * (a * b * ⅟b)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute a b<GOAL>⅟b * (a * b * ⅟b) = ⅟b * a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid α<VAR>f : β → α<VAR>g : γ → α<VAR>h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b<GOAL>map (fun s => ∏ b ∈ s, f b) atTop ≤ map (fun s => ∏ x ∈ s, g x) atTop
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>δ : (E →L[ℝ] E) → ℝ≥0<VAR>hδ : ∀ (A : E →L[ℝ] E), 0 < δ A ∧ (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ ↑(δ A) → |B.det - A.det| ≤ ↑ε) ∧ ∀ (t : Set E) (g : E → E), ApproximatesLinearOn g A t (δ A) → μ (g '' t) ≤ (ENNReal.ofReal |A.det| + ↑ε) * μ t<VAR>t : ℕ → Set E<VAR>A : ℕ → E →L[ℝ] E<VAR>t_disj : Pairwise (Disjoint on t)<VAR>t_meas : ∀ (n : ℕ), MeasurableSet (t n)<VAR>t_cover : s ⊆ ⋃ n, t n<VAR>ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ + 2 * ↑ε * μ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp0 : ¬p.toReal = 0<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ p.toReal) atTop < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R<VAR>hp0 : ¬p.toReal = 0<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<GOAL>liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hp0 : ¬p.toReal = 0<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ ↑R<GOAL>liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : OpensMeasurableSpace E<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → E<VAR>hfmeas : ∀ (n : ℕ), Measurable (f n)<VAR>hp0 : ¬p.toReal = 0<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ ↑R<GOAL>sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), ↑‖f b a‖₊ ^ p.toReal ∂μ} ≤ ↑R ^ p.toReal
<VAR>u : XgcdType<VAR>hr : u.r = 0<GOAL>u.finish.v = u.v
<VAR>u : XgcdType<VAR>hr : u.r = 0<VAR>ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u<GOAL>u.finish.v = u.v
<VAR>u : XgcdType<VAR>hr : u.r = 0<VAR>ha : ↑u.b * u.q = ↑u.a<GOAL>u.finish.v = u.v
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>hs : s < a<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>hs : s < a<VAR>d : ℝ<VAR>hd' : IsBigOWith d atTop f fun x => x ^ (-a)<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>hs : s < a<VAR>d : ℝ<VAR>hd' : ∃ a_1, ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>hs : s < a<VAR>d e : ℝ<VAR>he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>a s : ℝ<VAR>hf : f =O[atTop] fun x => x ^ (-a)<VAR>hs : s < a<VAR>d e : ℝ<VAR>he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖<VAR>he' : 0 < max e 1<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioi c) volume