ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x h h' : (i : ι) → M₁ i<GOAL>f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') = ∑ s ∈ filter (fun x => 2 ≤ x.card) Finset.univ.powerset, (f (s.piecewise h x) - f (s.piecewise h' x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : a * b = 1<GOAL>Tendsto (fun x => x * a) (cocompact M) (cocompact M)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : a * b = 1<GOAL>Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>a b : M<VAR>ha : a * b = 1<GOAL>Tendsto (fun x => x) (cocompact M) (cocompact M)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys₂ ≤ levenshtein C xs (ys₁ ++ ys₂)
<VAR>q : ℍ<VAR>hq : q.re = 0<GOAL>exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<GOAL>(fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q
<VAR>q : ℍ<VAR>hq : q.re = 0<GOAL>HasSum (fun n => (↑n !)⁻¹ • q ^ n) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)
<VAR>q : ℍ<VAR>hq : q.re = 0<GOAL>HasSum (fun n => (expSeries ℝ ℍ n) fun x => q) (↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>x✝ : ↥(torsion G)<VAR>x : G<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1<GOAL>↑((fun x_1 => ⟨x, ⋯⟩ * x_1)^[n] 1) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>x✝ : ↥(torsion G)<VAR>x : G<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1<GOAL>↑((fun x_1 => ⟨x, ⋯⟩ ^ n * x_1) 1) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : CommMonoid G<VAR>x✝ : ↥(torsion G)<VAR>x : G<VAR>n : ℕ<VAR>npos : n > 0<VAR>hn : Function.IsPeriodicPt (fun x_1 => x * x_1) n 1<GOAL>↑(⟨x, ⋯⟩ ^ n) * 1 = 1
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<GOAL>IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑n = 1}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hJ : M.Basis J X<VAR>hIJ : I \ J = {e}<GOAL>∃ f ∈ J \ I, J = insert f I \ {e}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : (M ↾ X).Base I<VAR>hJ : (M ↾ X).Base J<VAR>hIJ : I \ J = {e}<GOAL>∃ f ∈ J \ I, J = insert f I \ {e}
<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>s : Multiset α<VAR>a : α<VAR>comm : {x | x ∈ a ::ₘ s}.Pairwise Commute<GOAL>(a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a
<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>a : α<VAR>s : List α<VAR>comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute<GOAL>(a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
<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>a : α<VAR>s : List α<VAR>comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute<GOAL>a * s.prod = s.prod * a
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<GOAL>#(α → α) ≤ #(α ≃ α)
<VAR>α β : Type u<VAR>β' : Type v<VAR>inst✝ : Infinite α<GOAL>Nonempty ((α → Bool) ↪ Perm (α × Bool))
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>sphere x ε ∪ ball x ε = closedBall x ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>∀ᵐ (b : β) ∂Measure.map X μ, Integrable (fun ω => f (b, ω)) ((condDistrib Y X μ) b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>∀ᵐ (b : β) ∂(Measure.map (fun a => (X a, Y a)) μ).fst, Integrable (fun ω => f (b, ω)) ((Measure.map (fun a => (X a, Y a)) μ).condKernel b)
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a : R<GOAL>(if a0 : a = 0 then 0 else let_fun x := ⋯; gcd (0 % a) a) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : BEq α<VAR>a : α<VAR>l : AssocList α β<GOAL>find? a l = Option.map (fun x => x.snd) (List.find? (fun x => x.fst == a) l.toList)
<VAR>M : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>A : Type u_4<VAR>inst✝ : CommMonoid A<VAR>a b c : A<GOAL>c ∈ closure {a, b} ↔ ∃ m n, a ^ m * b ^ n = c
<VAR>M : Type u_1<VAR>A✝ : Type u_2<VAR>B : Type u_3<VAR>A : Type u_4<VAR>inst✝ : CommMonoid A<VAR>a b c : A<GOAL>(∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 1<GOAL>∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 1<GOAL>∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 1<VAR>x : α<VAR>hx : x ∈ s<VAR>hnx : x ∉ s \ {a}<GOAL>f x = 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → β<VAR>a : α<VAR>h : f a = 1<VAR>x : α<VAR>hx : x ∈ s<VAR>hnx : x ∉ s.erase a<GOAL>f x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>fst✝¹ snd✝¹ fst✝ snd✝ : α<GOAL>s(fst✝¹, snd✝¹) = s(fst✝, snd✝) ↔ (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = (fst✝, snd✝).swap
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>1 = span R {1}
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<GOAL>∀ (x : A), x ∈ 1 ↔ x ∈ span R {1}
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n a : A<GOAL>a ∈ 1 ↔ a ∈ span R {1}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>hm : m ≤ m0<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (↑g * f) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝ : MeasurableSpace X<VAR>f : X → ℝ<VAR>m m0 : MeasurableSpace X<VAR>μ : Measure X<VAR>hm : m ≤ m0<VAR>g : SimpleFunc X ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (↑(SimpleFunc.toLargerSpace hm g) * f) μ
<VAR>m n✝ : ℕ<VAR>a : Fin (n✝ + 1 + 1)<VAR>h : ¬a = 0<GOAL>↑(a - 1) = ↑a - 1
<VAR>m n✝ : ℕ<VAR>a : Fin (n✝ + 1 + 1)<VAR>h : ¬a = 0<GOAL>n✝ + 1 + 1 ≤ ↑a + (n✝ + 1)
<VAR>m n✝ : ℕ<VAR>a : Fin (n✝ + 1 + 1)<VAR>h : ¬a = 0<GOAL>n✝ + 1 + 1 ≤ n✝ + 1 + ↑a
<VAR>m n✝ : ℕ<VAR>a : Fin (n✝ + 1 + 1)<VAR>h : ¬a = 0<GOAL>↑a ≠ 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>ε ≤ ↑|G.edgeDensity (⋯.choose, ⋯.choose).1 (⋯.choose, ⋯.choose).2 - G.edgeDensity s t|
<VAR>x✝ y z x : ℝ<GOAL>0 ^ x ≤ 1
<VAR>M : Type u_1<VAR>inst✝¹⁵ : Monoid M<VAR>N : Type u_2<VAR>inst✝¹⁴ : Monoid N<VAR>P : Type u_3<VAR>inst✝¹³ : Monoid P<VAR>φ : M →* N<VAR>φ' : N →* M<VAR>ψ : N →* P<VAR>χ : M →* P<VAR>A : Type u_4<VAR>inst✝¹² : AddMonoid A<VAR>inst✝¹¹ : DistribMulAction M A<VAR>B : Type u_5<VAR>inst✝¹⁰ : AddMonoid B<VAR>inst✝⁹ : DistribMulAction N B<VAR>B₁ : Type u_6<VAR>inst✝⁸ : AddMonoid B₁<VAR>inst✝⁷ : DistribMulAction M B₁<VAR>C : Type u_7<VAR>inst✝⁶ : AddMonoid C<VAR>inst✝⁵ : DistribMulAction P C<VAR>A' : Type u_8<VAR>inst✝⁴ : AddGroup A'<VAR>inst✝³ : DistribMulAction M A'<VAR>B' : Type u_9<VAR>inst✝² : AddGroup B'<VAR>inst✝¹ : DistribMulAction N B'<VAR>F : Type u_10<VAR>inst✝ : FunLike F A B<VAR>f : A →ₑ+[φ] B<VAR>x : A<GOAL>(f.comp (DistribMulActionHom.id M)) x = f x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ioo ⊥ ↑a = Iio a
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>l : IntegrationParams<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<GOAL>HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<GOAL>∫ (x : ι → ℝ) in ↑I, f x ∂μ = y
<VAR>ι : Type u<VAR>E : Type v<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f : (ι → ℝ) → E<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>I : Box ι<VAR>hc : ContinuousOn f (Box.Icc I)<VAR>l : IntegrationParams<VAR>y : E<VAR>hy : HasIntegral I l f μ.toBoxAdditive.toSMul y<VAR>this : IntegrableOn f (↑I) μ<GOAL>∫ (x : ι → ℝ) in ↑I, f x ∂μ = y
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>f : M →ₗ[R] M'<VAR>hv : LinearIndependent R (⇑f ∘ v)<GOAL>Disjoint (span R (range v)) (LinearMap.ker f)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>f : M →ₗ[R] M'<VAR>hv : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥<GOAL>Disjoint (span R (range v)) (LinearMap.ker f)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<GOAL>(if 0 = 0 then {i | ¬f i = 0}.Finite else Summable fun i => ‖f i‖ ^ 0) ↔ {i | ¬f i = 0}.Finite
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : PartialOrder α<VAR>a b c d : α<VAR>inst✝ : MulPosStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a < b * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝² : Semiring α<VAR>inst✝¹ : PartialOrder α<VAR>a b c d : α<VAR>inst✝ : MulPosStrictMono α<VAR>hn : 0 < a<VAR>hm : 1 < b<GOAL>a = 1 * a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<GOAL>x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : Quotient.mk'' f ≠ 0<GOAL>‖Quotient.mk'' f‖ = ↑p ^ (-valuation (Quotient.mk'' f))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : Quotient.mk'' f ≠ 0<GOAL>↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : Quotient.mk'' f ≠ 0<GOAL>↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℚ_[p]<VAR>f : CauSeq ℚ (padicNorm p)<VAR>hf : Quotient.mk'' f ≠ 0<GOAL>¬f ≈ 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>f_add : ∀ (a b : R), f (a + b) ≤ f a + f b<VAR>x y : R<GOAL>seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>f_add : ∀ (a b : R), f (a + b) ≤ f a + f b<VAR>x y z : R<GOAL>f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>f_add : ∀ (a b : R), f (a + b) ≤ f a + f b<VAR>x y z : R<GOAL>f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>m : Sym2 α<GOAL>m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Finset α<VAR>a b : α<VAR>m : Sym2 α<GOAL>(∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>h : Summable fun n => dist (f n) (f n.succ)<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>‖toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>(if 1 = ⊤ then eLpNormEssSup f μ else ∫⁻ (a : α), ↑‖f a‖₊ ∂μ).toReal = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>F G : Ultrafilter α<VAR>x : α<VAR>hF : ↑F ≤ 𝓝 x<VAR>hG : ↑G ≤ 𝓝 x<GOAL>Ultrafilter.extend g F = Ultrafilter.extend g G
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>F G : Ultrafilter α<VAR>x : α<VAR>hG : ↑G ≤ 𝓝 x<VAR>hF : map g ↑F ≤ 𝓝 (g x)<GOAL>Ultrafilter.extend g F = Ultrafilter.extend g G
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>F G : Ultrafilter α<VAR>x : α<VAR>hF : map g ↑F ≤ 𝓝 (g x)<VAR>hG : map g ↑G ≤ 𝓝 (g x)<GOAL>Ultrafilter.extend g F = Ultrafilter.extend g G
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : Karoubi C<VAR>f : P.Hom Q<GOAL>P.p ≫ f.f = f.f ≫ Q.p
<VAR>x y : ℝ<VAR>f : Cauchy abs<GOAL>(Real.inv' { cauchy := f }).cauchy = { cauchy := f }.cauchy⁻¹
<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✝⁷ : CommRing R<VAR>inst✝⁶ : (i : ι) → AddCommGroup (Mᵢ i)<VAR>inst✝⁵ : (i : ι) → AddCommGroup (Nᵢ i)<VAR>inst✝⁴ : AddCommGroup P<VAR>inst✝³ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝² : (i : ι) → Module R (Nᵢ i)<VAR>inst✝¹ : Module R P<VAR>inst✝ : Fintype ι<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<VAR>x y : (i : ι) → Mᵢ i<GOAL>(pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i : ι, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Surjective f<VAR>s : Set X<GOAL>μH[d] (f '' s) = μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Surjective f<VAR>s : Set X<GOAL>((OuterMeasure.comap f) (OuterMeasure.mkMetric fun r => r ^ d)) s = (OuterMeasure.mkMetric fun r => r ^ d) s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>f : X → Y<VAR>d : ℝ<VAR>hf : Isometry f<VAR>hd : 0 ≤ d ∨ Surjective f<VAR>s : Set X<GOAL>0 ≤ d → Monotone fun r => r ^ d
<VAR>m n a b c d : ℤ<VAR>h₁ : a ≡ b [ZMOD n]<VAR>h₂ : a + c ≡ b + d [ZMOD n]<VAR>this : d - c = b + d - (a + c) - (b - a)<GOAL>n ∣ b + d - (a + c) - (b - a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : T2Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddCommGroup α<VAR>inst✝ : Neg β<VAR>h : Antiperiodic f c<VAR>a : α<GOAL>Antiperiodic (fun x => f (x - a)) c
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l : List ι<VAR>nod : Multiset.Nodup (Quot.mk Setoid.r l)<VAR>hs : ∀ i ∈ Quot.mk Setoid.r l, s i ≠ 0<VAR>pp : {x | x ∈ Quot.mk Setoid.r l}.Pairwise (Coprime on s)<GOAL>↑(Quotient.recOn (motive := fun x => x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] }) (Quot.mk Setoid.r l) (fun l nod x co => chineseRemainderOfList a s l ⋯) ⋯ nod hs pp) < (Multiset.map s (Quot.mk Setoid.r l)).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>l : List α<VAR>f : α → β<GOAL>∏ i : Fin l.length, f l[↑i] = (List.map f l).prod
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f' : Y ≃ₜ Z<VAR>f'' : Z ≃ₜ Z'<GOAL>(e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')
<VAR>N✝ : ℕ<VAR>H K : Subgroup SL(2, ℤ)<VAR>h : H ≤ K<VAR>N : ℕ+<VAR>hN : Gamma ↑N ≤ H<GOAL>IsCongruenceSubgroup K
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>u : Rˣ<GOAL>u⁻¹ = u ↔ u = 1 ∨ u = -1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>u : Rˣ<GOAL>u * u = 1 ↔ u = 1 ∨ u = -1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>u : Rˣ<GOAL>↑(u * u) = ↑1 ↔ ↑u = ↑1 ∨ ↑u = ↑(-1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>u : Rˣ<GOAL>↑u * ↑u = 1 ↔ ↑u = 1 ∨ ↑u = -1
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_5, u_2} D<VAR>E : Type u_3<VAR>inst✝¹ : Category.{?u.5419, u_3} E<VAR>J : GrothendieckTopology C<VAR>K✝ : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>G : C ⥤ D<VAR>K : GrothendieckTopology D<VAR>inst✝ : G.IsCoverDense K<VAR>U : D<GOAL>Sieve.coverByImage G U ∈ K.sieves U
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f✝ : X✝ → Y✝<VAR>g : Y✝ → Z<VAR>X : ι → Type u_6<VAR>Y : ι → Type u_7<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X i)<VAR>inst✝ : (i : ι) → TopologicalSpace (Y i)<VAR>f : (i : ι) → X i → Y i<VAR>h : ∀ (i : ι), IsProperMap (f i)<GOAL>IsProperMap fun x i => f i (x i)
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : TopologicalSpace X✝<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>f✝ : X✝ → Y✝<VAR>g : Y✝ → Z<VAR>X : ι → Type u_6<VAR>Y : ι → Type u_7<VAR>inst✝¹ : (i : ι) → TopologicalSpace (X i)<VAR>inst✝ : (i : ι) → TopologicalSpace (Y i)<VAR>f : (i : ι) → X i → Y i<VAR>h : ∀ (i : ι), Continuous (f i) ∧ ∀ ⦃𝒰 : Ultrafilter (X i)⦄ ⦃y : Y i⦄, Tendsto (f i) (↑𝒰) (𝓝 y) → ∃ x, f i x = y ∧ ↑𝒰 ≤ 𝓝 x<GOAL>(Continuous fun x i => f i (x i)) ∧ ∀ ⦃𝒰 : Ultrafilter ((i : ι) → X i)⦄ ⦃y : (i : ι) → Y i⦄, Tendsto (fun x i => f i (x i)) (↑𝒰) (𝓝 y) → ∃ x, (fun i => f i (x i)) = y ∧ ↑𝒰 ≤ 𝓝 x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r : R<VAR>h : r ≠ 0<GOAL>C r ≠ 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r : R<VAR>h : C r = 0<GOAL>r = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonAssocSemiring R<VAR>r : R<VAR>h : C r = C 0<GOAL>r = 0
<VAR>q₁ q₂ : ℚ<GOAL>(q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))