ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Finite α<VAR>S : Set G<VAR>hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap<VAR>hS2 : closure S = ⊤<VAR>h : IsPretransitive G α<VAR>this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S))) α<GOAL>closure (⇑(toPermHom G α) '' S) = ⊤
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>x : ↥p<VAR>hx : x ∈ ↑(eigenspace (LinearMap.restrict f hfp) μ)<GOAL>p.subtype x ∈ f.eigenspace μ
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>p : Submodule R M<VAR>hfp : ∀ x ∈ p, f x ∈ p<VAR>μ : R<VAR>x : ↥p<VAR>hx : ⟨f ↑x, ⋯⟩ = μ • x<GOAL>f (p.subtype x) = μ • p.subtype x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<GOAL>W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q - W'.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2 - Q x * P z ^ 2 * addZ P Q ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>inst✝ : I.Boundaryless<VAR>x : M<VAR>hx : x ∈ f.source<VAR>s : Set M<VAR>h : s ∈ 𝓝 x<GOAL>↑(f.extend I) '' s ∈ 𝓝 (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>inst✝² : TopologicalSpace H'<VAR>inst✝¹ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>inst✝ : I.Boundaryless<VAR>x : M<VAR>hx : x ∈ f.source<VAR>s : Set M<VAR>h : s ∈ 𝓝 x<GOAL>↑(f.extend I) ⁻¹' (↑(f.extend I) '' s) ∈ 𝓝 x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R (m + n)) (φ * (monomial R n) a) = (coeff R m) φ * a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>n ≤ m + n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬p = 0<GOAL>f p.leadingCoeff ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬p = 0<GOAL>f p.leadingCoeff ≠ f 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ ^ 2 = re ⟪x, ((adjoint A).comp A) x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<VAR>h : ⟪x, ((adjoint A).comp A) x⟫_𝕜 = ⟪A x, A x⟫_𝕜<GOAL>‖A x‖ ^ 2 = re ⟪x, ((adjoint A).comp A) x⟫_𝕜
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<GOAL>P.isoClosure.map F = P.map F
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<GOAL>P.isoClosure.map F ≤ P.map F
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<VAR>F : C ⥤ D<GOAL>P.map F ≤ P.isoClosure.map F
<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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<GOAL>g =o[𝓝[insert x s] x] g' ↔ g =o[𝓝[s] x] g'
<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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[insert x s] x) g g') ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝[s] x) g g'
<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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'
<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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>‖g x‖ ≤ c * ‖g' 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>inst✝ : TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>g : α → E'<VAR>g' : α → F'<VAR>h : g x = 0<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>0 ≤ c * ‖g' x‖
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>hJ : J ≤ I<GOAL>∃ y, HasIntegral J l f vol y ∧ Tendsto (integralSum f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y✝ y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>hJ : J ≤ I<VAR>y : F<VAR>hy : Tendsto (integralSum f vol) (l.toFilteriUnion I (Prepartition.single I J hJ)) (𝓝 y)<GOAL>HasIntegral J l f vol y
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>ι' : Type u_7<VAR>inst✝¹ : Countable ι'<VAR>m : Measure α<VAR>m' : ι' → Measure β<VAR>inst✝ : ∀ (n : ι'), SFinite (m' n)<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(m.prod (sum m')) s = (sum fun p => m.prod (m' p)) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>ι' : Type u_7<VAR>inst✝¹ : Countable ι'<VAR>m : Measure α<VAR>m' : ι' → Measure β<VAR>inst✝ : ∀ (n : ι'), SFinite (m' n)<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α), (sum m') (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>ι' : Type u_7<VAR>inst✝¹ : Countable ι'<VAR>m : Measure α<VAR>m' : ι' → Measure β<VAR>inst✝ : ∀ (n : ι'), SFinite (m' n)<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)<GOAL>∫⁻ (x : α), (sum m') (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>ι' : Type u_7<VAR>inst✝¹ : Countable ι'<VAR>m : Measure α<VAR>m' : ι' → Measure β<VAR>inst✝ : ∀ (n : ι'), SFinite (m' n)<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<VAR>M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)<GOAL>∫⁻ (x : α), ∑' (i : ι'), (m' i) (Prod.mk x ⁻¹' s) ∂m = ∑' (i : ι'), ∫⁻ (x : α), (m' i) (Prod.mk x ⁻¹' s) ∂m
<VAR>f : ℝ → ℝ<VAR>p : ℝ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : 0 < c₁<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x ^ p) u ∈ Set.Icc (c₁ * (fun x => f x ^ p) x) (c₂ * (fun x => f x ^ p) x)
<VAR>f : ℝ → ℝ<VAR>p : ℝ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : 0 < c₁<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>hc₁p : 0 < c₁ ^ p<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x ^ p) u ∈ Set.Icc (c₁ * (fun x => f x ^ p) x) (c₂ * (fun x => f x ^ p) x)
<VAR>f : ℝ → ℝ<VAR>p : ℝ<VAR>hf : GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : 0 < c₁<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>hc₁p : 0 < c₁ ^ p<VAR>hc₂p : 0 < c₂ ^ p<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x ^ p) u ∈ Set.Icc (c₁ * (fun x => f x ^ p) x) (c₂ * (fun x => f x ^ p) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<VAR>h : a / b = c<GOAL>a = b * c
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>d : n → R<GOAL>(∀ (i : n), 0 ≤ d i) → (diagonal d).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>d : n → R<VAR>hd : ∀ (i : n), 0 ≤ d i<GOAL>∀ (x : n → R), 0 ≤ star x ⬝ᵥ diagonal d *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>d : n → R<VAR>hd : ∀ (i : n), 0 ≤ d i<VAR>x : n → R<VAR>i : n<VAR>x✝ : i ∈ Finset.univ<GOAL>0 ≤ star x i * (diagonal d *ᵥ x) i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>x : MvPolynomial σ R<GOAL>x ∈ weightedHomogeneousSubmodule R w m ↔ x ∈ supported R R {d | (weight w) d = m}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>x : MvPolynomial σ R<GOAL>x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ x_1 ∈ ↑x.support, x_1 ∈ {d | (weight w) d = m}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>x : MvPolynomial σ R<GOAL>x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ (x_1 : σ →₀ ℕ), x x_1 ≠ 0 → x_1 ∈ {d | (weight w) d = m}
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>hm : μ.IsMetric<GOAL>inst✝¹ ≤ μ.caratheodory
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>μ : OuterMeasure X<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>hm : μ.IsMetric<GOAL>borel X ≤ μ.caratheodory
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>m n : ℕ<GOAL>m / n ≤ m
<VAR>a b c d m✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>m : ℕ<GOAL>m / 0 ≤ m
<VAR>a b c d m✝ n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>m n : ℕ<VAR>hn : n > 0<GOAL>m / n ≤ m
<VAR>n : ℕ<GOAL>ringChar (ZMod n) = n
<VAR>n : ℕ<GOAL>CharP (ZMod n) n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u_5<VAR>inst✝⁴ : LinearOrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : DenselyOrdered 𝕜<VAR>inst✝ : NoZeroSMulDivisors 𝕜 E<VAR>A B : Set E<VAR>x : E<VAR>hA : Convex 𝕜 A<GOAL>x ∈ extremePoints 𝕜 A ↔ x ∈ A \ (convexHull 𝕜) (A \ {x})
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<GOAL>IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<GOAL>(∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3<GOAL>∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3<GOAL>0 ∣ n → 0 % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3<GOAL>1 ∣ n → 1 % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3<VAR>p q : ℕ<VAR>hp : Nat.Prime p<VAR>hq : q ∣ n → q % 4 ≠ 3<VAR>hpq : p * q ∣ n<GOAL>p * q % 4 ≠ 3
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommRing α<VAR>a✝ b✝ c d a b : α<GOAL>|a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommRing α<VAR>a✝ b✝ c d a b : α<GOAL>(a - b) * (a - b) = a * a + b * b - (1 + 1) * a * b
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.homologyIsoSc' i j k hi hk).hom ≫ (K.sc' i j k).homologyι = K.homologyι j ≫ (K.opcyclesIsoSc' i j k hi hk).hom
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>r : R<GOAL>(expand R 1) (C r) = C r
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f✝ f g : R[X]<VAR>ihf : (expand R 1) f = f<VAR>ihg : (expand R 1) g = g<GOAL>(expand R 1) (f + g) = f + g
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p q : ℕ<VAR>f : R[X]<VAR>n : ℕ<VAR>r : R<VAR>x✝ : (expand R 1) (C r * X ^ n) = C r * X ^ n<GOAL>(expand R 1) (C r * X ^ (n + 1)) = C r * X ^ (n + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>ht : NullMeasurableSet t μ<VAR>hd : AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ s + μ t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : IsNormal f<VAR>a : Ordinal.{u_2}<GOAL>a.cof ≤ (f a).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : IsNormal f<GOAL>cof 0 ≤ (f 0).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : IsNormal f<VAR>b : Ordinal.{u_2}<GOAL>(succ b).cof ≤ (f (succ b)).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>f : Ordinal.{u_2} → Ordinal.{u_2}<VAR>hf : IsNormal f<VAR>a : Ordinal.{u_2}<VAR>ha : a.IsLimit<GOAL>a.cof ≤ (f a).cof
<VAR>α : Type u_1<VAR>s✝ t : Set α<VAR>s : Set (α × α)<GOAL>diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>R : Type u_3<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Finite K<VAR>inst✝³ : CommRing R<VAR>inst✝² : Finite ι<VAR>inst✝¹ : Algebra K R<VAR>inst✝ : Algebra.IsAlgebraic K R<VAR>ps : ι → MvPolynomial ι R<VAR>hinj : Injective fun v i => (MvPolynomial.eval v) (ps i)<GOAL>Surjective fun v i => (MvPolynomial.eval v) (ps i)
<VAR>n m : ℕ<GOAL>n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
<VAR>n : ℕ<GOAL>n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0
<VAR>n m : ℕ<VAR>hm : m ≠ 0<GOAL>n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
<VAR>n m : ℕ<VAR>hm : m ≠ 0<GOAL>n ∣ m → n ≤ m
<VAR>α✝ : Type u<VAR>u : Level<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n d : ℕ<VAR>inv✝ : Invertible ↑d<GOAL>↑(Int.negOfNat n) * ⅟↑d = -(↑n / ↑d)
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<VAR>hl₁ : l₁.Nodup<GOAL>l₁.diff (a :: l₂) = List.filter (fun x => decide (x ∉ a :: l₂)) l₁
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<VAR>hl₁ : l₁.Nodup<GOAL>List.filter (fun a_1 => decide (decide (a_1 ∉ l₂) = true ∧ decide (a_1 ≠ a) = true)) l₁ = List.filter (fun x => decide (x ∉ a :: l₂)) l₁
<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<GOAL>ContDiff 𝕜 ⊤ f ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f