ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<GOAL>(convexHull 𝕜) s ⊆ ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
<VAR>𝕜 : Type u_1<VAR>E : Type u<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<GOAL>⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) s
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j k : N →* P<VAR>h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a<GOAL>j = k
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j k : N →* P<VAR>h : ∀ (a : M), (j.comp f.toMap) a = (k.comp f.toMap) a<GOAL>f.lift ⋯ = f.lift ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : NonAssocSemiring S<VAR>inst✝¹ : FunLike F R S<VAR>n : ℕ<VAR>h✝ : NeZero ↑n<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>h : ↑n = 0<GOAL>f ↑n = f 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<VAR>w : E i<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E i<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<GOAL>(LinearMap.single i) w ∈ tangentConeAt 𝕜 (univ.pi s) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<VAR>w : E i<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E i<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<VAR>this : ∀ (n : ℕ) (j : ι), j ≠ i → ∃ d', x j + d' ∈ s j ∧ ‖c n • d'‖ < (1 / 2) ^ n<GOAL>(LinearMap.single i) w ∈ tangentConeAt 𝕜 (univ.pi s) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<VAR>w : E i<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E i<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<VAR>d' : ℕ → (j : ι) → E j<VAR>hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j<VAR>hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n<GOAL>(LinearMap.single i) w ∈ tangentConeAt 𝕜 (univ.pi s) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝¹ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<VAR>w : E i<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E i<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<VAR>d' : ℕ → (j : ι) → E j<VAR>hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j<VAR>hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n<VAR>n : ℕ<VAR>hn : x i + d n ∈ s i<VAR>j : ι<VAR>x✝ : j ∈ univ<GOAL>(x + (fun n => Function.update (d' n) i (d n)) n) j ∈ s j
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E✝ : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E✝<VAR>inst✝⁷ : NormedSpace 𝕜 E✝<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>x✝ y : E✝<VAR>s✝ t : Set E✝<VAR>ι : Type u_5<VAR>inst✝² : DecidableEq ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>s : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>i : ι<VAR>hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)<VAR>w : E i<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E i<VAR>hd : ∀ᶠ (n : ℕ) in atTop, x i + d n ∈ s i<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<VAR>d' : ℕ → (j : ι) → E j<VAR>hd's : ∀ (n : ℕ) (j : ι), j ≠ i → x j + d' n j ∈ s j<VAR>hcd' : ∀ (n : ℕ) (j : ι), j ≠ i → ‖c n • d' n j‖ < (1 / 2) ^ n<VAR>j : ι<GOAL>Tendsto (fun i_1 => (c i_1 • (fun n => Function.update (d' n) i (d n)) i_1) j) atTop (𝓝 ((LinearMap.single i) w j))
<VAR>B : Type u<VAR>inst✝ : Quiver B<VAR>a b c : B<VAR>p : Path a b<VAR>f g : Hom b c<VAR>η' : Hom₂ f g<GOAL>(preinclusion B).map { as := p } ◁ Quot.mk Rel η' ≫ (normalizeIso p g).hom = (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>wittPolyProd p (n + 1) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1)) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1)) * (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1)) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1)) * (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1)) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1)) * (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1)) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1)) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) + (↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))) + remainder p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) = remainder p n + (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) + (↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>(∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + (↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)))) = remainder p n + (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<VAR>mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))<GOAL>↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) = -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (0, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) + (↑p ^ (n + 1) * X (1, n + 1) * ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) + ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1)))))
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : ContinuousConstSMul G α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>c : G<VAR>h : Tendsto (fun x => c • f x) l (𝓝 (c • a))<GOAL>Tendsto f l (𝓝 a)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y a b : R<VAR>h : a * x + b * y = 1<GOAL>IsCoprime (-x) y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y a b : R<VAR>h : a * x + b * y = 1<GOAL>-a * -x + b * y = 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : LinearOrderedSemiring R<VAR>inst✝⁴ : FloorSemiring R<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : OrderTopology R<VAR>inst✝¹ : MeasurableSpace R<VAR>inst✝ : OpensMeasurableSpace R<VAR>f : α → R<VAR>n : R<GOAL>MeasurableSet (floor ⁻¹' {⌊n⌋₊})
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝ : Semigroup G<VAR>a b c : G<VAR>h : SemiconjBy a b c<VAR>j : G<GOAL>a * (b * j) = c * (a * j)
<VAR>K R : Type u<VAR>V V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → V<GOAL>LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (range b)
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<VAR>hb : b ≠ last n<GOAL>a.pred ha < b.castPred hb ↔ a ≤ b
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y L : R<GOAL>C (f L) * (X - C (f x)) + C (f y) = Polynomial.map f (C L * (X - C x) + C y)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R✝ : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>R : ℝ<GOAL>dist ((R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ((R / dist y c) ^ 2 • (y -ᵥ c) +ᵥ c) = R ^ 2 / (dist x c * dist y c) * dist x y
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c d x y z : P<VAR>r R✝ : ℝ<VAR>hx : x ≠ c<VAR>hy : y ≠ c<VAR>R : ℝ<GOAL>dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>univ.noncommProd (fun i => Pi.mulSingle i (x i)) ⋯ i = x i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>univ.noncommProd (fun i_1 => (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M i_1) (x i_1))) ⋯ = x i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>(↑univ).Pairwise fun a b => Commute ((fun i => (MonoidHom.mulSingle M i) (x i)) a) ((fun i => (MonoidHom.mulSingle M i) (x i)) b)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>ι → M i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>∀ x_1 ∈ insert i (univ.erase i), (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = ?h.convert_3 x_1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>inst✝⁵ : Monoid β<VAR>inst✝⁴ : Monoid γ<VAR>inst✝³ : FunLike F β γ<VAR>M : ι → Type u_6<VAR>inst✝² : (i : ι) → Monoid (M i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>x : (i : ι) → M i<VAR>i : ι<GOAL>(insert i (univ.erase i)).noncommProd ?h.convert_3 ⋯ = x i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M₁<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid N₁<VAR>inst✝⁸ : AddCommMonoid N₂<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : Module R N₂<VAR>inst✝² : Module R P<VAR>inst✝¹ : PartialOrder P<VAR>inst✝ : CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>(Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M₁<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid N₁<VAR>inst✝⁸ : AddCommMonoid N₂<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module R M₂<VAR>inst✝⁴ : Module R N₁<VAR>inst✝³ : Module R N₂<VAR>inst✝² : Module R P<VAR>inst✝¹ : PartialOrder P<VAR>inst✝ : CovariantClass P P (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>Q₁ : QuadraticMap R M₁ P<VAR>Q₂ : QuadraticMap R M₂ P<GOAL>((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic ↔ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<GOAL>Tendsto (fun n => u n / ↑n) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<GOAL>∀ (a : ℝ), 1 < a → ∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<GOAL>∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<GOAL>∃ c, (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧ Tendsto c atTop atTop ∧ Tendsto (fun n => u (c n) / ↑(c n)) atTop (𝓝 l)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<GOAL>∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊<GOAL>∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊<VAR>A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))<GOAL>∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)