ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>ι' : Sort u_6<VAR>inst✝ : Mul M<VAR>t₁ t₂ : TopologicalSpace M<VAR>h₁ : ContinuousMul M<VAR>h₂ : ContinuousMul M<VAR>b : Bool<GOAL>ContinuousMul M
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((injectiveResolutions C).map f) ≫ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map J.iso.hom ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex = ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex) ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫ (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ) ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app J.cocomplex = (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>I : InjectiveResolution X<VAR>J : InjectiveResolution Y<VAR>φ : I.cocomplex ⟶ J.cocomplex<VAR>comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫ (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ = (F.mapHomotopyCategory (ComplexShape.up ℕ)).map I.iso.hom ≫ (F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.app I.cocomplex ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ)
<GOAL>sin (π / 2) = 1 ∨ sin (π / 2) = -1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f f' : StructuredArrow S T<VAR>g : f.right ≅ f'.right<VAR>w : autoParam (f.hom ≫ T.map g.hom = f'.hom) _auto✝<GOAL>(Functor.fromPUnit S).map (eqToIso ⋯).hom ≫ f'.hom = f.hom ≫ T.map g.hom
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>k : (x + y).RightMoves<VAR>P : (x + y).RightMoves → Prop<VAR>hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))<VAR>hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))<GOAL>P k
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>k : (x + y).RightMoves<VAR>P : (x + y).RightMoves → Prop<VAR>hl : ∀ (j : x.RightMoves), P (toRightMovesAdd (Sum.inl j))<VAR>hr : ∀ (j : y.RightMoves), P (toRightMovesAdd (Sum.inr j))<GOAL>P (toRightMovesAdd (toRightMovesAdd.symm k))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g✝ φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f'✝ : ℝ → E<VAR>f f' g : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>a✝ : α<GOAL>a✝ ∈ (σ * τ * σ⁻¹).support ↔ a✝ ∈ map (Equiv.toEmbedding σ) τ.support
<VAR>m✝ m : ℕ<VAR>a : Fin m → ℕ<VAR>i j : Fin m<VAR>hij : i ≠ j<VAR>ltij : i < j<GOAL>((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)
<VAR>m✝ m : ℕ<VAR>a : Fin m → ℕ<VAR>i j : Fin m<VAR>hij : i ≠ j<VAR>ltij : i < j<VAR>hja : ↑j < Nat.supOfSeq a<GOAL>((↑i + 1) * (Nat.supOfSeq a)! + 1).Coprime ((↑j + 1) * (Nat.supOfSeq a)! + 1)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace ℝ E<VAR>ι : Type u_2<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>ne : Nonempty ι<VAR>e f : OrthonormalBasis ι ℝ E<VAR>x : Orientation ℝ E ι<VAR>v : ι → E<GOAL>|(e.adjustToOrientation x).toBasis.det v| = |e.toBasis.det v|
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>∫⁻ (ω : Ω), ↑(f₁ ω) + ↑(f₂ ω) ∂↑μ = ∫⁻ (ω : Ω), ↑(f₁ ω) ∂↑μ + ∫⁻ (ω : Ω), ↑(f₂ ω) ∂↑μ
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M : Matrix m n R<VAR>N : Matrix n o R<VAR>i : m<GOAL>(M * N).toMvPolynomial i = (bind₁ N.toMvPolynomial) (M.toMvPolynomial i)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>hα : IsIntegral F α<GOAL>F⟮α⟯.toSubalgebra = Algebra.adjoin F {α}
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>hα : IsIntegral F α<GOAL>∀ x ∈ {α}, IsAlgebraic F x
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>x : E<VAR>hα : IsIntegral F x<GOAL>IsAlgebraic F x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p I : Ideal A<VAR>hI : I ≠ ⊥<GOAL>p ∈ normalizedFactors I ↔ p.IsPrime ∧ p ∣ I
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>z : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hz : z ∈ s<VAR>m : Fin 2 → E<GOAL>(iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>z : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hz : z ∈ s<VAR>m : Fin 2 → E<GOAL>(((iteratedFDerivWithin 𝕜 0 (fun y => fderivWithin 𝕜 (fun y => fderivWithin 𝕜 f s y) s y) s z) (init (init m))) (init m (last 0))) (m (last 1)) = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsPrincipalIdealRing A<VAR>inst✝ : NoZeroSMulDivisors A L<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsPrincipalIdealRing A<VAR>inst✝ : NoZeroSMulDivisors A L<VAR>this : Module.Free A C<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsPrincipalIdealRing A<VAR>inst✝ : NoZeroSMulDivisors A L<VAR>this✝ : Module.Free A C<VAR>this : IsNoetherian A C<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsPrincipalIdealRing A<VAR>inst✝ : NoZeroSMulDivisors A L<VAR>this✝¹ : Module.Free A C<VAR>this✝ : IsNoetherian A C<VAR>this : IsLocalization (algebraMapSubmonoid C A⁰) L<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝¹⁸ : CommRing R<VAR>inst✝¹⁷ : CommRing A<VAR>inst✝¹⁶ : Field K<VAR>inst✝¹⁵ : IsDomain A<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹² : Field L<VAR>C : Type u_5<VAR>inst✝¹¹ : CommRing C<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra A L<VAR>inst✝⁸ : IsScalarTower A K L<VAR>inst✝⁷ : Algebra C L<VAR>inst✝⁶ : IsIntegralClosure C A L<VAR>inst✝⁵ : Algebra A C<VAR>inst✝⁴ : IsScalarTower A C L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsPrincipalIdealRing A<VAR>inst✝ : NoZeroSMulDivisors A L<VAR>this✝¹ : Module.Free A C<VAR>this✝ : IsNoetherian A C<VAR>this : IsLocalization (algebraMapSubmonoid C A⁰) L<VAR>b : Basis (Module.Free.ChooseBasisIndex A C) K L := Basis.localizationLocalization K A⁰ L (Module.Free.chooseBasis A C)<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>h : a ∣ b<GOAL>a ^ 0 ∣ b ^ 0
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>h : a ∣ b<VAR>n : ℕ<GOAL>a ^ (n + 1) ∣ b ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>h : a ∣ b<VAR>n : ℕ<GOAL>a ^ n * a ∣ b ^ n * b
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : ν ≪ μ<GOAL>(fun x => rexp (llr μ ν x)) =ᶠ[ae ν] fun x => (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : ν ≪ μ<VAR>x : α<VAR>hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal<VAR>hx_pos : 0 < μ.rnDeriv ν x<GOAL>rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsCartesian f φ<GOAL>IsCartesian.map p f φ φ = 𝟙 a
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsCartesian (p.map φ) φ<GOAL>IsCartesian.map p (p.map φ) φ φ = 𝟙 a✝
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsCartesian (p.map φ) φ<GOAL>𝟙 a✝ = IsCartesian.map p (p.map φ) φ φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₁} 𝒮<VAR>inst✝¹ : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsCartesian (p.map φ) φ<GOAL>𝟙 a✝ ≫ φ = φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Finset β<GOAL>HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<VAR>r : ℝ<VAR>hr : 0 < r<VAR>w : α<VAR>hw : r⁻¹ < ‖w‖<GOAL>0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : Fin 3 → P<GOAL>AffineIndependent k p ↔ ¬Collinear k (Set.range p)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hq0 : 0 ≤ q<VAR>hq1 : q ≤ 1<VAR>a : α<GOAL>↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>inst✝ : Fintype I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>he' : ∏ i : I, (1 - e i) = 0<GOAL>∑ i : I, e i = 1
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝³ : Traversable t<VAR>inst✝² : LawfulTraversable t<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m α<VAR>x : α<VAR>xs : t β<GOAL>foldlm f x xs = unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝³ : Traversable t<VAR>inst✝² : LawfulTraversable t<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m α<VAR>x : α<VAR>xs : t β<GOAL>unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x = List.foldlM f x (toList xs)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<GOAL>padicValRat p q = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<GOAL>padicValRat p q = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>padicValRat p q = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯) = ↑((multiplicity (↑p) n).get ⋯) - ↑((multiplicity (↑p) d).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯) = ↑((multiplicity (↑p) (c * q.num)).get ⋯) - ↑((multiplicity (↑p) (c * ↑q.den)).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯) = ↑((multiplicity (↑p) c).get ⋯ + (multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity (↑p) c).get ⋯ + (multiplicity ↑p ↑q.den).get ⋯)
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯) = ↑((multiplicity (↑p) c).get ⋯) + ↑((multiplicity (↑p) q.num).get ⋯) - (↑((multiplicity (↑p) c).get ⋯) + ↑((multiplicity ↑p ↑q.den).get ⋯))
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>n d : ℤ<VAR>hqz : q ≠ 0<VAR>qdf : q = n /. d<VAR>hd : d ≠ 0<VAR>c : ℤ<VAR>hc1 : n = c * q.num<VAR>hc2 : d = c * ↑q.den<GOAL>↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity p q.den).get ⋯) = ↑((multiplicity (↑p) c).get ⋯) + ↑((multiplicity (↑p) q.num).get ⋯) - (↑((multiplicity (↑p) c).get ⋯) + ↑((multiplicity p q.den).get ⋯))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Set α<VAR>s : Finset ↑t<VAR>a : α<VAR>ha : a ∈ ↑(map (Embedding.subtype fun x => x ∈ t) s)<GOAL>a ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : Set α<VAR>s : Finset ↑t<VAR>a : α<VAR>ha : a ∈ map (Embedding.subtype fun x => x ∈ t) s<GOAL>a ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>a : α<VAR>h : a ∈ s<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct<VAR>s' : WSeq α<VAR>sd : some (a, s') ∈ (s.drop n).destruct<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>a : α<VAR>h✝ : a ∈ s<VAR>n : ℕ<VAR>h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (s.drop n).destruct<VAR>s' : WSeq α<VAR>sd : some (a, s') ∈ (s.drop n).destruct<VAR>b : β<VAR>t' : WSeq β<VAR>td : some (b, t') ∈ (t.drop n).destruct<VAR>ab : R a b<VAR>right✝ : LiftRel R s' t'<GOAL>∃ b, b ∈ t ∧ R a b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>g : PolynomialModule R M<VAR>n : ℕ<GOAL>((monomial i) r • g) n = if i ≤ n then r • g (n - i) else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>n : ℕ<GOAL>((monomial i) r • 0) n = if i ≤ n then r • 0 (n - i) else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>n : ℕ<VAR>p q : PolynomialModule R M<VAR>hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0<VAR>hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0<GOAL>((monomial i) r • (p + q)) n = if i ≤ n then r • (p + q) (n - i) else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>I : Ideal R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra S R<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower S R M<VAR>i : ℕ<VAR>r : R<VAR>n a✝ : ℕ<VAR>b✝ : M<GOAL>((monomial i) r • (single R a✝) b✝) n = if i ≤ n then r • ((single R a✝) b✝) (n - i) else 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_meas : NullMeasurableSet s μ<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<GOAL>∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : Group H<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MulAction H β<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : Countable G<VAR>h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s<VAR>h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ<VAR>h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)<VAR>aedisjoint : Pairwise (AEDisjoint μ on fun g => g • s)<VAR>h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ<GOAL>∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s