ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LE G<VAR>inst✝² : Preorder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>a b : G<VAR>c d : P<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d ∧ ¬d ≤ c<VAR>hbdc : b • d ≤ b • c<VAR>h : d ≤ c<GOAL>False
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>n : R[X]<VAR>d : ↥R[X]⁰<GOAL>(map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : MonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>hφ : R[X]⁰ ≤ Submonoid.comap φ S[X]⁰<VAR>n : R[X]<VAR>d : ↥R[X]⁰<GOAL>(if h : φ ↑d ∈ S[X]⁰ then { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, h⟩ } else 0) = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>s : Set X<GOAL>𝓝[s \ {y}] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>s : Set X<GOAL>{y}ᶜ ∈ 𝓝[s] x
<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<GOAL>ContDiffOn 𝕜 0 f s ↔ ContinuousOn f s
<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>H : ContinuousOn f s<GOAL>ContDiffOn 𝕜 0 f s
<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>H : ContinuousOn f s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<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>H : ContinuousOn f s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<VAR>this : ↑m = 0<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<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>H : ContinuousOn f s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<VAR>this : ↑m = 0<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn 0 f p u
<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>H : ContinuousOn f s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<VAR>this : ↑m = 0<GOAL>HasFTaylorSeriesUpToOn 0 f (ftaylorSeriesWithin 𝕜 f s) (insert x s)
<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>H : ContinuousOn f s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ 0<VAR>this : ↑m = 0<GOAL>ContinuousOn f (insert x s) ∧ ∀ x_1 ∈ insert x s, (ftaylorSeriesWithin 𝕜 f s x_1 0).uncurry0 = f x_1
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<GOAL>Squarefree n ↔ n.minSqFac = none
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>this : n.MinSqFacProp n.minSqFac<GOAL>Squarefree n ↔ n.minSqFac = none
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℝ≥0∞<VAR>hf : ∀ i ∈ s, f i ≠ ⊤<VAR>r : ℝ<GOAL>∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hfg : range f = range g<VAR>b : β<VAR>H : ∀ a < b, f a = g a<GOAL>f b ≤ g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hfg : range f = range g<VAR>b : β<VAR>H : ∀ a < b, f a = g a<VAR>c : β<VAR>hc : f c = g b<GOAL>f b ≤ g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hfg : range f = range g<VAR>b : β<VAR>H : ∀ a < b, f a = g a<VAR>c : β<VAR>hc : f c = g b<VAR>hcb : c < b<GOAL>f b ≤ g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r r' : α → α → Prop<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : PartialOrder γ<VAR>f g : β → γ<VAR>hf : StrictMono f<VAR>hg : StrictMono g<VAR>hfg : range f = range g<VAR>b : β<VAR>H : ∀ a < b, f a = g a<VAR>c : β<VAR>hc : f c = g b<VAR>hbc : b ≤ c<GOAL>f b ≤ g b
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((of R).symm y).support ⊆ s<GOAL>((of R).symm (x • y)).coeff a = ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((of R).symm y).support ⊆ s<GOAL>∑ ij ∈ VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((of R).symm y).coeff ij.2 = ∑ ij ∈ VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((of R).symm y).support ⊆ s<GOAL>∀ x_1 ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a, x.coeff x_1.1 • ((of R).symm y).coeff x_1.2 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((of R).symm y).support ⊆ s<VAR>b : Γ × Γ'<VAR>hb : b ∈ VAddAntidiagonal ⋯ hs a \ VAddAntidiagonal ⋯ ⋯ a<GOAL>x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : Zero R<VAR>inst✝¹ : AddCommMonoid V<VAR>inst✝ : SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((of R).symm y).support ⊆ s<VAR>b : Γ × Γ'<VAR>hb : (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧ (x.coeff b.1 ≠ 0 → b.1 +ᵥ b.2 = a → ((of R).symm y).coeff b.2 = 0)<GOAL>x.coeff b.1 • ((of R).symm y).coeff b.2 = 0
<VAR>n : Nat<GOAL>range n = [] ↔ n = 0
<VAR>n : ℕ<VAR>a : Fin n<VAR>x : ℕ<GOAL>x ∈ map valEmbedding (Ici a) ↔ x ∈ Icc (↑a) (n - 1)
<VAR>n : ℕ<VAR>a : Fin n<VAR>x : ℕ<GOAL>(∃ a_1, a ≤ a_1 ∧ valEmbedding a_1 = x) ↔ ↑a ≤ x ∧ x ≤ n - 1
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousAt (f i) x<GOAL>LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>ι : Type u_3<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x<GOAL>LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Bijective f<VAR>g : α → γ<GOAL>(fun g => g ∘ f) (g ∘ surjInv ⋯) = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Mul α<VAR>x y : WithZero α<VAR>hxy : x * y ≠ 0<GOAL>unzero hxy = unzero ⋯ * unzero ⋯
<VAR>α : Type u_1<VAR>inst✝³ : AddGroup α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>sign (-a) = -sign a
<VAR>α : Type u_1<VAR>inst✝³ : AddGroup α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>(if a < 0 then 1 else if 0 < a then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>a : Ordinal.{u}<VAR>ha : ∀ b < o, (beth b).ord ≤ a<GOAL>(beth o).ord ≤ a
<VAR>o : Ordinal.{u}<VAR>ho : o.IsLimit<VAR>a : Ordinal.{u}<VAR>ha : ∀ b < o, (beth b).ord ≤ a<GOAL>⨆ a, beth ↑a ≤ a.card
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → α → β<VAR>s t : Finset α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>image2 f (↑s ∪ ↑t) (↑s ∩ ↑t) ⊆ image2 f ↑s ↑t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝¹ : R →+* S<VAR>f✝ : R →+* B<VAR>f : R →+* S<VAR>x : B<VAR>n : ℕ<VAR>hn : 0 < n<VAR>p : R[X]<VAR>hmonic : p.Monic<VAR>heval : eval₂ (algebraMap R B) (x ^ n) p = 0<GOAL>IsIntegral R x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁸ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁷ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : ContinuousNeg E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>hf : StronglyMeasurable f<GOAL>Measurable (g - f)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁸ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁷ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : ContinuousAdd E<VAR>inst✝¹ : ContinuousNeg E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>hf : StronglyMeasurable f<GOAL>Measurable (g + -f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrable f μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set X<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_union : univ ⊆ ⋃ n, u n<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrable f μ<VAR>u : ℕ → Set X<VAR>u_open : ∀ (n : ℕ), IsOpen (u n)<VAR>u_union : univ ⊆ ⋃ n, u n<VAR>hu : ∀ (n : ℕ), IntegrableOn f (u n ∩ univ) μ<VAR>n : ℕ<GOAL>IntegrableOn f (u n) μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<GOAL>∃! s, ∃ (h : s.Nodup), s.formPerm h = f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>val✝ : Fintype α<GOAL>∃! s, ∃ (h : s.Nodup), s.formPerm h = f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>val✝ : Fintype α<VAR>x : α<VAR>hx : f x ≠ x<VAR>hy : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<GOAL>∃! s, ∃ (h : s.Nodup), s.formPerm h = f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>val✝ : Fintype α<VAR>x : α<VAR>hx : f x ≠ x<VAR>hy : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<GOAL>(↑(f.toList x)).formPerm ⋯ = f
<VAR>α : Type u_1<VAR>inst✝¹ : Finite α<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hf : f.IsCycle<VAR>val✝ : Fintype α<VAR>x : α<VAR>hx : f x ≠ x<VAR>hy : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<GOAL>∀ (y : Cycle α), (fun s => ∃ (h : s.Nodup), s.formPerm h = f) y → y = ↑(f.toList x)
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>ψ θ : R ⧸ AddSubgroup.zmultiples p<VAR>n : ℕ<VAR>hz : n ≠ 0<GOAL>n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>ψ θ : R ⧸ AddSubgroup.zmultiples p<VAR>n : ℕ<VAR>hz : n ≠ 0<GOAL>(∃ k, ψ = θ + ↑(↑k • (p / ↑n))) ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
<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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>h : HasFiniteIntegral f μ<VAR>s : Set α<GOAL>HasFiniteIntegral f (μ.restrict 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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>h : HasFiniteIntegral f μ<VAR>s : Set α<GOAL>∫⁻ (a : α) in s, ↑‖f a‖₊ ∂μ ≤ ∫⁻ (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>E : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>h : HasFiniteIntegral f μ<VAR>s : Set α<GOAL>μ = μ.restrict univ
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b✝ b : R<GOAL>gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a b✝ b : R<GOAL>b ∣ 0 ∧ b ∣ b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a✝ b✝ a b : R<VAR>x✝¹ : a ≠ 0<VAR>x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a<VAR>IH₁ : gcd (b % a) a ∣ b % a<VAR>IH₂ : gcd (b % a) a ∣ a<GOAL>gcd a b ∣ a ∧ gcd a b ∣ b
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>a✝ b✝ a b : R<VAR>x✝¹ : a ≠ 0<VAR>x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a<VAR>IH₁ : gcd (b % a) a ∣ b % a<VAR>IH₂ : gcd (b % a) a ∣ a<GOAL>gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>S : Set α<VAR>c : α<GOAL>c ∈ Iic (sInf S) ↔ c ∈ ⨅ a ∈ S, Iic a
<VAR>α : Type u<VAR>β : Type v<VAR>M : Type w<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>w : α → M<VAR>b : M<VAR>n : ℕ<VAR>inst✝ : LinearOrderedCancelAddCommMonoid M<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>hb : t.card • b < ∑ x ∈ s, w x<GOAL>∑ i ∈ t, b < ∑ i ∈ t, ∑ x ∈ filter (fun x => f x = i) s, w x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<GOAL>StarConvex 𝕜 x s ↔ s.OrdConnected
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c a : M<VAR>h : IsUnit a<VAR>y : M<GOAL>(fun x => a * x) (↑h.unit⁻¹ * y) = y
<VAR>R : Type u1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>A : Type u_1<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>N : Type u4<VAR>N' : Type u5<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>n : ℕ<VAR>f : M →ₗ[R] N<VAR>m : Fin n → M<GOAL>((map f).toLinearMap.compAlternatingMap (ιMulti R n)) m = ((ιMulti R n).compLinearMap f) m
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : CompleteSpace E<VAR>f : ι → E<GOAL>Summable f ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R[X]ᵐᵒᵖ<GOAL>((opRingEquiv R) p).leadingCoeff = op (unop p).leadingCoeff
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h : ‖u - v‖ = ⨅ w, ‖u - ↑w‖<GOAL>∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖<VAR>h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<GOAL>∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖<VAR>h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<VAR>w : F<VAR>hw : w ∈ K<GOAL>⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖<VAR>h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<VAR>w : F<VAR>hw : w ∈ K<VAR>le : ⟪u - v, w⟫_ℝ ≤ 0<GOAL>⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖<VAR>h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<VAR>w : F<VAR>hw : w ∈ K<VAR>le : ⟪u - v, w⟫_ℝ ≤ 0<VAR>ge : ⟪u - v, w⟫_ℝ ≥ 0<GOAL>⟪u - v, w⟫_ℝ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K✝ : Submodule 𝕜 E<VAR>K : Submodule ℝ F<VAR>u v : F<VAR>hv : v ∈ K<VAR>h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0<VAR>this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0<GOAL>‖u - v‖ = ⨅ w, ‖u - ↑w‖