ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.y S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.y S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ 2 ∣ S.a + ↑η * S.b<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>x : β<VAR>hx : x ≠ 0<GOAL>¬(const abv x).LimZero
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x y : α<VAR>S U Z : Set α<GOAL>IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S
<VAR>α : Type u_1<VAR>s✝ : Set ℕ<VAR>inst✝ : Infinite ↑s✝<VAR>s t : Set α<VAR>e : ℕ → α<VAR>he : ∀ (n : ℕ), e n ∈ s ∪ t<GOAL>∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T25Space X<VAR>x y : X<VAR>h : Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure)<VAR>hxy : x = y<GOAL>False
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>abscissaOfAbsConv f ≤ ↑s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>Real.toEReal '' {x | LSeriesSummable f ↑x} ∈ {x | ↑s.re ∈ x}
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : LSeriesSummable f s<GOAL>LSeriesSummable f ↑s.re
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>f : γ → (x : α) → β x<VAR>hf : ∀ (x : α), Continuous' fun g => f g x<VAR>c : Chain γ<VAR>a : α<GOAL>{ toFun := f, monotone' := ⋯ } (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P ≃ₗ[R] Q<VAR>f✝ : N ≃ₗ[R] P<VAR>m : M<VAR>n✝ : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<VAR>f : M ≃ₗ[R] M<VAR>n : ℕ<GOAL>rTensor N f ^ n = rTensor N (f ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a✝ b : α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>i : Fin (n + 1)<VAR>s : Sym α (n - ↑i)<VAR>hx : a ∉ s<GOAL>count a ↑(fill a i s) = ↑i
<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>ha : s ⊆ Ioi a<VAR>hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s<VAR>h : (⇑ofDual ⁻¹' s).Nonempty<GOAL>∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<GOAL>toLaurent (X ^ n) = T ↑n
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_not_mem : a ∉ s<GOAL>⋃ x ∈ s, Ici x = Ioi a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_not_mem : a ∉ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>Ici x ⊆ Ioi a
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f : ι → α<VAR>a_glb : IsGLB s a<VAR>a_not_mem : a ∉ s<VAR>x : α<VAR>hx : x ∈ Ioi a<GOAL>x ∈ ⋃ i ∈ s, Ici i
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>h'f : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasLineDerivWithinAt 𝕜 f₁ f' s x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>h'f : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝[(fun t => x + t • v) ⁻¹' s] 0] fun t => f (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>h'f : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<VAR>A : Continuous fun t => x + t • v<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝[(fun t => x + t • v) ⁻¹' s] 0] fun t => f (x + t • v)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>∑ s : Finset α, ↑((𝒜 ∪ ℬ).truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) + ∑ s : Finset α, ↑((𝒜 ⊻ ℬ).truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) = ∑ s : Finset α, ↑(𝒜.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) + ∑ s : Finset α, ↑(ℬ.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ✝ : Finset (Finset α)<VAR>s : Finset α<VAR>𝒜 ℬ : Finset (Finset α)<GOAL>∀ s ∈ univ, ↑((𝒜 ∪ ℬ).truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) + ↑((𝒜 ⊻ ℬ).truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) = ↑(𝒜.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card)) + ↑(ℬ.truncatedInf s).card / (↑s.card * ↑((card α).choose s.card))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>sinh ((dist a b + dist b c) / 2) = (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>dist ↑a ↑b * dist (↑b) ((starRingEnd ℂ) ↑c) / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c / (2 * √(a.im * b.im) * (2 * √(b.im * c.im))) = (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>(dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) / (2 * 2 * (√(a.im * b.im) * √(b.im * c.im))) = (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) / (2 * 2 * (√(a.im * c.im) * b.im))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>√(a.im * b.im) * √(b.im * c.im) = √(a.im * c.im) * b.im
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>(J l R).det * (J l R).det = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>(-1) ^ (Fintype.card l + Fintype.card l) = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>Even (Fintype.card l + Fintype.card l)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>‖-x‖ = ‖x‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>sInf (norm '' {m | ↑m = -x}) = sInf (norm '' {m | ↑m = x})
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<VAR>r : ℝ<GOAL>r ∈ norm '' {m | ↑m = -x} ↔ r ∈ norm '' {m | ↑m = x}
<VAR>a✝ b✝ m n p✝ a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>p : ℕ<GOAL>(a * b).factorization p = (a.factorization + b.factorization) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ : Filter α<VAR>inst✝ : SemilatticeSup β<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<GOAL>f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Ioc (a i) (b i)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Ioc (a i) (b i)<VAR>hφ : AECover μ l φ<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Ioc (a i) (b i)<VAR>hφ : AECover μ l φ<GOAL>(fun i => ∫ (x : ℝ) in φ i, f x ∂μ) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝³ : l.IsCountablyGenerated<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>φ : ι → Set ℝ := fun i => Ioc (a i) (b i)<VAR>hφ : AECover μ l φ<VAR>i : ι<VAR>hai : a i ≤ 0<VAR>hbi : 0 ≤ b i<GOAL>∫ (x : ℝ) in φ i, f x ∂μ = ∫ (x : ℝ) in a i..b i, f x ∂μ
<VAR>x✝ y x : ℝ<VAR>a✝ : ℕ<GOAL>log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑(eval₂ C X φ)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>∑ i ∈ Finset.range (φ.natDegree + 1), (PowerSeries.C R) (φ.coeff i) * PowerSeries.X ^ i = ∑ x ∈ Finset.range (φ.natDegree + 1), coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<GOAL>∀ x ∈ Finset.range (φ.natDegree + 1), (PowerSeries.C R) (φ.coeff x) * PowerSeries.X ^ x = coeToPowerSeries.ringHom (C (φ.coeff x) * X ^ x)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<VAR>x✝ : ℕ<VAR>a✝ : x✝ ∈ Finset.range (φ.natDegree + 1)<GOAL>(PowerSeries.C R) (φ.coeff x✝) * PowerSeries.X ^ x✝ = coeToPowerSeries.ringHom (C (φ.coeff x✝) * X ^ x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<GOAL>H.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<VAR>this : Nonempty α<GOAL>H.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<VAR>this✝ : Nonempty α<VAR>this : Nonempty β<GOAL>H.Connected
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<VAR>t₀ t₁ : ℝ<GOAL>range ⇑(γ.truncate t₀ t₁) ⊆ range ⇑γ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<VAR>t₀ t₁ : ℝ<GOAL>range ⇑(γ.truncate t₀ t₁) ⊆ range γ.extend
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<VAR>t₀ t₁ : ℝ<GOAL>∀ (x : ℝ) (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range γ.extend
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x✝ y<VAR>a b : X<VAR>γ : Path a b<VAR>t₀ t₁ x : ℝ<VAR>_hx : x ∈ I<GOAL>(γ.truncate t₀ t₁) ⟨x, _hx⟩ ∈ range γ.extend
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : A.IsSymm<VAR>k : ℤ<GOAL>(A ^ k).IsSymm
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hα : (𝓤 α).HasBasis p s<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hα : (𝓤 α).HasBasis p s<GOAL>(∀ (i : κ), p i → ∀ᶠ (x : X) in 𝓝 x₀, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝 x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<GOAL>TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<VAR>h_non : (Ico x y).Nonempty<GOAL>TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<VAR>h_non : (Ico x y).Nonempty<VAR>z : α<VAR>z_mem : z ∈ Ico x y<VAR>hz : ∀ x_1 ∈ Ico x y, ¬z < x_1<GOAL>TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<VAR>h_non : (Ico x y).Nonempty<VAR>z : α<VAR>z_mem : z ∈ Ico x y<VAR>hz : ∀ x_1 ∈ Ico x y, ¬z < x_1<VAR>z_card : (Ico x z).card < (Ico x y).card<GOAL>TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x < y<VAR>h_non : (Ico x y).Nonempty<VAR>z : α<VAR>z_mem : z ∈ Ico x y<VAR>hz : ∀ x_1 ∈ Ico x y, ¬z < x_1<VAR>z_card : (Ico x z).card < (Ico x y).card<VAR>hzy : z ⋖ y<GOAL>TransGen (fun x x_1 => x ⋖ x_1) x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (s.indicator fun x => c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ ⦃f g : α → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) f → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) g → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f + g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∀ ⦃f : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) (f n)) → (fun f => ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ) fun x => ⨆ n, f n 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>n : ℕ<GOAL>‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsDomain k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p<VAR>this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p<GOAL>(succNthDefiningPoly p n a₁ a₂ bs).degree = ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsDomain k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p<VAR>this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p<GOAL>(C (a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) + nthRemainder p n (fun v => bs v ^ p) (truncateFun (n + 1) a₁) - a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) - nthRemainder p n bs (truncateFun (n + 1) a₂))).degree < (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsDomain k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p<VAR>this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p<GOAL>0 < (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : CommRing k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsDomain k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>this✝ : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p<VAR>this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1)) - X * C (a₂.coeff 0 ^ p ^ (n + 1))).degree = ↑p<GOAL>0 < ↑p
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<GOAL>HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (log (1 + a⁻¹))
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<GOAL>log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<VAR>h₂ : 2 * a + 1 ≠ 0<GOAL>log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<VAR>h₂ : 2 * a + 1 ≠ 0<VAR>h₃ : a ≠ 0<GOAL>log (1 + a⁻¹) = log (1 + 1 / (2 * a + 1)) - log (1 - 1 / (2 * a + 1))
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<VAR>h₂ : 2 * a + 1 ≠ 0<VAR>h₃ : a ≠ 0<GOAL>log (1 + a⁻¹) = log ((1 + 1 / (2 * a + 1)) / (1 - 1 / (2 * a + 1)))
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<VAR>h₂ : 2 * a + 1 ≠ 0<VAR>h₃ : a ≠ 0<GOAL>1 + 1 / (2 * a + 1) ≠ 0
<VAR>a : ℝ<VAR>h : 0 < a<VAR>h₁ : |1 / (2 * a + 1)| < 1<VAR>h₂ : 2 * a + 1 ≠ 0<VAR>h₃ : a ≠ 0<GOAL>1 - 1 / (2 * a + 1) ≠ 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>f : P →ᵃⁱ[𝕜] P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>edist (f x) (f y) = edist x y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>update f i '' Ioc (f i) b = Ioc f (update f i b)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<VAR>this : ∀ (a : α), ∃ l, f a = ↑l<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<VAR>f' : α → List β<VAR>h' : ∀ (a : α), f a = ↑(f' a)<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<VAR>f' : α → List β<VAR>h' : ∀ (a : α), f a = ↑(f' a)<VAR>this : f = fun a => ↑(f' a)<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f g : α → Multiset β<VAR>f' : α → List β<VAR>h' : ∀ (a : α), f a = ↑(f' a)<VAR>this : f = fun a => ↑(f' a)<VAR>hd : Symmetric fun a b => (f' a).Disjoint (f' b)<GOAL>(s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Pairwise (fun a b => (f a).Disjoint (f b)) s