ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<VAR>hz : z ≤ 0<GOAL>1 ≤ x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx1 : 0 < x<VAR>hx2 : x ≤ 1<VAR>hz : z ≤ 0<GOAL>1 = x ^ 0
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : Module R M✝<VAR>P : Type u_3<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : Module R P<VAR>f : M✝ →ₗ[R] P<VAR>ι : Type u_4<VAR>M : ι → Type u_5<VAR>inst✝² : Finite ι<VAR>inst✝¹ : (i : ι) → AddCommMonoid (M i)<VAR>inst✝ : (i : ι) → Module R (M i)<VAR>p : (i : ι) → Submodule R (M i)<VAR>hsb : ∀ (i : ι), (p i).FG<GOAL>(pi univ p).FG
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ : R[X]<VAR>n : ℕ<VAR>a : R<VAR>n✝ : ℕ<GOAL>(PowerSeries.coeff R n✝) ↑((monomial n) a) = (PowerSeries.coeff R n✝) ((PowerSeries.monomial R n) a)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<GOAL>(AffineSubspace.map f s).WOppSide (f x) (f y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<GOAL>SameRay R (f x -ᵥ f p₁) (f p₂ -ᵥ f y)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>h : SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)<GOAL>SameRay R (f.linear (x -ᵥ p₁)) (f.linear (p₂ -ᵥ y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a✝ b c d a : K<VAR>h : a ≠ 0<GOAL>a / -a = -1
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : InvolutiveStar R<VAR>inst✝¹ : StarRing A<VAR>inst✝ : StarModule R A<VAR>r : R<VAR>a : A<GOAL>star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)
<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>f : α → F<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>essSup (fun x => ↑‖f x‖₊) (c • μ) = essSup (fun x => ↑‖f x‖₊) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>r.preimage ∅ = ∅
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>M : Type u_3<VAR>inst✝ : AddMonoid M<GOAL>AddMonoid.IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>M : Type u_3<VAR>inst✝ : AddMonoid M<GOAL>(∀ (y : ℕ) (x : M), x ≠ 0 → y ≠ 0 → ¬y • x = 0) ↔ ∀ {c : ℕ} {x : M}, c • x = 0 → c = 0 ∨ x = 0
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Multiset α<GOAL>∀ (a : List α), card (powersetCard n ⟦a⟧) = (card ⟦a⟧).choose n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f✝ : α ≃o β<VAR>s✝ t : LowerSet α<VAR>a : α<VAR>b : β<VAR>f : α ≃o β<VAR>s : LowerSet β<GOAL>↑((map f).symm s) = ↑((map f.symm) s)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ ≠ x₂<GOAL>W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>(fderivWithin 𝕜 f s x) 1 = 0
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>0 1 = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : S.HasLeftHomology<VAR>inst✝ : F.PreservesLeftHomologyOf S<GOAL>(S.map F).leftHomologyπ ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (S.leftHomologyData.map F) = (S.map F).leftHomologyπ ≫ leftHomologyMap' (𝟙 (S.map F)) (S.map F).leftHomologyData (hl.map F) ≫ F.map (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<GOAL>∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>∃ s, map i f = C (i f.leadingCoeff) * ∏ a ∈ s, (X - C a)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>map i f = C (i f.leadingCoeff) * ∏ a ∈ s.toFinset, (X - C a)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>s.Nodup
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>(Multiset.map (fun a => X - C a) s).prod.Separable
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>(?h.hs.f * (Multiset.map (fun a => X - C a) s).prod).Separable
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>K[X]
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>i✝ i : F →+* K<VAR>f : F[X]<VAR>sep : f.Separable<VAR>sp : Splits i f<VAR>s : Multiset K<VAR>h : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<GOAL>(map i f).Separable
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hab : a < b<GOAL>∃ p, a.factorization p < b.factorization p
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hab : a < b<VAR>hb : b ≠ 0<GOAL>∃ p, a.factorization p < b.factorization p
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : ∀ (p : ℕ), b.factorization p ≤ a.factorization p<GOAL>b ≤ a
<VAR>a✝ b✝ m n p a b : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : b ∣ a<GOAL>b ≤ a
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>h : a ≠ 0 ∨ s ≠ 0<GOAL>Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s = completedHurwitzZetaEven a s / s.Gammaℝ
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>h✝ : a ≠ 0 ∨ s ≠ 0<VAR>h : s ≠ 0<GOAL>Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) s = completedHurwitzZetaEven a s / s.Gammaℝ
<VAR>a : UnitAddCircle<VAR>h : a ≠ 0 ∨ 0 ≠ 0<GOAL>Function.update (fun s => completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) 0 = completedHurwitzZetaEven a 0 / Gammaℝ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x✝ : M<GOAL>((ofDirectSum.comp toDirectSum).toLinearMap ∘ₗ ι R) x✝ = ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ ι R) x✝
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : μ.Regular<VAR>s : Set G<VAR>hs : IsOpen s<GOAL>μ s = 0 ↔ s = ∅ ∨ μ = 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>s : Set G<VAR>hs : IsOpen s<VAR>inst✝¹ : IsMulLeftInvariant 0<VAR>inst✝ : Regular 0<GOAL>0 s = 0 ↔ s = ∅ ∨ 0 = 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : μ.Regular<VAR>s : Set G<VAR>hs : IsOpen s<VAR>hμ : NeZero μ<GOAL>μ s = 0 ↔ s = ∅ ∨ μ = 0
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Ioi a, g' x ≤ 0<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>IntegrableOn g' (Ioi a) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Ioi a, g' x ≤ 0<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>Integrable (-g') (volume.restrict (Ioi a))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (cthickening ε s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : NormedOrderedGroup α<VAR>s : Set α<VAR>hs : IsUpperSet s<VAR>ε : ℝ<GOAL>IsUpperSet (⋂ ε_1, ⋂ (_ : max 0 ε < ε_1), thickening ε_1 s)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁸ : LinearOrderedRing 𝕜<VAR>inst✝⁷ : DenselyOrdered 𝕜<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : OrderTopology 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>[x-[𝕜]y] ⊆ closure (openSegment 𝕜 x y)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁸ : LinearOrderedRing 𝕜<VAR>inst✝⁷ : DenselyOrdered 𝕜<VAR>inst✝⁶ : TopologicalSpace 𝕜<VAR>inst✝⁵ : OrderTopology 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>x y : E<GOAL>(fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<GOAL>P y ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<VAR>hPx : P x ≠ 0<GOAL>P y ≠ 0
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<VAR>hPx : P x ≠ 0<VAR>hPy : P y = 0<GOAL>False
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>inst✝ : NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : 0 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * 0 ≠ 0 ∨ W'.a₁ * P x * 0 ≠ 0)<VAR>hPz : P z = 0<VAR>hPx : P x ≠ 0<VAR>hPy : P y = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>h : ¬IsSuccLimit a<GOAL>a ∈ range succ
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>h : ¬IsSuccLimit a<VAR>b : α<VAR>hb : ¬IsMax b ∧ succ b = a<GOAL>a ∈ range succ
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : 1 < n<GOAL>n < n * n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : 1 < n<VAR>this : n * 1 < n * n<GOAL>n < n * n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : R<VAR>n : ℕ<VAR>hx : (x - x ^ 2) ^ n = 0<VAR>P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n<GOAL>IsIdempotentElem (1 - (1 - x ^ n) ^ n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : R<VAR>n : ℕ<VAR>hx : (x - x ^ 2) ^ n = 0<VAR>P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n<VAR>this : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2<GOAL>IsIdempotentElem (1 - (1 - x ^ n) ^ n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : R<VAR>n : ℕ<VAR>hx : (x - x ^ 2) ^ n = 0<VAR>P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n<VAR>this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2<VAR>this : (Polynomial.aeval x) ((Polynomial.X - Polynomial.X ^ 2) ^ n) ∣ (Polynomial.aeval x) (P - P ^ 2)<GOAL>IsIdempotentElem (1 - (1 - x ^ n) ^ n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>x : R<VAR>n : ℕ<VAR>hx : (x - x ^ 2) ^ n = 0<VAR>P : Polynomial ℤ := 1 - (1 - Polynomial.X ^ n) ^ n<VAR>this✝ : (Polynomial.X - Polynomial.X ^ 2) ^ n ∣ P - P ^ 2<VAR>this : 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2 = 0<GOAL>IsIdempotentElem (1 - (1 - x ^ n) ^ n)
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>(fun s => ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩) ((fun s => ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩) ⟨k, ⟨l, ⟨s, hs⟩⟩⟩) = ⟨k, ⟨l, ⟨s, hs⟩⟩⟩
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>⟨k + l - s.card, ⟨s.card, ⟨Finset.map (finCongr ⋯).toEmbedding s, ⋯⟩⟩⟩ = ⟨k, ⟨l, ⟨s, hs⟩⟩⟩
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<GOAL>∀ (k' l' : ℕ), k' = k → l' = l → ∀ (hkl : k + l = k' + l') (hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'), ⟨k', ⟨l', ⟨Finset.map (finCongr hkl).toEmbedding s, hs'⟩⟩⟩ = ⟨k, ⟨l, ⟨s, hs⟩⟩⟩
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k'✝ l'✝ : ℕ<VAR>s : Finset (Fin (k'✝ + l'✝))<VAR>hs : s.card = l'✝<VAR>hkl : k'✝ + l'✝ = k'✝ + l'✝<VAR>hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'✝<GOAL>⟨k'✝, ⟨l'✝, ⟨Finset.map (finCongr hkl).toEmbedding s, hs'⟩⟩⟩ = ⟨k'✝, ⟨l'✝, ⟨s, hs⟩⟩⟩
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>n : ℕ<VAR>s : Finset (Fin n)<GOAL>(fun s => ⟨s.fst + s.snd.fst, ↑s.snd.snd⟩) ((fun s => ⟨s.fst - s.snd.card, ⟨s.snd.card, ⟨Finset.map (finCongr ⋯).toEmbedding s.snd, ⋯⟩⟩⟩) ⟨n, s⟩) = ⟨n, s⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<GOAL>Tendsto (fun m => ((κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)).toReal) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<GOAL>(κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<GOAL>Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0<GOAL>Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0<GOAL>Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>seq : ℕ → Set β<VAR>hseq : Monotone seq<VAR>hseq_iUnion : ⋃ i, seq i = univ<VAR>h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0<GOAL>(κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∨ (κ.fst a) (countablePartitionSet n x) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Inv α<VAR>a : Part α<VAR>ma : α<VAR>ha : ma ∈ a<GOAL>ma⁻¹ ∈ a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Inv α<VAR>a : Part α<VAR>ma : α<VAR>ha : ma ∈ a<GOAL>∃ a_1 ∈ a, a_1⁻¹ = ma⁻¹
<VAR>α : Type u_1<VAR>f g h✝ h : Perm α<VAR>x✝ : α<GOAL>(h * f * h⁻¹) x✝ = x✝ ∨ (h * g * h⁻¹) x✝ = x✝ ↔ f (h⁻¹ x✝) = h⁻¹ x✝ ∨ g (h⁻¹ x✝) = h⁻¹ x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<GOAL>(orthogonalProjection K) v = 0 ↔ v ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>h : (orthogonalProjection K) v = 0<GOAL>v ∈ Kᗮ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>h : v ∈ Kᗮ<GOAL>v - ↑0 ∈ Kᗮ
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x✝ y : (i : I) → f i<VAR>i✝ : I<VAR>inst✝⁴ : DecidableEq I<VAR>inst✝³ : (i : I) → One (f i)<VAR>inst✝² : (i : I) → One (g i)<VAR>inst✝¹ : (i : I) → One (h i)<VAR>inst✝ : One β<VAR>i : I<VAR>x : β<VAR>i' : I<GOAL>mulSingle i x i' = mulSingle i' x i
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K I⁻¹ = dual A K 1 * I
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<GOAL>let x := minAx.toCompleteLattice; ⨆ i, ⨅ j, f i j = ⨅ g, ⨆ i, f i (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<GOAL>⨅ g, ⨆ i, f i (g i) ≤ ⨆ i, ⨅ j, f i j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<GOAL>⨆ g, ⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j