ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>(closure L).toFun (⇑f ⁻¹' ↑t) = s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' ↑t)) = Substructure.map f.toHom s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>↑t ⊆ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ ↑t<GOAL>x ∈ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ ↑t<VAR>h' : x ∈ ↑((closure L).toFun ↑t)<GOAL>x ∈ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ ↑t<VAR>h' : x ∈ ↑(Substructure.map f.toHom s)<GOAL>x ∈ range ⇑f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>B : D<GOAL>(comparisonAdjunction adj).counit.app B = colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) (counitCofork adj B)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<VAR>B : D<GOAL>coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫ (comparisonAdjunction adj).counit.app B = coequalizer.π (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A)) ≫ colimit.desc (parallelPair (F.map (G.map (adj.counit.app B))) (adj.counit.app (F.obj (G.obj B)))) (counitCofork adj B)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>c • boundedBy m = boundedBy (c • m)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>OuterMeasure.ofFunction (c • fun s => ⨆ (_ : s.Nonempty), m s) ⋯ = OuterMeasure.ofFunction (fun s => ⨆ (_ : s.Nonempty), (c • m) s) ⋯
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>s : Set α<GOAL>(c • fun s => ⨆ (_ : s.Nonempty), m s) s = ⨆ (_ : s.Nonempty), (c • m) s
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M ≃+ M₁<VAR>hi : Bijective ⇑i<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>Module.rank R M = Module.rank R' M₁
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>f : α → β → α<VAR>xs : t β<VAR>x : α<GOAL>foldl f x xs = List.foldl f x (toList xs)
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>f : α → β → α<VAR>xs : t β<VAR>x : α<GOAL>foldl f x xs = unop ((Foldl.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x
<VAR>m n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : AddCommMonoid α<VAR>n : ℕ<VAR>a : Fin (n + 2) → α<GOAL>sum a = ∑ i : Fin (n + 2), a i
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝² : MonoidWithZero M₀<VAR>a : M₀<VAR>m n : ℕ<VAR>inst✝¹ : NoZeroDivisors M₀<VAR>inst✝ : Nontrivial M₀<GOAL>a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDeriv 𝕜 (n + 1) f x) m = ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (init m)) (m (last n)) = ((⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F) ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x) m
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>h : AffineIndependent k fun p => ↑p<GOAL>∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>h : AffineIndependent k fun p => ↑p<GOAL>∃ t, ∅ ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Set P<VAR>h : AffineIndependent k fun p => ↑p<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<GOAL>∃ t, s ⊆ t ∧ (AffineIndependent k fun p => ↑p) ∧ affineSpan k t = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing ((⋃₀ 𝔖).restrict ∘ F)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝
<VAR>α β : FinPartOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<VAR>x✝ : (forget FinPartOrd).obj α<GOAL>(↑e ≫ ↑e.symm) x✝ = (𝟙 α) x✝
<VAR>α β : FinPartOrd<VAR>e : ↑α.toPartOrd ≃o ↑β.toPartOrd<VAR>x✝ : (forget FinPartOrd).obj β<GOAL>(↑e.symm ≫ ↑e) x✝ = (𝟙 β) x✝
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<GOAL>Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<GOAL>∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>t : ℝ<VAR>f : AddCircle T → E<GOAL>t ≤ t + T
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M<VAR>inst✝¹⁵ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁸ : AddCommMonoid M'✝<VAR>inst✝⁷ : AddCommMonoid M''<VAR>inst✝⁶ : Module R M'✝<VAR>inst✝⁵ : Module R M''<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : FiniteDimensional K V<VAR>ι : Type u_10<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>B : BilinForm K V<VAR>hB : B.Nondegenerate<VAR>sym : B.IsSymm<VAR>b : Basis ι K V<VAR>i j : ι<GOAL>(B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝² : Fintype β<VAR>inst✝¹ : (b : β) → PseudoMetricSpace (π b)<VAR>inst✝ : Nonempty β<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>ball x r = Set.univ.pi fun b => ball (x b) r
<VAR>R : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k
<VAR>R : Type u_1<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(n.factorization.prod fun p k => (σ 1) (p ^ k)) = ∏ p ∈ n.primeFactors, ∑ k ∈ range (n.factorization p + 1), p ^ k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>U R (n - 1) = 2 * X * U R n - U R (n + 1)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>lieSpan R L s ≤ lieSpan R L t
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>s ⊆ ↑(lieSpan R L t)
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>h : M.IsPerfectMatching<VAR>c : G.ConnectedComponent<GOAL>(M.induce c.supp).IsMatching
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<GOAL>Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s<VAR>a : ℝ<VAR>ha : ‖a‖ ≤ 1<VAR>x : E<VAR>hx : x ∈ s<GOAL>a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s<VAR>a : ℝ<VAR>ha : -1 ≤ a ∧ a ≤ 1<VAR>x : E<VAR>hx : x ∈ s<GOAL>a • x ∈ s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : Set E<VAR>hs : Convex ℝ s<VAR>h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s<VAR>a : ℝ<VAR>ha : -1 ≤ a ∧ a ≤ 1<VAR>x : E<VAR>hx : x ∈ s<GOAL>((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E → 𝕜 → F := fun x t => f (x + t • v)<VAR>hg : Continuous (Function.uncurry g)<GOAL>Measurable fun x => lineDeriv 𝕜 f x v
<VAR>a b : Cardinal.{u_1}<VAR>h : b ≠ 0<GOAL>a ≤ a * b
<VAR>a b : Cardinal.{u_1}<VAR>h : b ≠ 0<GOAL>a ≤ b * a
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>X : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : SMul M X<VAR>t₁ t₂ : TopologicalSpace X<VAR>inst✝¹ : ContinuousSMul M X<VAR>inst✝ : ContinuousSMul M X<GOAL>ContinuousSMul M X
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>X : Type u_3<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : SMul M X<VAR>t₁ t₂ : TopologicalSpace X<VAR>inst✝¹ : ContinuousSMul M X<VAR>inst✝ : ContinuousSMul M X<VAR>b : Bool<GOAL>ContinuousSMul M 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>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<GOAL>Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)
<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>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>ns : ℕ → ℕ<VAR>hns : Tendsto ns atTop atTop<GOAL>∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
<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>inst✝ : IsFiniteMeasure μ<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ<VAR>hg : Memℒp g p μ<VAR>hui : UnifIntegrable f p μ<VAR>hfg : TendstoInMeasure μ f atTop g<VAR>ns : ℕ → ℕ<VAR>hns : Tendsto ns atTop atTop<VAR>ms : ℕ → ℕ<VAR>left✝ : StrictMono ms<VAR>hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))<GOAL>∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>PTendsto' f l₁ l₂ → PTendsto f l₁ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α →. β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>(∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<GOAL>IsMaximal (eraseLast s).last (last s)
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<VAR>this : s.length - 1 + 1 = s.length<GOAL>IsMaximal (eraseLast s).last (last s)
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<VAR>this : s.length - 1 + 1 = s.length<GOAL>IsMaximal (s.toFun ⟨s.length.pred, ⋯⟩) (s.toFun (Fin.last s.length))
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>h : 0 < s.length<VAR>this : s.length - 1 + 1 = s.length<GOAL>Fin.last s.length = ⟨s.length - 1, ⋯⟩.succ
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : NormOneClass A<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : NormOneClass A<VAR>h✝ : IsEmpty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>A : Type u_1<VAR>inst✝² : NormedCommRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : NormOneClass A<VAR>h✝ : Nonempty ι<GOAL>‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : F × E<VAR>hv : x ∈ Submodule.map (LinearEquiv.prodComm R E F) f.graph<VAR>hv' : x.1 = 0<GOAL>x.2 = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>x : F × E<VAR>hv' : x.1 = 0<VAR>hv : ∃ a b, (∃ (h : a ∈ f.domain), ↑f ⟨a, ⋯⟩ = b) ∧ (b, a) = x<GOAL>x.2 = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>a : E<VAR>b : F<VAR>ha : a ∈ f.domain<VAR>h1 : ↑f ⟨a, ⋯⟩ = 0<VAR>hv' : b = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>hf : ∀ (m : ↥f.domain), f.toFun m = 0 → m = 0<VAR>a : E<VAR>b : F<VAR>ha : a ∈ f.domain<VAR>h1 : ↑f ⟨a, ⋯⟩ = 0<VAR>hv' : b = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>a : E<VAR>b : F<VAR>ha : a ∈ f.domain<VAR>h1 : ↑f ⟨a, ⋯⟩ = 0<VAR>hv' : b = 0<VAR>hf : ⟨a, ha⟩ = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f : E →ₗ.[R] F<VAR>a : E<VAR>b : F<VAR>ha : a ∈ f.domain<VAR>h1 : ↑f ⟨a, ⋯⟩ = 0<VAR>hv' : b = 0<VAR>hf : a = 0<GOAL>a = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<GOAL>f ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<GOAL>(f.sum fun n a => C a * X ^ n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<GOAL>(fun n a => C a * X ^ n) n (f.coeff n) ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<GOAL>C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<VAR>this : C (f.coeff n) ∈ p<GOAL>C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<VAR>this✝ : C (f.coeff n) ∈ p<VAR>this : (monomial n) 1 • C (f.coeff n) ∈ p<GOAL>C (f.coeff n) * X ^ n ∈ Ideal.span {g | ∃ i, g = C (f.coeff i)}
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<VAR>this✝ : C (f.coeff n) ∈ p<VAR>this : (monomial n) 1 • C (f.coeff n) ∈ p<GOAL>C (f.coeff n) * X ^ n = (monomial n) 1 • C (f.coeff n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r f : R[X]<VAR>I : Ideal R[X]<VAR>p : Ideal R[X] := Ideal.span {g | ∃ i, g = C (f.coeff i)}<VAR>n : ℕ<VAR>_hn : n ∈ f.support<VAR>this✝ : C (f.coeff n) ∈ p<VAR>this : (monomial n) 1 • C (f.coeff n) ∈ p<GOAL>C (f.coeff n) * X ^ n = (monomial n) (f.coeff n)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<VAR>hG : IsCoseparator G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (h : Y ⟶ G), f ≫ h = 0<GOAL>∀ (h : Y ⟶ G), f ≫ h = 0 ≫ h