ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<VAR>N k : ℕ<VAR>hku : ∀ l ≤ N, u l ≤ u k<GOAL>∃ n ≥ N, ∀ k < n, u k < u n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<VAR>N k : ℕ<VAR>hku : ∀ l ≤ N, u l ≤ u k<VAR>ex : ∃ n ≥ N, u k < u n<GOAL>∃ n ≥ N, ∀ k < n, u k < u n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<VAR>N k : ℕ<VAR>hku : ∀ l ≤ N, u l ≤ u k<VAR>ex : ∃ n ≥ N, u k < u n<VAR>n : ℕ<VAR>hnN : n ≥ N<VAR>hnk : u k < u n<VAR>hn_min : ∀ m < n, N ≤ m → u m ≤ u k<GOAL>∃ n ≥ N, ∀ k < n, u k < u n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : NoMaxOrder β<VAR>u : ℕ → β<VAR>hu : Tendsto u atTop atTop<VAR>N k : ℕ<VAR>hku : ∀ l ≤ N, u l ≤ u k<VAR>ex : ∃ n ≥ N, u k < u n<VAR>n : ℕ<VAR>hnN : n ≥ N<VAR>hnk : u k < u n<VAR>hn_min : ∀ m < n, N ≤ m → u m ≤ u k<GOAL>∀ k < n, u k < u n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : NoMaxOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>frontier (Icc a b) = {a, b}
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<GOAL>LowerSemicontinuousOn f univ ↔ LowerSemicontinuous f
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>hs : abscissaOfAbsConv f < ↑s.re<GOAL>∃ x < s.re, LSeriesSummable f ↑x
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>hs : abscissaOfAbsConv f < ↑s.re<VAR>x : ℝ<VAR>hx₁ : abscissaOfAbsConv f < ↑x<VAR>hx₂ : ↑x < ↑s.re<GOAL>∃ x < s.re, LSeriesSummable f ↑x
<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>s : Set P<VAR>p₀ : P<VAR>h : p₀ ∈ s<GOAL>Collinear k s ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<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>s : Set P<VAR>p₀ : P<VAR>h : p₀ ∈ s<GOAL>(∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v) ↔ ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<GOAL>(s.embDomain f) (f a) = s a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<VAR>b : β<GOAL>s (Classical.choose ⋯) = s a
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n < x + ε
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>(∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n < x + ε
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>hq : q.natDegree ≠ 0<GOAL>Function.Surjective ⇑(restrictComp p q hq)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>hq : q.natDegree ≠ 0<VAR>this : Fact (Splits (algebraMap F (p.comp q).SplittingField) p)<GOAL>Function.Surjective ⇑(restrictComp p q hq)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>hq : q.natDegree ≠ 0<VAR>this : Fact (Splits (algebraMap F (p.comp q).SplittingField) p)<GOAL>Function.Surjective ⇑(let h := ⋯; restrict p (p.comp q).SplittingField)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F✝ : ι → α → β<VAR>f✝ : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p✝ : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)
<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>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)<VAR>x : E<VAR>xs : x ∈ s<VAR>u : Set E<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : ContDiffOn 𝕜 n f (s ∩ u)<GOAL>ContDiffWithinAt 𝕜 n f s x
<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>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)<VAR>x : E<VAR>xs : x ∈ s<VAR>u : Set E<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>hu : ContDiffOn 𝕜 n f (s ∩ u)<GOAL>u ∈ 𝓝 x
<VAR>x y : ℂ<GOAL>cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
<VAR>x y : ℂ<VAR>s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)<GOAL>cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
<VAR>x y : ℂ<VAR>s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)<GOAL>cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
<VAR>x y : ℂ<VAR>s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)<GOAL>cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
<VAR>x y : ℂ<VAR>s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)<VAR>s2 : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)<GOAL>cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>g : γ → α<VAR>t₂ : TopologicalSpace β<VAR>t₁ : TopologicalSpace γ<GOAL>Continuous g ↔ Continuous (f ∘ g)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a p q : ℤ<VAR>hpq : p + n = q<VAR>p' q' : ℤ<VAR>hp' : p' = p + a<VAR>hq' : q' = q + a<GOAL>p' + n = q'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<GOAL>IsPositive 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>x : E<GOAL>0 ≤ reApplyInnerSelf 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>x : E<GOAL>0 ≤ re ⟪0 x, x⟫_𝕜
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>inst✝² : AddMonoidWithOne R<VAR>inst✝¹ : SetLike S R<VAR>s : S<VAR>inst✝ : AddSubmonoidWithOneClass S R<VAR>n : ℕ<GOAL>↑n ∈ s
<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>inst✝¹ : FiniteDimensional ℝ F<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : E → ι → ℝ<VAR>s : Set E<VAR>hf : LipschitzOnWith C f s<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s 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>inst✝¹ : FiniteDimensional ℝ F<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : E → ι → ℝ<VAR>s : Set E<VAR>hf : LipschitzOnWith C f s<VAR>A : ∀ (i : ι), LipschitzWith 1 fun x => x i<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s 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>inst✝¹ : FiniteDimensional ℝ F<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : E → ι → ℝ<VAR>s : Set E<VAR>hf : LipschitzOnWith C f s<VAR>A : ∀ (i : ι), LipschitzWith 1 fun x => x i<VAR>this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x => f x i) s x<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s 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>inst✝¹ : FiniteDimensional ℝ F<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>f : E → ι → ℝ<VAR>s : Set E<VAR>hf : LipschitzOnWith C f s<VAR>A : ∀ (i : ι), LipschitzWith 1 fun x => x i<VAR>this : ∀ (i : ι), ∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x => f x i) s x<VAR>x : E<VAR>hx : ∀ (i : ι), x ∈ s → DifferentiableWithinAt ℝ (fun x => f x i) s x<VAR>xs : x ∈ s<GOAL>DifferentiableWithinAt ℝ f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s✝ : Set α<VAR>f : ι → α<VAR>a : α<VAR>s : Set α<VAR>hs : BddAbove s<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>f : ι → α<VAR>a : α<VAR>hs : BddAbove ∅<GOAL>IsLUB ∅ (sSup ∅)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s✝ : Set α<VAR>f : ι → α<VAR>a : α<VAR>s : Set α<VAR>hs : BddAbove s<VAR>hne : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>head✝ : Sigma β<VAR>l : List (Sigma β)<GOAL>(head✝ :: l).kunion [] = head✝ :: l
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>v.IsEquiv v' ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>(∀ {x : K}, v x < 1 ↔ v' x < 1) ↔ ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g✝ : α → F β<VAR>h✝ : β → G γ<VAR>f : β → γ<VAR>x : t β<VAR>g : α → G β<VAR>h : β → γ<VAR>x✝ : t α<GOAL>traverse (map h ∘ g) x✝ = (map (map h) ∘ traverse g) x✝
<VAR>a b c d m k : ℕ<VAR>p q : ℕ → Prop<VAR>t : ℕ<VAR>hl : m * m < t * t<VAR>hr : t * t < (m + 1) * (m + 1)<GOAL>False
<VAR>a b c d m k : ℕ<VAR>p q : ℕ → Prop<VAR>t : ℕ<VAR>hl : m * m < t * t<VAR>hr : t * t < (m + 1) * (m + 1)<VAR>h1 : m < t<GOAL>False
<VAR>a b c d m k : ℕ<VAR>p q : ℕ → Prop<VAR>t : ℕ<VAR>hl : m * m < t * t<VAR>hr : t * t < (m + 1) * (m + 1)<VAR>h1 : m < t<VAR>h2 : t < m + 1<GOAL>False
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hf : ¬Integrable f μ<GOAL>∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hf : ¬Integrable f μ<VAR>h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ✝ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α → E<VAR>hf : ¬Integrable f μ<VAR>h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ<GOAL>f = (fun x => f x - ⨍ (a : α), f a ∂μ) + fun x => ⨍ (a : α), f a ∂μ
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>W.Ψ (2 * (↑m + 2) + 1) = W.Ψ (↑m + 4) * W.Ψ (↑m + 2) ^ 3 - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>(C (W.preΨ' (2 * (m + 2) + 1)) * if Even (2 * (m + 2) + 1) then W.ψ₂ else 1) = (C (W.preΨ' (m + 4)) * if Even (m + 4) then W.ψ₂ else 1) * (C (W.preΨ' (m + 2)) * if Even (m + 2) then W.ψ₂ else 1) ^ 3 - (C (W.preΨ' (m + 1)) * if Even (m + 1) then W.ψ₂ else 1) * (C (W.preΨ' (m + 3)) * if Even (m + 3) then W.ψ₂ else 1) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>C ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) * 1 = (C (W.preΨ' (m + 4)) * if Even m then W.ψ₂ else 1) * (C (W.preΨ' (m + 2)) * if Even m then W.ψ₂ else 1) ^ 3 - (C (W.preΨ' (m + 1)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<VAR>C : ℝ≥0<GOAL>‖f‖₊ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<VAR>C : ℝ≥0<GOAL>↑‖f‖₊ ≤ ↑C ↔ ∀ (m : (i : ι) → E i), ↑‖f m‖₊ ≤ ↑(C * ∏ i : ι, ‖m i‖₊)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.length<GOAL>l.attach.formPerm.cycleType = {l.length}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>l.attach.formPerm.cycleType = {l.length}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.attach.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>l.attach.formPerm.cycleType = {l.length}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.attach.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>↑(map (Finset.card ∘ support) [l.attach.formPerm]) = {l.length}
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.attach.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>[l.attach.formPerm].prod = l.attach.formPerm
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.attach.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>∀ σ ∈ [l.attach.formPerm], σ.IsCycle
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>hl : l.attach.Nodup<VAR>hn : 2 ≤ l.attach.length<GOAL>Pairwise Perm.Disjoint [l.attach.formPerm]
<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>a x : E<VAR>ha : ¬a = 0<GOAL>⟪a, x⟫_ℝ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) 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>a x : E<VAR>ha : ¬a = 0<GOAL>∀ (i : Fin 2), (⟪a, x⟫_ℝ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a) ((o.basisRightAngleRotation a ha) i) = (‖a‖ ^ 2 • (innerₛₗ ℝ) x) ((o.basisRightAngleRotation a ha) i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>ht : t ⊆ range f<GOAL>(f ⁻¹' t).encard = t.encard
<VAR>n m : ℕ<VAR>a : Fin (n + 1)<VAR>ha : a.succ ≠ last (n + 1)<GOAL>a < a.succ.castPred ha
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this : Encodable ↑s<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝² : Encodable ↑s<VAR>this✝¹ : TopologicalSpace ↑s := ⊥<VAR>this✝ : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>this : ∀ (UV : ↑s), ∃ f, EqOn (⇑f) 0 (↑UV).1 ∧ EqOn (⇑f) (fun x => ε UV) (↑UV).2ᶜ ∧ ∀ (x : X), f x ∈ Icc 0 (ε UV)<GOAL>∃ f, Inducing f
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : SecondCountableTopology X<VAR>B : Set (Set X)<VAR>hBc : B.Countable<VAR>hB : IsTopologicalBasis B<VAR>s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure UV.1 ⊆ UV.2}<VAR>this✝¹ : Encodable ↑s<VAR>this✝ : TopologicalSpace ↑s := ⊥<VAR>this : DiscreteTopology ↑s<VAR>hd : ∀ (UV : ↑s), Disjoint (closure (↑UV).1) (↑UV).2ᶜ<VAR>ε : ↑s → ℝ<VAR>ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1<VAR>hε : Tendsto ε cofinite (𝓝 0)<VAR>f : ↑s → C(X, ℝ)<VAR>hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1<VAR>hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x => ε UV) (↑UV).2ᶜ<VAR>hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)<GOAL>∃ f, Inducing f