ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ι : Sort u_9<VAR>v : ι → M<GOAL>span R (range v) = ⨆ i, span R {v i}
<VAR>b o✝ : Ordinal.{u}<VAR>x : Ordinal.{u} × Ordinal.{u}<VAR>o : Ordinal.{u}<VAR>ho : o ≠ 0<VAR>IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2<GOAL>x ∈ CNF b o → 0 < x.2
<VAR>b o✝ : Ordinal.{u}<VAR>x : Ordinal.{u} × Ordinal.{u}<VAR>o : Ordinal.{u}<VAR>ho : o ≠ 0<VAR>IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2<GOAL>x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)<GOAL>IsHomogeneous 𝒜 (⨆ i, f i)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), ∃ S, f i = span (Subtype.val '' S)<GOAL>∃ S, ⨆ i, f i = span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>s : κ → Set ↥(homogeneousSubmonoid 𝒜)<VAR>hs : ∀ (i : κ), f i = span (Subtype.val '' s i)<GOAL>⨆ i, f i = span (Subtype.val '' ⋃ i, s i)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>s : κ → Set ↥(homogeneousSubmonoid 𝒜)<VAR>hs : ∀ (i : κ), f i = span (Subtype.val '' s i)<GOAL>⨆ i, f i = ⨆ i, span (Subtype.val '' s i)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>s : κ → Set ↥(homogeneousSubmonoid 𝒜)<VAR>hs : ∀ (i : κ), f i = span (Subtype.val '' s i)<GOAL>(fun i => f i) = fun i => span (Subtype.val '' s i)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>x : ℝ<GOAL>0 < gaussianPDF μ v x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>x : ℝ<GOAL>0 < gaussianPDFReal μ v x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>s : Multiset α<GOAL>s.toList.prod = s.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s✝ t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>s : Multiset α<GOAL>s.toList.prod = (↑s.toList).prod
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>inst✝ : LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>(∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>c : β<GOAL>HasFiniteIntegral (fun x => c) μ ↔ c = 0 ∨ μ univ < ⊤
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : InnerProductSpace ℝ V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : V → E<VAR>hf : Integrable f volume<GOAL>Tendsto (fun c => ∫ (v : V), cexp (-↑c⁻¹ * ↑‖v‖ ^ 2) • f v) atTop (𝓝 (∫ (v : V), f v))
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : InnerProductSpace ℝ V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : V → E<VAR>hf : Integrable f volume<GOAL>∀ᵐ (a : V), Tendsto (fun n => cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) atTop (𝓝 (f a))
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : InnerProductSpace ℝ V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : V → E<VAR>hf : Integrable f volume<GOAL>∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (fun a => cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a) volume
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup V<VAR>inst✝⁵ : InnerProductSpace ℝ V<VAR>inst✝⁴ : MeasurableSpace V<VAR>inst✝³ : BorelSpace V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : V → E<VAR>hf : Integrable f volume<GOAL>∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : NullMeasurableSet s (map f μ)<GOAL>(map f μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)<GOAL>((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ) s = μ (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)<GOAL>((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (AEMeasurable.mk f hf ⁻¹' s)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : DecidableEq R<VAR>x y : R<VAR>hxy : ¬x = y<GOAL>rootMultiplicity x (X - C y) = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>c < a → c < b → c ∉ [[a, b]]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>c < a → c < b → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁷ : Semiring R₁<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁴ : TopologicalSpace M₁<VAR>inst✝³ : TopologicalSpace M₂<VAR>inst✝² : TopologicalSpace M₃<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M₁ → M₂<VAR>g : M₂ → M₃<VAR>hg : Continuous g<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : f ⁻¹' K ∈ 𝓝 0<GOAL>IsCompactOperator (g ∘ f)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁷ : Semiring R₁<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁴ : TopologicalSpace M₁<VAR>inst✝³ : TopologicalSpace M₂<VAR>inst✝² : TopologicalSpace M₃<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M₁ → M₂<VAR>g : M₂ → M₃<VAR>hg : Continuous g<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : f ⁻¹' K ∈ 𝓝 0<GOAL>f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝⁷ : Semiring R₁<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁴ : TopologicalSpace M₁<VAR>inst✝³ : TopologicalSpace M₂<VAR>inst✝² : TopologicalSpace M₃<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M₁ → M₂<VAR>g : M₂ → M₃<VAR>hg : Continuous g<VAR>K : Set M₂<VAR>hK : IsCompact K<VAR>hKf : f ⁻¹' K ∈ 𝓝 0<GOAL>f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>x ≤ y ↔ x' ≤ y'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>¬y < x ↔ ¬y' < x'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>y < x ↔ y' < x'
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp x y = cmp x' y'<GOAL>cmp y x = cmp y' x'
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<VAR>step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<VAR>step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<VAR>step2 : HasSum (fun i => fourierCoeff (⇑B) i • (fourier i) ↑y) (B ↑y)<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<VAR>step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<VAR>step2 : HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)<GOAL>HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<VAR>step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<VAR>step2 : HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)<VAR>n : ℤ<GOAL>1 / ↑n ^ k * (fourier n) ↑y = -(2 * ↑π * I) ^ k / ↑k ! * (-↑k ! / (2 * ↑π * I * ↑n) ^ k) • (fourier n) ↑y
<VAR>k : ℕ<VAR>hk : 2 ≤ k<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 1<VAR>y : ℝ<VAR>hy : y ∈ Ico 0 1<VAR>B : C(𝕌, ℂ) := { toFun := ofReal' ∘ periodizedBernoulli k, continuous_toFun := ⋯ }<VAR>step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k<VAR>step2 : HasSum (fun i => (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)<GOAL>↑(bernoulliFun k y) = B ↑y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>inst✝ : MeasurableSingletonClass (NullMeasurableSpace α μ)<VAR>s : Finset α<GOAL>NullMeasurableSet (↑s) μ
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>(A * B).FermatPsp b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<VAR>ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<VAR>ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)<VAR>ha₆ : 2 * p ∣ A * B - 1<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<VAR>ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)<VAR>ha₆ : 2 * p ∣ A * B - 1<VAR>ha₇ : A * B ∣ b ^ (2 * p) - 1<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<VAR>ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)<VAR>ha₇ : A * B ∣ b ^ (2 * p) - 1<VAR>q : ℕ<VAR>hq : A * B - 1 = 2 * p * q<GOAL>(A * B).ProbablePrime b
<VAR>b : ℕ<VAR>b_ge_two : 2 ≤ b<VAR>p : ℕ<VAR>p_prime : Prime p<VAR>p_gt_two : 2 < p<VAR>not_dvd : ¬p ∣ b * (b ^ 2 - 1)<VAR>A : ℕ := (b ^ p - 1) / (b - 1)<VAR>B : ℕ := (b ^ p + 1) / (b + 1)<VAR>hi_A : 1 < A<VAR>hi_B : 1 < B<VAR>hi_AB : 1 < A * B<VAR>hi_b : 0 < b<VAR>hi_p : 1 ≤ p<VAR>hi_bsquared : 0 < b ^ 2 - 1<VAR>hi_bpowtwop : 1 ≤ b ^ (2 * p)<VAR>hi_bpowpsubone : 1 ≤ b ^ (p - 1)<VAR>p_odd : Odd p<VAR>AB_not_prime : ¬Prime (A * B)<VAR>AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)<VAR>hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1<VAR>ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)<VAR>ha₂ : 2 ∣ b ^ p + b<VAR>ha₃ : p ∣ b ^ (p - 1) - 1<VAR>ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1<VAR>ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)<VAR>ha₇ : A * B ∣ b ^ (2 * p) - 1<VAR>q : ℕ<VAR>hq : A * B - 1 = 2 * p * q<VAR>ha₈ : b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1<GOAL>(A * B).ProbablePrime b