ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>E : Type u_4<VAR>inst✝³ : Fintype ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<VAR>e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ<GOAL>↑(finrank ℝ E) ≤ dimH (⇑e '' s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : dimH s < ↑d<GOAL>μH[↑d] s = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d<GOAL>μH[↑d] s = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d<VAR>d' : ℝ≥0<VAR>hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d'<VAR>hd'd : ↑d' < ↑d<GOAL>μH[↑d] s = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d<VAR>d' : ℝ≥0<VAR>hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d'<VAR>hd'd : d' < d<GOAL>μH[↑d] s = 0
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(baseChange W B).toAffine.negPolynomial = Polynomial.map (mapRingHom ↑f) (baseChange W A).toAffine.negPolynomial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a b x y : α<GOAL>IsChain r univ ↔ IsTrichotomous α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>h : IsChain r univ<VAR>a b : α<GOAL>r a b ∨ a = b ∨ r b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>h : IsChain r univ<VAR>a b : α<GOAL>¬a = b → r a b ∨ r b a
<VAR>ι : Type u_1<VAR>k : Type u_2<VAR>V : Type u_3<VAR>P : Type u_4<VAR>inst✝⁴ : Ring k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : Nontrivial k<VAR>s : Set P<VAR>p : P<VAR>hp : p ∈ s<VAR>w : ↑s → kˣ<VAR>this : s = Set.range Subtype.val<GOAL>affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>x : E<GOAL>IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ s<GOAL>(↑(fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ s<GOAL>(Multiset.card ↑(fill x m s)).choose (Multiset.count x ↑(fill x m s)) * (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ ↑s<GOAL>(Multiset.card ↑(fill x m s)).choose (Multiset.count x ↑(fill x m s)) * (Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial = n.choose ↑m * (↑s).multinomial
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ ↑s<GOAL>(Multiset.card ↑(fill x m s)).choose (Multiset.count x ↑(fill x m s)) = n.choose ↑m
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>m : Fin (n + 1)<VAR>s : Sym α (n - ↑m)<VAR>x : α<VAR>hx : x ∉ ↑s<GOAL>(Multiset.filter (fun x_1 => x ≠ x_1) ↑(fill x m s)).multinomial = (↑s).multinomial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(image Sym2.mk s.offDiag).card = s.card.choose 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>1 ≤ a / b ↔ a ≤ b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>hg : (g.comp f).FinitePresentation<VAR>hf : f.FiniteType<VAR>ins1 : Algebra A B := f.toAlgebra<VAR>ins2 : Algebra B C := g.toAlgebra<VAR>ins3 : Algebra A C := (g.comp f).toAlgebra<VAR>a : A<VAR>b : B<VAR>c : C<GOAL>(a • b) • c = a • b • c
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>hg : (g.comp f).FinitePresentation<VAR>hf : f.FiniteType<VAR>ins1 : Algebra A B := f.toAlgebra<VAR>ins2 : Algebra B C := g.toAlgebra<VAR>ins3 : Algebra A C := (g.comp f).toAlgebra<VAR>a : A<VAR>b : B<VAR>c : C<GOAL>(algebraMap B C) ((algebraMap A B) a) * ((algebraMap B C) b * c) = (algebraMap A C) a * ((algebraMap B C) b * c)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>x : L<GOAL>IsCompl (weightSpaceOf M 0 x) (posFittingCompOf R M x)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>(fun x => rexp (llr μ ν x)) =ᶠ[ae μ] fun x => (μ.rnDeriv ν x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ✝ ν✝ : Measure α<VAR>f : α → ℝ<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal<VAR>hx_pos : 0 < μ.rnDeriv ν x<GOAL>rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
<VAR>α : Type u_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>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioo a b)<GOAL>Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] b)
<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>l : Filter β<VAR>f✝ : α → β<VAR>f : β → ↑(Ioo a b)<GOAL>Tendsto (Subtype.val ∘ f) l (𝓝[<] b) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] b)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>a b : ℝ<VAR>hle : a ≤ b<VAR>f : X →ᵇ ℝ<VAR>hfs : EqOn (⇑f) 0 s<VAR>hft : EqOn (⇑f) 1 t<VAR>hf01 : ∀ (x : X), f x ∈ Icc 0 1<VAR>x : X<GOAL>a ≤ a + (b - a) * f x
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>a b : ℝ<VAR>hle : a ≤ b<VAR>f : X →ᵇ ℝ<VAR>hfs : EqOn (⇑f) 0 s<VAR>hft : EqOn (⇑f) 1 t<VAR>hf01 : ∀ (x : X), f x ∈ Icc 0 1<VAR>x : X<GOAL>a + (b - a) * f x ≤ b
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>s.GammaSeq n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : ∀ (x : ℝ), x = x / ↑n * ↑n<GOAL>s.GammaSeq n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : ∀ (x : ℝ), x = x / ↑n * ↑n<GOAL>s.GammaSeq n = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : ∀ (x : ℝ), x = x / ↑n * ↑n<GOAL>↑n ^ s * s.betaIntegral (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)) (x / ↑n) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)) x<GOAL>↑n ^ s * s.betaIntegral (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<GOAL>↑n ^ s * s.betaIntegral (↑n + 1) = ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<GOAL>∫ (x : ℝ) in 0 ..1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ∫ (x : ℝ) in 0 ..1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<GOAL>↑n ≠ 0
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<GOAL>∫ (x : ℝ) in Ioc 0 1, ↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) ∂volume = ∫ (x : ℝ) in Ioc 0 1, ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)) ∂volume
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<GOAL>↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑↑n * (↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<GOAL>↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<VAR>hn' : ↑n ≠ 0<GOAL>↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<VAR>hn' : ↑n ≠ 0<VAR>A : ↑n ^ s = ↑n ^ (s - 1) * ↑n<GOAL>↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<VAR>hn' : ↑n ≠ 0<VAR>A : ↑n ^ s = ↑n ^ (s - 1) * ↑n<VAR>B : (↑x * ↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑n ^ (s - 1)<GOAL>↑n ^ s * (↑x ^ (s - 1) * (1 - ↑x) ^ ↑n) = ↑n * ((1 - ↑x) ^ n * (↑x * ↑n) ^ (s - 1))
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n<VAR>this : ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) = ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)<VAR>x : ℝ<VAR>hx : x ∈ Ioc 0 1<VAR>hn' : ↑n ≠ 0<VAR>A : ↑n ^ s = ↑n ^ (s - 1) * ↑n<VAR>B : (↑x * ↑n) ^ (s - 1) = ↑x ^ (s - 1) * ↑n ^ (s - 1)<GOAL>↑n ^ (s - 1) * ↑n * (↑x ^ (s - 1) * (1 - ↑x) ^ n) = ↑n * ((1 - ↑x) ^ n * (↑x ^ (s - 1) * ↑n ^ (s - 1)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ioc a b ⊆ Icc a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.Ioc a b ⊆ Set.Icc a b
<VAR>α✝ : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ✝ ν : Measure α✝<VAR>inst✝⁴ : NormedAddCommGroup E✝<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hfp : Memℒp f p μ<GOAL>eLpNorm (↑(AEEqFun.mk f ⋯)) p μ < ⊤
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype p<VAR>inst✝ : Fintype q<GOAL>S l R = fromBlocks 1 0 0 (-1)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype p<VAR>inst✝ : Fintype q<GOAL>S l R = diagonal (Sum.elim (fun x => 1) fun i => -1)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>-Icc a b = Icc (-b) (-a)
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>Function.Surjective ⇑(lightToProfinite.map (S.proj n))
<VAR>S : LightProfinite<VAR>n : ℕ<GOAL>Function.Surjective ⇑((lightToProfinite.obj S).asLimitCone.π.app ((sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n)))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a✝ b : α<VAR>f : ι → α<VAR>a : α<GOAL>(⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<GOAL>x ∈ exposedPoints 𝕜 A ↔ IsExposed 𝕜 A {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<GOAL>IsExposed 𝕜 A {x} → x ∈ exposedPoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>h : IsExposed 𝕜 A {x}<GOAL>x ∈ exposedPoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>h : IsExposed 𝕜 A {x}<VAR>l : E →L[𝕜] 𝕜<VAR>hl : {x} = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<GOAL>x ∈ exposedPoints 𝕜 A
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>h : IsExposed 𝕜 A {x}<VAR>l : E →L[𝕜] 𝕜<VAR>hl : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ ∀ x_1 ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}, x_1 = x<GOAL>x ∈ exposedPoints 𝕜 A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<GOAL>Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<GOAL>(∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))) ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>r : Rˣ<GOAL>span R {↑r • x} = span R {x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>r : Rˣ<GOAL>span R {r • x} = span R {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)<VAR>s : Set X<VAR>hs : IsClosed s<VAR>h2s : s = ∅<GOAL>IsClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)<VAR>s : Set X<VAR>hs : IsClosed s<VAR>h2s : s.Nonempty<GOAL>IsClosed (f '' s)
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : V1 →ᵃ[k] V2<GOAL>⇑f.linear = ⇑f - fun x => f 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : V1 →ᵃ[k] V2<GOAL>⇑f.linear = (⇑f.linear + fun x => f 0) - fun x => (⇑f.linear + fun x => f 0) 0
<VAR>p q : ℚ≥0<GOAL>↑(p / q) = ↑(divNat (p.num * q.den) (p.den * q.num))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<GOAL>∃ f, a.IsFundamentalSequence a.cof.ord f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<GOAL>∃ o f, a.IsFundamentalSequence o f
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<GOAL>∃ o f, a.IsFundamentalSequence o f
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<GOAL>∃ o f, a.IsFundamentalSequence o f
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<VAR>this : IsWellOrder ι r<VAR>r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop := Subrel r {i | ∀ (j : ι), r j i → f j < f i}<VAR>hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}<GOAL>∃ o f, a.IsFundamentalSequence o f
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<VAR>this✝ : IsWellOrder ι r<VAR>r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop := Subrel r {i | ∀ (j : ι), r j i → f j < f i}<VAR>hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}<VAR>this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'<GOAL>∃ o f, a.IsFundamentalSequence o f
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<VAR>this✝ : IsWellOrder ι r<VAR>r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop := Subrel r {i | ∀ (j : ι), r j i → f j < f i}<VAR>hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}<VAR>this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'<GOAL>type r ≤ a.cof.ord
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<VAR>this✝ : IsWellOrder ι r<VAR>r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop := Subrel r {i | ∀ (j : ι), r j i → f j < f i}<VAR>hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}<VAR>this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'<VAR>i j : Ordinal.{u}<VAR>x✝¹ : i < type r'<VAR>h : j < type r'<VAR>x✝ : i < j<GOAL>r ↑(enum r' i x✝¹) ↑(enum r' j h)
<VAR>α : Type u_1<VAR>r✝ : α → α → Prop<VAR>a : Ordinal.{u}<VAR>ι : Type u<VAR>f : ι → Ordinal.{u}<VAR>hf : lsub f = a<VAR>hι : #ι = a.cof<VAR>r : ι → ι → Prop<VAR>wo : IsWellOrder ι r<VAR>hr : (#ι).ord = type r<VAR>this✝ : IsWellOrder ι r<VAR>r' : ↑{i | ∀ (j : ι), r j i → f j < f i} → ↑{i | ∀ (j : ι), r j i → f j < f i} → Prop := Subrel r {i | ∀ (j : ι), r j i → f j < f i}<VAR>hrr' : r' ↪r r := Subrel.relEmbedding r {i | ∀ (j : ι), r j i → f j < f i}<VAR>this : IsWellOrder (↑{i | ∀ (j : ι), r j i → f j < f i}) r'<GOAL>a ≤ (type r').blsub fun i x => f ↑(enum r' i x)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type w<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Linear R C<VAR>X Y Z : C<VAR>r : Rˣ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(r • f) ≫ g = r • f ≫ g
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k)) • P.f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.g (1 / x) = (P.ε⁻¹ * ↑(x ^ P.k) * (P.ε * ↑((1 / x) ^ P.k))) • P.g (1 / x)