ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<VAR>F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))<VAR>hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<VAR>F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))<VAR>hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0<VAR>key : ∑ x : σ → K, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<VAR>F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))<VAR>hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0<VAR>key : ∑ x : σ → K, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })<GOAL>∑ x : σ → K, (eval x) F = 0
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<VAR>F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))<VAR>hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0<VAR>key : ∑ x : σ → K, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })<GOAL>F.totalDegree < (q - 1) * Fintype.card σ
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<VAR>hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0<VAR>F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))<VAR>hF : ∀ (x : σ → K), (eval x) F = if x ∈ S then 1 else 0<VAR>key : ∑ x : σ → K, (eval x) F = ↑(Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 })<VAR>i : ι<VAR>x✝ : i ∈ s<GOAL>(1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>n : ℕ<VAR>a : α<GOAL>n • (a ::ₘ s) = n • {a} + n • s
<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>f : α → β<VAR>s : Set α<VAR>h : IsOpenMap (s.restrict f)<VAR>finv : β → α<VAR>hleft : LeftInvOn finv f s<GOAL>ContinuousOn finv (f '' s)
<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>f : α → β<VAR>s : Set α<VAR>h : IsOpenMap (s.restrict f)<VAR>finv : β → α<VAR>hleft : LeftInvOn finv f s<VAR>t : Set α<VAR>ht : IsOpen t<GOAL>IsOpen (f '' (t ∩ s))
<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>f : α → β<VAR>s : Set α<VAR>h : IsOpenMap (s.restrict f)<VAR>finv : β → α<VAR>hleft : LeftInvOn finv f s<VAR>t : Set α<VAR>ht : IsOpen t<GOAL>finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<GOAL>Set.range ⇑(asOrderHom (standardSimplex.const (n + 2) k m)) ∪ {i} ≠ Set.univ
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<GOAL>¬univ ⊆ {i, k}
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<VAR>h : univ ⊆ {i, k}<GOAL>False
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<VAR>h : univ ⊆ {i, k}<VAR>this : univ.card ≤ 2<GOAL>False
<VAR>n : ℕ<VAR>i k : Fin (n + 3)<VAR>m : SimplexCategoryᵒᵖ<VAR>h : univ ⊆ {i, k}<VAR>this : n + 3 ≤ 2<GOAL>False
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>arccos (⟪-x, -y⟫_ℝ / (‖-x‖ * ‖-y‖)) = arccos (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖))
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<GOAL>slope f x y ≤ f'
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<GOAL>∀ᶠ (c : ℝ) in 𝓝[<] y, slope f x y ≤ slope f y c
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝 y, x_1 ∈ Iio y → (f x - f y) / (x - y) ≤ (f x_1 - f y) / (x_1 - y)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>t : ℝ<VAR>ht : x < t<VAR>ht' : t < y<GOAL>(f x - f y) / (x - y) ≤ (f t - f y) / (t - y)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<VAR>t : ℝ<VAR>ht : x < t<VAR>ht' : t < y<GOAL>t ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>a : Fin n.succ → ℕ<GOAL>(map d) a % d = a 0 % d
<VAR>𝒮 : Type u₁<VAR>inst✝ : Category.{v₁, u₁} 𝒮<VAR>𝒳 : BasedCategory 𝒮<VAR>𝒴 : BasedCategory 𝒮<VAR>𝒵 : BasedCategory 𝒮<VAR>F : 𝒳 ⥤ᵇ 𝒴<VAR>G : 𝒴 ⥤ᵇ 𝒵<GOAL>(F.toFunctor ⋙ G.toFunctor) ⋙ 𝒵.p = 𝒳.p
<VAR>J : Type<VAR>inst✝⁴ : Finite J<VAR>K : Type<VAR>inst✝³ : Finite K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : J → C<VAR>g : K → C<VAR>m : (j : J) → (k : K) → f j ⟶ g k<VAR>x✝¹ : J<VAR>x✝ : K<GOAL>components (matrix m) x✝¹ x✝ = m x✝¹ x✝
<VAR>s : ℕ<VAR>h : s ≠ 0<GOAL>(s.xgcdAux 1 0 0 0 1).2.2 = 0
<VAR>s : ℕ<VAR>h : s.succ ≠ 0<GOAL>(s.succ.xgcdAux 1 0 0 0 1).2.2 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : NonUnitalNonAssocSemiring A<VAR>inst✝ : DistribMulAction R A<VAR>r : R<VAR>a : A<GOAL>0 • 0 + r • a + a * 0 = r • a
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>a b c d : α<GOAL>Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 1<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>(f + g).prod h = f.prod h * g.prod h
<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✝⁶ : OrderedRing 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>x z : P<VAR>r : R<GOAL>(lineMap x z) r ∈ affineSpan R {x, z}
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.58544, u_1} C<VAR>inst✝⁵ : Category.{?u.58548, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).hom.app X = (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).hom.app X) ≫ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : s =ᶠ[ae μ] univ<GOAL>univ ∪ t =ᶠ[ae μ] univ
<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>r : ℝ≥0<GOAL>radius 0 = ⊤
<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>r : ℝ≥0<GOAL>(constFormalMultilinearSeries 𝕜 E 0).radius = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q : R[X]<VAR>P : R[X] → Prop<VAR>p : R[X]<VAR>h0 : 0 < p.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (C a * X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)<VAR>h : 0 < degree 0<GOAL>P 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q : R[X]<VAR>P : R[X] → Prop<VAR>p : R[X]<VAR>h0 : 0 < p.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (C a * X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)<VAR>h : 0 < ⊥<GOAL>P 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ q : R[X]<VAR>P : R[X] → Prop<VAR>p✝ : R[X]<VAR>h0✝ : 0 < p✝.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (C a * X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)<VAR>p : R[X]<VAR>a : R<VAR>heq0 : p.coeff 0 = 0<VAR>x✝ : a ≠ 0<VAR>ih : 0 < p.degree → P p<VAR>h0 : 0 < (p + C a).degree<VAR>h : 0 ≥ p.degree<GOAL>0 < (C a).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ q : R[X]<VAR>P : R[X] → Prop<VAR>p✝ : R[X]<VAR>h0✝ : 0 < p✝.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (C a * X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)<VAR>p : R[X]<VAR>x✝ : p ≠ 0<VAR>ih : 0 < p.degree → P p<VAR>h0' : 0 < (p * X).degree<VAR>h0 : ¬0 < p.degree<GOAL>P (p * X)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ q : R[X]<VAR>P : R[X] → Prop<VAR>p✝ : R[X]<VAR>h0✝ : 0 < p✝.degree<VAR>hC : ∀ {a : R}, a ≠ 0 → P (C a * X)<VAR>hX : ∀ {p : R[X]}, 0 < p.degree → P p → P (p * X)<VAR>hadd : ∀ {p : R[X]} {a : R}, 0 < p.degree → P p → P (p + C a)<VAR>p : R[X]<VAR>x✝ : p ≠ 0<VAR>ih : 0 < p.degree → P p<VAR>h0' : 0 < (C (p.coeff 0) * X).degree<VAR>h0 : ¬0 < p.degree<GOAL>P (C (p.coeff 0) * X)
<VAR>e : ONote<VAR>n : ℕ+<VAR>a₁ a₂ : ONote<VAR>h : a₁ < a₂<GOAL>e.oadd n a₁ < e.oadd n a₂
<VAR>e : ONote<VAR>n : ℕ+<VAR>a₁ a₂ : ONote<VAR>h : a₁ < a₂<GOAL>(e.oadd n a₁).repr < (e.oadd n a₂).repr
<VAR>e : ONote<VAR>n : ℕ+<VAR>a₁ a₂ : ONote<VAR>h : a₁ < a₂<GOAL>ω ^ e.repr * ↑↑n + a₁.repr < ω ^ e.repr * ↑↑n + a₂.repr
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>S : Set E<VAR>q : ℕ<VAR>inst✝¹ : ExpChar F q<VAR>n : ℕ<VAR>L : IntermediateField F E := adjoin F S<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)<GOAL>L = M
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>S : Set E<VAR>q : ℕ<VAR>inst✝¹ : ExpChar F q<VAR>n : ℕ<VAR>L : IntermediateField F E := adjoin F S<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)<VAR>hi : M ≤ L<GOAL>L = M
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>S : Set E<VAR>q : ℕ<VAR>inst✝¹ : ExpChar F q<VAR>n : ℕ<VAR>L : IntermediateField F E := adjoin F S<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)<VAR>hi : M ≤ L<VAR>this : Algebra ↥M ↥L := (inclusion hi).toAlgebra<GOAL>L = M
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>S : Set E<VAR>q : ℕ<VAR>inst✝¹ : ExpChar F q<VAR>n : ℕ<VAR>L : IntermediateField F E := adjoin F S<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)<VAR>hi : M ≤ L<VAR>this✝ : Algebra ↥M ↥L := (inclusion hi).toAlgebra<VAR>this : Algebra.IsSeparable ↥M ↥(extendScalars hi)<GOAL>L = M
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>S : Set E<VAR>q : ℕ<VAR>inst✝¹ : ExpChar F q<VAR>n : ℕ<VAR>L : IntermediateField F E := adjoin F S<VAR>inst✝ : Algebra.IsSeparable F ↥L<VAR>M : IntermediateField F E := adjoin F ((fun x => x ^ q ^ n) '' S)<VAR>hi : M ≤ L<VAR>this✝¹ : Algebra ↥M ↥L := (inclusion hi).toAlgebra<VAR>this✝ : Algebra.IsSeparable ↥M ↥(extendScalars hi)<VAR>this : IsPurelyInseparable ↥M ↥(extendScalars hi)<GOAL>L = M
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hφ : Tendsto (fun n => support (φ n)) l (𝓝 0).smallSets<VAR>hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ<VAR>hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)<VAR>hk : Tendsto k l (𝓝 x₀)<GOAL>Tendsto (fun i => (φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ<VAR>hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)<VAR>hk : Tendsto k l (𝓝 x₀)<VAR>hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t<GOAL>Tendsto (fun i => (φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ<VAR>hcg : ∀ ε > 0, ∀ᶠ (x : ι × G) in l ×ˢ 𝓝 x₀, dist (uncurry g x) z₀ < ε<VAR>hk : Tendsto k l (𝓝 x₀)<VAR>hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t<GOAL>∀ ε > 0, ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ<VAR>hk : Tendsto k l (𝓝 x₀)<VAR>hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t<VAR>hcg : ∀ ε > 0, ∃ pa, (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ {i : ι}, pa i → ∀ {x : G}, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε<GOAL>∀ ε > 0, ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>ι : Type u_1<VAR>g : ι → G → E'<VAR>l : Filter ι<VAR>x₀ : G<VAR>z₀ : E'<VAR>φ : ι → G → ℝ<VAR>k : ι → G<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x<VAR>hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1<VAR>hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ<VAR>hk : Tendsto k l (𝓝 x₀)<VAR>hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t<VAR>hcg : ∀ ε > 0, ∃ pa, (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ {i : ι}, pa i → ∀ {x : G}, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε