ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>f : E →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(range f)<GOAL>(ker f).ClosedComplemented
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>f : E →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(range f)<VAR>f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯<GOAL>(ker f).ClosedComplemented
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>f : E →L[𝕜] F<VAR>inst✝ : FiniteDimensional 𝕜 ↥(range f)<VAR>f' : E →L[𝕜] ↥(range f) := f.codRestrict (range f) ⋯<VAR>g : ↥(range f) →L[𝕜] E<VAR>hg : f'.comp g = id 𝕜 ↥(range f)<GOAL>(ker f).ClosedComplemented
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>a : Args<GOAL>a.Numeric → P124 a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>a : Args<GOAL>∀ (x : Args), (∀ (y : Args), ArgsRel y x → y.Numeric → P124 y) → x.Numeric → P124 x
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>a✝ a : Args<VAR>ih : ∀ (y : Args), ArgsRel y a → y.Numeric → P124 y<VAR>ha : a.Numeric<GOAL>P124 a
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>a✝ a : Args<VAR>ha : a.Numeric<VAR>ih : ∀ (a' : Args), ArgsRel a' a → P124 a'<GOAL>P124 a
<VAR>M✝ : Type u_1<VAR>inst✝² : Monoid M✝<VAR>s✝ : Set M✝<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t✝ : Set A<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>s t : Set M<VAR>x : M<VAR>hx : x ∈ Closure (s ∪ t)<VAR>L : List M<VAR>HL1✝ : ∀ x ∈ L, x ∈ s ∪ t<VAR>HL2 : L.prod = x<VAR>hd : M<VAR>tl : List M<VAR>ih : (∀ x ∈ tl, x ∈ s ∪ t) → ∃ y ∈ Closure s, ∃ z ∈ Closure t, y * z = tl.prod<VAR>HL1 : ∀ x ∈ hd :: tl, x ∈ s ∪ t<VAR>y : M<VAR>hy : y ∈ Closure s<VAR>z : M<VAR>hz : z ∈ Closure t<VAR>hyzx : y * z = tl.prod<VAR>hs : hd ∈ s<GOAL>hd * y * z = (hd :: tl).prod
<VAR>M✝ : Type u_1<VAR>inst✝² : Monoid M✝<VAR>s✝ : Set M✝<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t✝ : Set A<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>s t : Set M<VAR>x : M<VAR>hx : x ∈ Closure (s ∪ t)<VAR>L : List M<VAR>HL1✝ : ∀ x ∈ L, x ∈ s ∪ t<VAR>HL2 : L.prod = x<VAR>hd : M<VAR>tl : List M<VAR>ih : (∀ x ∈ tl, x ∈ s ∪ t) → ∃ y ∈ Closure s, ∃ z ∈ Closure t, y * z = tl.prod<VAR>HL1 : ∀ x ∈ hd :: tl, x ∈ s ∪ t<VAR>y : M<VAR>hy : y ∈ Closure s<VAR>z : M<VAR>hz : z ∈ Closure t<VAR>hyzx : y * z = tl.prod<VAR>ht : hd ∈ t<GOAL>y * (z * hd) = (hd :: tl).prod
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype (Sym2 V)<VAR>this : DecidableEq V<GOAL>Fintype.card G.Dart = ∑ v : V, G.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype (Sym2 V)<VAR>this : DecidableEq V<GOAL>univ.card = ∑ x : V, (filter (fun d => d.toProd.1 = x) univ).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ : Finset β<VAR>f✝ f g : β → α<VAR>hfg : ∀ a ∈ s₁, f a = g a<GOAL>s₁.gcd f = s₁.gcd g
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>normalizedFactors (n + 1) = ↑(n + 1).primeFactorsList
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>Multiset.Rel (fun x x_1 => x ~ᵤ x_1) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(normalizedFactors (n + 1)).prod ~ᵤ (↑(n + 1).primeFactorsList).prod
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s✝ t : Set α<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>inst✝ : Nonempty ι<VAR>s : Set α<GOAL>s ∈ iInf f ↔ ∃ i, s ∈ f i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<GOAL>Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ<VAR>s : Set X<VAR>hsc : s ∈ cocompact X<VAR>hs : IntegrableOn f s μ<VAR>hloc : LocallyIntegrable f μ<GOAL>Integrable f μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ<VAR>s : Set X<VAR>hsc : s ∈ cocompact X<VAR>hs : IntegrableOn f s μ<VAR>hloc : LocallyIntegrable f μ<VAR>t : Set X<VAR>htc : IsCompact t<VAR>ht : sᶜ ⊆ t<GOAL>Integrable f μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s✝ : Set X<VAR>x✝ : IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ<VAR>s : Set X<VAR>hsc : s ∈ cocompact X<VAR>hs : IntegrableOn f s μ<VAR>hloc : LocallyIntegrable f μ<VAR>t : Set X<VAR>htc : IsCompact t<VAR>ht : sᶜ ⊆ t<GOAL>IntegrableOn f sᶜ μ ∧ IntegrableOn f s μ
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<VAR>m : R<VAR>x✝ : m ∈ S<VAR>n : R<VAR>hn : n ∈ ⊥<GOAL>m * n ∈ ⊥
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S : AddSubmonoid R<VAR>m : R<VAR>x✝ : m ∈ S<VAR>n : R<VAR>hn : n = 0<GOAL>m * n = 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<VAR>x : ℝ<GOAL>0 < ↑x ↔ 0 < x
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hy : SameRay R y z<VAR>hx : SameRay R 0 z<GOAL>SameRay R (0 + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<VAR>hx₀ : x ≠ 0<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hx₀ : x ≠ 0<VAR>hy : SameRay R 0 z<GOAL>SameRay R (x + 0) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<VAR>hx : SameRay R x 0<VAR>hy : SameRay R y 0<GOAL>SameRay R (x + y) 0
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<VAR>hz₀ : z ≠ 0<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<VAR>hz₀ : z ≠ 0<VAR>rx rz₁ : R<VAR>hrx : 0 < rx<VAR>hrz₁ : 0 < rz₁<VAR>Hx : rx • x = rz₁ • z<GOAL>SameRay R (x + y) z
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>hx : SameRay R x z<VAR>hy : SameRay R y z<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<VAR>hz₀ : z ≠ 0<VAR>rx rz₁ : R<VAR>hrx : 0 < rx<VAR>hrz₁ : 0 < rz₁<VAR>Hx : rx • x = rz₁ • z<VAR>ry rz₂ : R<VAR>hry : 0 < ry<VAR>hrz₂ : 0 < rz₂<VAR>Hy : ry • y = rz₂ • z<GOAL>SameRay R (x + y) z
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>hz : z ≠ 0<GOAL>(1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n + 2) = (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>hz : z ≠ 0<GOAL>z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / ↑(2 * n + 2) ^ 2
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>hz : z ≠ 0<GOAL>2 * ↑n + 1 = ↑(2 * n + 2) - 1
<VAR>z : ℂ<VAR>n✝ n : ℕ<VAR>hz : z ≠ 0<GOAL>2 * ↑n + 2 = ↑(2 * n + 2)
<VAR>n : ℕ<VAR>hn : Squarefree n<GOAL>IsSquare (-1) ↔ ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
<VAR>n : ℕ<VAR>hn : Squarefree n<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3<GOAL>IsSquare (-1)
<VAR>hn : Squarefree 0<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 0 → q % 4 ≠ 3<GOAL>IsSquare (-1)
<VAR>hn : Squarefree 1<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3<GOAL>IsSquare (-1)
<VAR>p n : ℕ<VAR>hpp : Nat.Prime p<VAR>ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)<VAR>hn : Squarefree (p * n)<VAR>H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3<GOAL>IsSquare (-1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>∑ i ∈ Ioo k n, (↑i ^ 2)⁻¹ ≤ ∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>Ioo k n ⊆ Ioc k (max (k + 1) n)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>∀ i ∈ Ioc k (max (k + 1) n), i ∉ Ioo k n → 0 ≤ (↑i ^ 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>∑ i ∈ Ioc k (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>(↑k.succ ^ 2)⁻¹ + ∑ k ∈ Ico (k.succ + 1) (max (k + 1) n).succ, (↑k ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>k.succ < (max (k + 1) n).succ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹ ≤ ((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>k.succ ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>(↑k.succ)⁻¹ - (↑(max k.succ n))⁻¹ ≤ (↑k + 1)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<GOAL>((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<VAR>A : 1 ≤ ↑k + 1<GOAL>((↑k + 1) ^ 2)⁻¹ + (↑k + 1)⁻¹ ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<VAR>A : 1 ≤ ↑k + 1<GOAL>1 / (↑k + 1) ^ 2 + 1 / (↑k + 1) ≤ 1 / (↑k + 1) + 1 / (↑k + 1)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>k n : ℕ<VAR>A : 1 ≤ ↑k + 1<GOAL>↑k + 1 ≤ (↑k + 1) ^ 2
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x✝¹ : ℝ<VAR>x✝ : 𝕜<GOAL>{ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun (x✝¹ • x✝) = (RingHom.id ℝ) x✝¹ • { toFun := __spread✝⁻⁰.toFun, map_add' := ⋯ }.toFun x✝
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x✝¹ : ℝ<VAR>x✝ : 𝕜<GOAL>↑x✝¹ * ↑(RCLike.im x✝) * I = ↑x✝¹ * (↑(RCLike.im x✝) * I)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x✝ : 𝕜<GOAL>‖{ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread✝⁻⁰.invFun, left_inv := ⋯, right_inv := ⋯ } x✝‖ = ‖x✝‖
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>𝕜 : Type u_2<VAR>inst✝ : RCLike 𝕜<VAR>h : RCLike.im RCLike.I = 1<VAR>x✝ : 𝕜<GOAL>normSq ({ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread✝⁻⁰.invFun, left_inv := ⋯, right_inv := ⋯ } x✝) = RCLike.re x✝ * RCLike.re x✝ + RCLike.im x✝ * RCLike.im x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>(f ^ Int.negSucc n) a = a ↔ ↑s.card ∣ Int.negSucc n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>(f⁻¹ ^ (n + 1)) a = a ↔ ↑s.card ∣ Int.negSucc n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<GOAL>memberSubfamily a (image (fun x => x.erase a) 𝒜) = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>L S : TopologicalSpace α<VAR>inst✝¹ : IsLawson α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsClosed s ↔ IsClosed s
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : ¬r b a<VAR>h₂ : r b c<GOAL>r a c
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : ¬r b a<VAR>h₂ : r b c<VAR>h₃ : r a b<GOAL>r a c
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a c : α<VAR>h₁ : ¬r a a<VAR>h₂ : r a c<GOAL>r a c
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsTrans α r<VAR>inst✝ : IsTrichotomous α r<VAR>a b c : α<VAR>h₁ : ¬r b a<VAR>h₂ : r b c<VAR>h₃ : r b a<GOAL>r a c
<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>h : HasIntegral I l f vol y<VAR>h' : HasIntegral I l g vol y'<GOAL>HasIntegral I l (f - g) vol (y - y')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>f : α → β → γ<VAR>x : Vector α n<VAR>y : Vector β n<VAR>m✝ : Fin (n - 1)<GOAL>(zipWith f x y).tail.get m✝ = (zipWith f x.tail y.tail).get m✝
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(-o).rightAngleRotation x = -o.rightAngleRotation x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>∀ (v : E), ⟪(-o).rightAngleRotation x, v⟫_ℝ = ⟪-o.rightAngleRotation x, v⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪(-o).rightAngleRotation x, y⟫_ℝ = ⟪-o.rightAngleRotation x, y⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>((-o).areaForm x) y = ⟪-o.rightAngleRotation x, y⟫_ℝ
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>h : ¬ringChar R = 2<GOAL>orderOf (-1) = 2
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>h : ¬ringChar R = 2<GOAL>(-1) ^ 2 = 1
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>h : ¬ringChar R = 2<GOAL>-1 ≠ 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.index = 2 ↔ ∃ a, ∀ (b : G), Xor' (b * a ∈ H) (b ∈ H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>(∃ x ∉ H, ∀ x_1 ∉ H, x_1⁻¹ * x ∈ H) ↔ ∃ a, ∀ (b : G), b * a ∈ H ↔ b ∉ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>a : G<VAR>ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H<VAR>b : G<VAR>hba : b * a ∈ H<VAR>hb : b ∈ H<GOAL>False
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>a : G<VAR>ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H<VAR>b : G<VAR>hb : b ∉ H<GOAL>b * a ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>a : G<VAR>ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H<GOAL>a ∉ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>a : G<VAR>ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H<VAR>b : G<VAR>hb : b ∉ H<GOAL>b⁻¹ * a ∈ H
<VAR>x y : ℝ<VAR>f : Cauchy abs<GOAL>{ cauchy := f⁻¹ } = Real.inv' { cauchy := f }
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H✝<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<GOAL>zeroRootSubalgebra R L H = H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H✝<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<GOAL>zeroRootSubalgebra R L H ≤ H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H✝<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<GOAL>rootSpace H 0 ≤ H.toLieSubmodule
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H✝<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<VAR>k : ℕ<VAR>hk : rootSpace H 0 ≤ LieSubmodule.ucs k ⊥<GOAL>rootSpace H 0 ≤ H.toLieSubmodule
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>setToSimpleFunc T' f = c • setToSimpleFunc T f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∑ x ∈ filter (fun x => x ≠ 0) f.range, (T' (↑f ⁻¹' {x})) x = c • ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (↑f ⁻¹' {x})) x