ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<VAR>S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))<VAR>f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x<VAR>this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x<GOAL>n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<VAR>S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))<VAR>f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x<VAR>this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x<GOAL>(∏ x ∈ Finset.filter (fun x => x ≤ (2 * n).sqrt) S, f x) * ∏ x ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S, f x ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<VAR>S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))<VAR>f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x<VAR>this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x<GOAL>∏ x ∈ Finset.filter (fun x => x ≤ (2 * n).sqrt) S, f x ≤ (2 * n) ^ (2 * n).sqrt
<VAR>n : ℕ<VAR>n_large : 2 < n<VAR>no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n<VAR>n_pos : 0 < n<VAR>n2_pos : 1 ≤ 2 * n<VAR>S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))<VAR>f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x<VAR>this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x<GOAL>∏ x ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S, f x ≤ 4 ^ (2 * n / 3)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>inst✝ : Field k<VAR>φ : MvPowerSeries σ k<VAR>h : (constantCoeff σ k) φ = 0<VAR>n : σ →₀ ℕ<GOAL>(coeff k n) φ⁻¹ = (coeff k n) 0
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : (i : ι) → TopologicalSpace (E i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (E i)<VAR>inst✝⁵ : (i : ι) → Module 𝕜 (E i)<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>x : (i : ι) → E i<VAR>this : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>Continuous fun p => p x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : (i : ι) → TopologicalSpace (E i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (E i)<VAR>inst✝⁵ : (i : ι) → Module 𝕜 (E i)<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module 𝕜 F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)<VAR>x : (i : ι) → E i<VAR>this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>Continuous fun p => p x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Algebra R S<VAR>A B : Subalgebra R S<GOAL>(A.mulMap B).range = A ⊔ B
<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>s : Set J<VAR>inst✝ : Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)<GOAL>(fullSubcategoryInclusion fun x => x ∈ s).Final
<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>s : Set J<VAR>inst✝ : Small.{v, u} ↑s<VAR>hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)<VAR>i : J<GOAL>∃ c, Nonempty (i ⟶ (fullSubcategoryInclusion fun x => x ∈ s).obj c)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.num ≠ 0<GOAL>↑q⁻¹ = (↑q)⁻¹
<VAR>α : Type u_1<VAR>inst✝ : Lattice α<VAR>s : Sym2 α<GOAL>s.inf ≤ s.sup
<VAR>α : Type u_1<VAR>inst✝ : Lattice α<VAR>x✝ y✝ : α<GOAL>s(x✝, y✝).inf ≤ s(x✝, y✝).sup
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<GOAL>∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<VAR>h : 0 ≤ 1<GOAL>∃ t, ↑(t 0) = ↑0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, ↑(t m) = ↑1) ∧ ∀ (n m : ℕ), ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<VAR>h : 0 ≤ 1<VAR>n m : ℕ<GOAL>∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑I × ↑I)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : univ ⊆ ⋃ i, c i<VAR>δ : ℝ<VAR>δ_pos : δ > 0<VAR>ball_subset : ∀ x ∈ univ, ∃ i, Metric.ball x δ ⊆ c i<VAR>hδ : 0 < δ / 2<VAR>h : 0 ≤ 1<VAR>n m : ℕ<VAR>i : ι<VAR>hsub : Metric.ball (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) δ ⊆ c i<GOAL>∃ i, Icc (addNSMul h (δ / 2) n) (addNSMul h (δ / 2) (n + 1)) ×ˢ Icc (addNSMul h (δ / 2) m) (addNSMul h (δ / 2) (m + 1)) ⊆ c i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<GOAL>t.centerMass (-w) z = t.centerMass w z
<VAR>R✝ : Type u_1<VAR>inst✝²⁰ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>inst✝¹⁹ : Semiring A✝<VAR>inst✝¹⁸ : Algebra R✝ A✝<VAR>M✝ : Type u_3<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module A✝ M✝<VAR>inst✝¹⁵ : Module R✝ M✝<VAR>inst✝¹⁴ : IsScalarTower R✝ A✝ M✝<VAR>N : Type u_4<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module A✝ N<VAR>inst✝¹¹ : Module R✝ N<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ N<VAR>R : Type u_5<VAR>A : Type u_6<VAR>M : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module A M<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>r : R<VAR>m : M<VAR>h : r • m = 0<GOAL>r = 0 ∨ m = 0
<VAR>R✝ : Type u_1<VAR>inst✝²⁰ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>inst✝¹⁹ : Semiring A✝<VAR>inst✝¹⁸ : Algebra R✝ A✝<VAR>M✝ : Type u_3<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module A✝ M✝<VAR>inst✝¹⁵ : Module R✝ M✝<VAR>inst✝¹⁴ : IsScalarTower R✝ A✝ M✝<VAR>N : Type u_4<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module A✝ N<VAR>inst✝¹¹ : Module R✝ N<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ N<VAR>R : Type u_5<VAR>A : Type u_6<VAR>M : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module A M<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>r : R<VAR>m : M<VAR>h : (algebraMap R A) r • m = 0<GOAL>r = 0 ∨ m = 0
<VAR>R✝ : Type u_1<VAR>inst✝²⁰ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>inst✝¹⁹ : Semiring A✝<VAR>inst✝¹⁸ : Algebra R✝ A✝<VAR>M✝ : Type u_3<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module A✝ M✝<VAR>inst✝¹⁵ : Module R✝ M✝<VAR>inst✝¹⁴ : IsScalarTower R✝ A✝ M✝<VAR>N : Type u_4<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module A✝ N<VAR>inst✝¹¹ : Module R✝ N<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ N<VAR>R : Type u_5<VAR>A : Type u_6<VAR>M : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module A M<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>r : R<VAR>m : M<VAR>h : (algebraMap R A) r • m = 0<VAR>H : (algebraMap R A) r = 0<GOAL>r = 0 ∨ m = 0
<VAR>R✝ : Type u_1<VAR>inst✝²⁰ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>inst✝¹⁹ : Semiring A✝<VAR>inst✝¹⁸ : Algebra R✝ A✝<VAR>M✝ : Type u_3<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module A✝ M✝<VAR>inst✝¹⁵ : Module R✝ M✝<VAR>inst✝¹⁴ : IsScalarTower R✝ A✝ M✝<VAR>N : Type u_4<VAR>inst✝¹³ : AddCommMonoid N<VAR>inst✝¹² : Module A✝ N<VAR>inst✝¹¹ : Module R✝ N<VAR>inst✝¹⁰ : IsScalarTower R✝ A✝ N<VAR>R : Type u_5<VAR>A : Type u_6<VAR>M : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module A M<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : NoZeroSMulDivisors R A<VAR>inst✝ : NoZeroSMulDivisors A M<VAR>r : R<VAR>m : M<VAR>h : (algebraMap R A) r • m = 0<VAR>H : m = 0<GOAL>r = 0 ∨ m = 0
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Group α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>x.2.card + (e⁻¹ • x.2).card = 2 * x.2.card
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom = C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
<VAR>σ K : Type u<VAR>inst✝ : Field K<GOAL>Module.rank K (MvPolynomial σ K) = Cardinal.mk (σ →₀ ℕ)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹¹ : OrderedSemiring 𝕜<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalSpace F<VAR>inst✝⁸ : AddCommMonoid E<VAR>inst✝⁷ : AddCommMonoid F<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : Module 𝕜 F<VAR>s✝ : Set E<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set β<VAR>hs : s.OrdConnected<GOAL>StrictConvex 𝕜 s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹¹ : OrderedSemiring 𝕜<VAR>inst✝¹⁰ : TopologicalSpace E<VAR>inst✝⁹ : TopologicalSpace F<VAR>inst✝⁸ : AddCommMonoid E<VAR>inst✝⁷ : AddCommMonoid F<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : Module 𝕜 F<VAR>s✝ : Set E<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set β<VAR>hs : s.OrdConnected<VAR>x : β<VAR>hx : x ∈ s<VAR>y : β<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>(fun x y => openSegment 𝕜 x y ⊆ interior s) x y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<GOAL>toSubmodule S * toSubmodule T ≤ toSubmodule (S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<GOAL>∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Subalgebra R A<VAR>y : A<VAR>hy : y ∈ toSubmodule S<VAR>z : A<VAR>hz : z ∈ toSubmodule T<GOAL>y * z ∈ S ⊔ T
<VAR>n✝ : ℕ<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∏ i ∈ n.divisors, f (n / i) i
<VAR>n✝ : ℕ<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ x ∈ n.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 = ∏ i ∈ n.divisors, f (n / i) i
<VAR>s step n : Nat<VAR>x✝ : 0 < n + 1<GOAL>(range' s (n + 1) step)[0]? = some (s + step * 0)
<VAR>s step m n : Nat<VAR>h : m + 1 < n + 1<GOAL>(range' s (n + 1) step)[m + 1]? = some (s + step * (m + 1))
<VAR>s step m n : Nat<VAR>h : m + 1 < n + 1<GOAL>(range' (s + step) n step)[m]? = some (s + step * (m + 1))
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<GOAL>cthickening δ E = ⋃ x ∈ E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>hδ : 0 ≤ δ<VAR>hE : IsCompact ∅<GOAL>cthickening δ ∅ = ⋃ x ∈ ∅, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<GOAL>cthickening δ E = ⋃ x ∈ E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ E<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ E<VAR>y : α<VAR>yE : y ∈ E<VAR>hy : infEdist x E = edist x y<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ E<VAR>y : α<VAR>yE : y ∈ E<VAR>hy : infEdist x E = edist x y<VAR>D1 : edist x y ≤ ENNReal.ofReal δ<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<VAR>hne : E.Nonempty<VAR>x : α<VAR>hx : x ∈ cthickening δ E<VAR>y : α<VAR>yE : y ∈ E<VAR>hy : infEdist x E = edist x y<VAR>D1 : edist x y ≤ ENNReal.ofReal δ<VAR>D2 : dist x y ≤ δ<GOAL>x ∈ ⋃ x ∈ E, closedBall x δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifIntegrable ((fun x => g) + fun n => f n - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifIntegrable (fun x => g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), Memℒp (f n) p μ<VAR>hg : Memℒp g p μ<VAR>hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)<VAR>this : f = (fun x => g) + fun n => f n - g<GOAL>UnifIntegrable (fun n => f n - g) p μ
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : IsHausdorff ⊤ M<VAR>x y : M<VAR>n : ℕ<GOAL>x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type u_3<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h : IsHausdorff ⊤ M<VAR>x y : M<VAR>n : ℕ<GOAL>x - y ≡ 0 [SMOD ⊤]
<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>P : Fin 3 → R<VAR>u : R<GOAL>W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P
<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>P : Fin 3 → R<VAR>u : R<GOAL>-(u ^ 4 * W'.dblU P) * ((u ^ 4) ^ 2 * W'.dblX P - u ^ 2 * P x * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 2) + u ^ 3 * P y * (u ^ 3 * P y - u ^ 3 * W'.negY P) ^ 3 = (u ^ 4) ^ 3 * (-W'.dblU P * (W'.dblX P - P x * (P y - W'.negY P) ^ 2) + P y * (P y - W'.negY P) ^ 3)
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#(α ≃ β) = 0 ↔ #α ≠ #β
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>a : ℚ<VAR>hp : Fact (Nat.Prime p)<VAR>H : 1 < padicNorm p a<GOAL>¬a.isInt = true
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>a : ℚ<VAR>hp : Fact (Nat.Prime p)<VAR>H : a.isInt = true<GOAL>padicNorm p a ≤ 1
<VAR>p✝ : ℕ<VAR>hp✝ : Fact (Nat.Prime p✝)<VAR>p : ℕ<VAR>a : ℚ<VAR>hp : Fact (Nat.Prime p)<VAR>H : a.isInt = true<GOAL>padicNorm p ↑a.num ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<GOAL>1 ≤ ‖A‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>h : ‖A‖ < 1<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>h : ‖A‖ < 1<VAR>i : α<VAR>j : β<GOAL>A i j = 0 i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>h : ‖A‖ < 1<VAR>i : α<VAR>j : β<GOAL>A i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>h : ∀ (i : α) (j : β), ‖A i j‖ < 1<VAR>i : α<VAR>j : β<GOAL>A i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>i : α<VAR>j : β<VAR>h : ‖A i j‖ < 1<GOAL>A i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>i : α<VAR>j : β<VAR>h : |↑(A i j)| < 1<GOAL>A i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>hA : A ≠ 0<VAR>i : α<VAR>j : β<VAR>h : |A i j| < 1<GOAL>A i j = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : ¬p.natDegree < n<GOAL>p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : n ≤ p.natDegree<GOAL>p.mirror.coeff n = p.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : n ≤ p.natDegree<GOAL>p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : n ≤ p.natDegree<VAR>h3 : ¬p.natTrailingDegree ≤ n<GOAL>p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : n ≤ p.natDegree<VAR>h3 : n < p.natTrailingDegree<GOAL>p.mirror.coeff n = p.coeff (p.natDegree + p.natTrailingDegree - n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>h2 : n ≤ p.natDegree<VAR>h3 : n < p.natTrailingDegree<GOAL>p.mirror.coeff n = 0
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>this : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>this : ∀ (n : ℕ), ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n<VAR>φ : ℕ → ℕ<VAR>φ_extr : StrictMono φ<VAR>hφ : ∀ (n l : ℕ), l ≥ φ n → (u l, u (φ n)) ∈ V n<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<GOAL>Continuous f ↔ ∀ (b : β), Continuous fun x => f (x, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<GOAL>ContinuousOn f univ ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) univ
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).cos * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).cos * ‖y + x‖ = ‖y‖
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>x y : ↑F F.M<VAR>h : M.mk x = M.mk y<GOAL>x = y
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx : x ≠ 0<VAR>h'x : x ≠ ⊤<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>R : P.M → P.M → Prop<VAR>h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)<VAR>x y : P.M<VAR>h' : R x y<VAR>this : Inhabited P.A<GOAL>x = y