ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>m : ↥(B.orthogonal (Submodule.span K {x}))<VAR>hm : ∀ (n : ↥(B.orthogonal (Submodule.span K {x}))), ((B.restrict (B.orthogonal (Submodule.span K {x}))) m) n = 0<VAR>y : V<VAR>hy : y ∈ Submodule.span K {x}<VAR>z : V<VAR>hz : z ∈ B.orthogonal (Submodule.span K {x})<VAR>this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})<GOAL>(B ↑m) (y + z) = 0
<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>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝¹ : AddCommMonoid M₂'<VAR>inst✝ : Module R M₂'<VAR>B : BilinForm K V<VAR>b₁ : B.Nondegenerate<VAR>b₂ : B.IsRefl<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<VAR>m : ↥(B.orthogonal (Submodule.span K {x}))<VAR>y : V<VAR>hy : y ∈ Submodule.span K {x}<VAR>z : V<VAR>hz : z ∈ B.orthogonal (Submodule.span K {x})<VAR>this : y + z ∈ Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x})<VAR>hm : ((domRestrict₁₂ B (B.orthogonal (Submodule.span K {x})) (B.orthogonal (Submodule.span K {x}))) m) ⟨z, hz⟩ = 0<GOAL>(B ↑m) (y + z) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<GOAL>rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝²¹ : CommRing R<VAR>inst✝²⁰ : CommRing S<VAR>inst✝¹⁹ : Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ✝ : Type u_4<VAR>inst✝¹⁸ : CommRing Rₘ<VAR>inst✝¹⁷ : Algebra R Rₘ<VAR>inst✝¹⁶ : CommRing Sₘ✝<VAR>inst✝¹⁵ : Algebra S Sₘ✝<VAR>M : Submonoid R<VAR>inst✝¹⁴ : IsLocalization M Rₘ<VAR>inst✝¹³ : IsLocalization (algebraMapSubmonoid S M) Sₘ✝<VAR>inst✝¹² : Algebra Rₘ Sₘ✝<VAR>inst✝¹¹ : Algebra R Sₘ✝<VAR>inst✝¹⁰ : IsScalarTower R Rₘ Sₘ✝<VAR>inst✝⁹ : IsScalarTower R S Sₘ✝<VAR>Sₘ : Type u_5<VAR>inst✝⁸ : CommRing Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : Algebra R Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<GOAL>discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (discr R ⇑b)
<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 : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ ∃ f', ContDiff 𝕜 (↑n) f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>e : X ≃ᵈ X<VAR>n : ℕ<GOAL>⇑(e ^ n) = (⇑e)^[n]
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>e : X ≃ᵈ X<VAR>n : ℕ<GOAL>(⇑(toPerm e))^[n] = (⇑e)^[n]
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>u : Set δ<VAR>inst✝ : MeasureSpace δ<VAR>p : δ → Prop<VAR>hu : NullMeasurableSet u volume<GOAL>volume univ = volume u
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>u : Set δ<VAR>inst✝ : MeasureSpace δ<VAR>p : δ → Prop<VAR>hu : NullMeasurableSet u volume<GOAL>volume (Subtype.val '' univ) = volume u
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>u : Set δ<VAR>inst✝ : MeasureSpace δ<VAR>p : δ → Prop<VAR>hu : NullMeasurableSet u volume<GOAL>Injective Subtype.val
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>u : Set δ<VAR>inst✝ : MeasureSpace δ<VAR>p : δ → Prop<VAR>hu : NullMeasurableSet u volume<GOAL>∀ (s : Set { x // x ∈ u }), MeasurableSet s → NullMeasurableSet (Subtype.val '' s) volume
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ z₁' : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>((z₁ + z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h + z₁'.comp z₂ h).v p q hpq
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t A B : Set β<VAR>a✝ : α<VAR>x : β<VAR>a : α<VAR>s : Set α<VAR>x✝ : α<GOAL>x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)<VAR>g' : ℕ → β<VAR>g : ℕ → α<VAR>hgs : ∀ (n : ℕ), g n ∈ s<VAR>heq : ∀ (n : ℕ), f (g n) = g' n<GOAL>∃ m n, m < n ∧ r' (g' m) (g' n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>hs : s.PartiallyWellOrderedOn r<VAR>hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)<VAR>g : ℕ → α<VAR>hgs : ∀ (n : ℕ), g n ∈ s<VAR>heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n<GOAL>∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>ha : G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - ℓ
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>v w : V<VAR>h : G.IsSRGWith n k ℓ μ<VAR>ha : G.Adj v w<GOAL>(G.neighborFinset v ∪ G.neighborFinset w).card = 2 * k - Fintype.card ↑(G.commonNeighbors v w)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed (C1 C ho)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<GOAL>IsClosed {f | f (term I ho) = true}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>h : Continuous fun f => f (term I ho)<GOAL>IsClosed {f | f (term I ho) = true}
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a⁻¹ * a ≠ ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).PreservesMonomorphisms<GOAL>MorphismProperty.injective C = monomorphisms C
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : (forget C).PreservesMonomorphisms<GOAL>(forget C).PreservesMonomorphisms
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>IH4 x₁ x₂ y → IH4 (-x₂) (-x₁) y ∧ IH4 x₁ x₂ (-y)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<GOAL>(∀ ⦃z w : PGame⦄, w.IsOption y → (z.IsOption x₁ → P2 z x₂ w) ∧ (z.IsOption x₂ → P2 x₁ z w)) → (∀ ⦃z w : PGame⦄, w.IsOption y → ((-z).IsOption x₂ → P2 z (-x₁) w) ∧ ((-z).IsOption x₁ → P2 (-x₂) z w)) ∧ ∀ ⦃z w : PGame⦄, (-w).IsOption y → (z.IsOption x₁ → P2 z x₂ w) ∧ (z.IsOption x₂ → P2 x₁ z w)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝¹³ : CommRing K<VAR>inst✝¹² : CommRing L<VAR>inst✝¹¹ : CommRing M<VAR>inst✝¹⁰ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁹ : ExpChar K p<VAR>inst✝⁸ : ExpChar L p<VAR>inst✝⁷ : ExpChar M p<VAR>inst✝⁶ : ExpChar N p<VAR>inst✝⁵ : PerfectRing L p<VAR>inst✝⁴ : IsPerfectClosure i p<VAR>inst✝³ : PerfectRing M p<VAR>inst✝² : IsPerfectClosure j p<VAR>inst✝¹ : PerfectRing N p<VAR>inst✝ : IsPerfectClosure k p<VAR>x : L<GOAL>(equiv j i p) ((equiv i j p) x) = x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : NonAssocRing α<VAR>a b : α<VAR>n✝ : ℤ<VAR>n : ℕ<VAR>x : α<GOAL>Commute (↑↑n) x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : NonAssocRing α<VAR>a b : α<VAR>n✝ : ℤ<VAR>n : ℕ<VAR>x : α<GOAL>Commute (↑-[n+1]) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>s : Set α<VAR>μ : Measure α<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C<GOAL>(μ.restrict s) univ < ⊤
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))
<VAR>a : UnitAddCircle<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))<GOAL>Tendsto (fun s => s * completedCosZeta a s) (𝓝[≠] 0) (𝓝 (-1))
<VAR>a : UnitAddCircle<VAR>h1 : Tendsto (fun s => s * (hurwitzEvenFEPair a).symm.Λ s) (𝓝[≠] 0) (𝓝 (-1))<VAR>s : ℂ<GOAL>((fun s => s * (hurwitzEvenFEPair a).symm.Λ s) ∘ fun s => s / 2) s = s * completedCosZeta a s
<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>hfi : HasFiniteIntegral f μ<GOAL>HasFiniteIntegral (fun a => ‖f a‖) μ
<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>hfi : HasFiniteIntegral f μ<VAR>eq : (fun a => ↑‖‖f a‖‖₊) = fun a => ↑‖f a‖₊<GOAL>HasFiniteIntegral (fun a => ‖f a‖) μ
<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>x : E<VAR>h : HasFPowerSeriesAt 0 p x<VAR>n : ℕ<GOAL>∀ (y : E), ((p n) fun x => y) = 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>x : E<VAR>h : HasFPowerSeriesAt 0 p x<VAR>n k : ℕ<VAR>hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0<GOAL>∀ (y : E), ((p k) fun x => y) = 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>x : E<VAR>h : HasFPowerSeriesAt 0 p x<VAR>n k : ℕ<VAR>hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0<VAR>psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y<GOAL>∀ (y : E), ((p k) fun x => y) = 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>x : E<VAR>n k : ℕ<VAR>hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0<VAR>psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y<VAR>h : (fun y => 0 (x + y) - p.partialSum k.succ y) =O[𝓝 0] fun y => ‖y‖ ^ k.succ<GOAL>∀ (y : E), ((p k) fun x => y) = 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>x : E<VAR>n k : ℕ<VAR>hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0<VAR>psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y<VAR>h : (fun x => (p k) fun x_1 => x) =O[𝓝 0] fun y => ‖y‖ ^ k.succ<GOAL>∀ (y : E), ((p k) fun x => y) = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>F.interUnionPullbackConeLift U V s ≫ F.val.map (homOfLE ⋯).op = s.fst
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>⋯.some.lift { pt := s.pt, π := { app := fun X_1 => Opposite.casesOn X_1 fun unop => Pairwise.casesOn unop (fun a => ULift.casesOn a fun down => WalkingPair.casesOn down s.fst s.snd) fun a a_1 => ULift.casesOn a fun down => WalkingPair.casesOn down (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op), naturality := ⋯ } } ≫ F.val.map (eqToHom ⋯).op ≫ F.val.map (homOfLE ⋯).op = s.fst
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>U V : Opens ↑X<VAR>s : PullbackCone (F.val.map (homOfLE ⋯).op) (F.val.map (homOfLE ⋯).op)<GOAL>⋯.some.lift { pt := s.pt, π := { app := fun X_1 => Pairwise.rec (fun a => WalkingPair.rec s.fst s.snd a.down) (fun a a_1 => WalkingPair.rec (s.fst ≫ F.val.map (homOfLE ⋯).op) (s.snd ≫ F.val.map (homOfLE ⋯).op) a.down) (unop X_1), naturality := ⋯ } } ≫ F.val.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) = s.fst
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : NonUnitalNonAssocSemiring A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : NonUnitalNonAssocSemiring C<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R B<VAR>inst✝ : Module R C<VAR>S T : NonUnitalSubalgebra R A<VAR>h : S.toNonUnitalSubsemiring = T.toNonUnitalSubsemiring<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NonUnitalNormedRing A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : SMulCommClass 𝕜 A A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.2‖ = ‖a‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α ↪ β<GOAL>(M.mapEmbedding f).Base (⇑f '' B)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<VAR>hB : M.Base B<VAR>f : α ↪ β<GOAL>∃ B₀, M.Base B₀ ∧ ⇑f '' B = ⇑f '' B₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<VAR>o : Option α<VAR>a m✝ hd : α<VAR>tl : List α<VAR>m : α<GOAL>m ∈ argmax f (hd :: tl) → m ∈ hd :: tl
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>hf : (s.formPerm hs).IsCycle<VAR>hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s<GOAL>∃! s_1, (↑s_1).formPerm ⋯ = s.formPerm hs
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩<GOAL>↑↑f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩<VAR>hf_f_meas : ↑↑f =ᶠ[ae μ] ↑↑↑f_meas<GOAL>↑↑f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩<VAR>hf_f_meas : ↑↑f =ᶠ[ae μ] ↑↑↑f_meas<GOAL>↑↑↑f_meas =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩<VAR>hf_f_meas : ↑↑f =ᶠ[ae μ] ↑↑↑f_meas<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f_meas) s μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = 0<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>f_meas : ↥(lpMeas E' 𝕜 m p μ) := ⟨f, hf_meas⟩<VAR>hf_f_meas : ↑↑f =ᶠ[ae μ] ↑↑↑f_meas<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f_meas x ∂μ = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.f i = i'<VAR>h : ∃ i, e.f i = i'<GOAL>e.r i' = some i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.f i = i'<VAR>h : ∃ i, e.f i = i'<VAR>this : h.choose = i<GOAL>e.r i' = some i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>e : c.Embedding c'<VAR>i : ι<VAR>i' : ι'<VAR>hi : e.f i = i'<VAR>h : ∃ i, e.f i = i'<VAR>this : h.choose = i<GOAL>(if h : ∃ i, e.f i = i' then some h.choose else none) = some i
<VAR>f : ℂ[X]<VAR>hf : 0 < f.degree<GOAL>∃ z, f.IsRoot z
<VAR>f : ℂ[X]<VAR>hf : 0 < f.degree<VAR>hf' : ∀ (z : ℂ), ¬f.IsRoot z<GOAL>False
<VAR>f : ℂ[X]<VAR>hf : 0 < f.degree<VAR>hf' : ∀ (z : ℂ), ¬f.IsRoot z<VAR>this : ∀ (z : ℂ), (eval z f)⁻¹ = 0<GOAL>False
<VAR>hf : 0 < (C 0).degree<VAR>hf' : ∀ (z : ℂ), ¬(C 0).IsRoot z<VAR>this : ∀ (z : ℂ), (eval z (C 0))⁻¹ = 0<GOAL>False
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<GOAL>levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<GOAL>∀ (ε : ℝ≥0∞) (B : Set Ω), 0 < ε → ε < ⊤ → MeasurableSet B → μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε