ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)).card = ((s * t).disjiUnion (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ?h).card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t : Finset α<GOAL>(↑(s * t)).PairwiseDisjoint fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>w : Word M<VAR>h : w ≠ empty<GOAL>∃ i j w', w'.toWord = w
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>w : Word M<VAR>h : w ≠ empty<GOAL>∃ i j w', w'.toWord.toList = w.toList
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1
<VAR>R : Type u_1<VAR>n : ℕ<VAR>this : μ n = 0 ∨ μ n = 1 ∨ μ n = -1<GOAL>μ n ≠ 0 ↔ μ n = 1 ∨ μ n = -1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>inst✝ : SeparableSpace ↑(range f ∪ {0})<GOAL>Tendsto (fun n => ∫ (x : α), ‖↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>inst✝ : SeparableSpace ↑(range f ∪ {0})<VAR>n : ℕ<GOAL>∫ (x : α), ‖↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ = (ENNReal.toReal ∘ fun n => ∫⁻ (x : α), ↑‖↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖₊ ∂μ) n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>inst✝ : SeparableSpace ↑(range f ∪ {0})<VAR>n : ℕ<GOAL>(∫⁻ (x : α), ↑‖↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖₊ ∂μ).toReal = (ENNReal.toReal ∘ fun n => ∫⁻ (x : α), ↑‖↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖₊ ∂μ) n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : Integrable f μ<VAR>inst✝ : SeparableSpace ↑(range f ∪ {0})<VAR>n : ℕ<GOAL>AEStronglyMeasurable (fun x => ↑(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>ih : ∀ c ⊆ Ici a, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hax : a ≤ x<GOAL>∃ m, x ≤ m ∧ ∀ (z : α), m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>ih : ∀ c ⊆ Ici a, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hax : a ≤ x<VAR>m : α<VAR>left✝ : m ∈ Ici a<VAR>hxm : x ≤ m<VAR>hm : ∀ z ∈ Ici a, m ≤ z → z ≤ m<GOAL>∃ m, x ≤ m ∧ ∀ (z : α), m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ : Set α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>ih : ∀ c ⊆ Ici a, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hax : a ≤ x<VAR>c : Set α<VAR>hca : c ⊆ Ici a<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<VAR>y : α<VAR>hy : y ∈ c<GOAL>∃ ub ∈ Ici a, ∀ z ∈ c, z ≤ ub
<VAR>a x z : ℂ<VAR>θ : ℝ<GOAL>(cos ↑θ + sin ↑θ * I).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>I.radical = I ↔ I.IsRadical
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<VAR>f : α → F<VAR>hf_zero : f =ᶠ[ae μ] 0<GOAL>eLpNorm' f q μ = 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>inst✝ : HasOrthogonalProjection K<VAR>v w : E<GOAL>↑((orthogonalProjection (Submodule.span 𝕜 {v})) (↑‖v‖ ^ 2 • w)) = ⟪v, w⟫_𝕜 • v
<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>inst✝ : HasOrthogonalProjection K<VAR>v w : E<GOAL>⟪v, w⟫_𝕜 • v ∈ Submodule.span 𝕜 {v}
<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>inst✝ : HasOrthogonalProjection K<VAR>v w : E<GOAL>∀ w_1 ∈ Submodule.span 𝕜 {v}, ⟪↑‖v‖ ^ 2 • w - ⟪v, w⟫_𝕜 • v, w_1⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m m₁ m₂ : OuterMeasure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>m₁.trim s ≤ m₂ s ↔ m₁ s ≤ m₂ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<GOAL>sInf I.minimalPrimes = I.radical
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<GOAL>sInf I.minimalPrimes = sInf {J | I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<GOAL>sInf I.minimalPrimes ≤ sInf {J | I ≤ J ∧ J.IsPrime}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I J : Ideal R<GOAL>sInf {J | I ≤ J ∧ J.IsPrime} ≤ sInf I.minimalPrimes
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>k : ℕ<GOAL>s.powerset = univ ↔ s = univ
<VAR>k : ℕ<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>t : ℝ<VAR>n : ℕ<GOAL>f_int k a t (Int.ofNat n) = f_nat k a t n
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<GOAL>Continuous (ToSpec.toFun f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<GOAL>∀ s ∈ Set.range fun r => ↑(sbo r), IsOpen (ToSpec.toFun f ⁻¹' s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(CommRingCat.of (A⁰_ f))<GOAL>IsOpen (ToSpec.toFun f ⁻¹' (fun r => ↑(sbo r)) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>IsOpen (ToSpec.toFun f ⁻¹' (fun r => ↑(sbo r)) (Quotient.mk'' x))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>IsOpen (Subtype.val ⁻¹' ↑(pbo ↑x.num))
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hL : Tendsto f L L<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasDerivAtFilter f^[n] (f' ^ n) x L
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hL : Tendsto f L L<VAR>hx : f x = x<VAR>n : ℕ<VAR>this : HasFDerivAtFilter f^[n] (smulRight 1 f' ^ n) x L<GOAL>HasDerivAtFilter f^[n] (f' ^ n) x L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>xs ys : List α<VAR>n : ℕ<VAR>h : xs ~ ys<VAR>h' : ys.Nodup<GOAL>take n xs ~ List.filter (fun x => elem x (take n xs)) ys
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>g : β → α<VAR>b : β<VAR>s : Set α<VAR>h₁ : LeftInverse g f<VAR>h₂ : Function.RightInverse g f<GOAL>b ∈ f '' s ↔ g b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>g : β → α<VAR>b : β<VAR>s : Set α<VAR>h₁ : LeftInverse g f<VAR>h₂ : Function.RightInverse g f<GOAL>b ∈ g ⁻¹' s ↔ g b ∈ s
<VAR>n : ℕ<GOAL>Λ (n + 1) ≤ Real.log ↑(n + 1)
<VAR>n : ℕ<GOAL>Λ (n + 1) ≤ ∑ i ∈ (n + 1).divisors, Λ i
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a b : ℝ≥0∞<GOAL>(a / b).toReal = a.toReal / b.toReal
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>r : R<VAR>i : ℕ<VAR>a✝ : Nontrivial R<GOAL>((X + C r) ^ i).leadingCoeff = 1
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>a : P.A<VAR>f : P.B a → α<VAR>x : α<GOAL>x ∈ supp ⟨a, f⟩ ↔ x ∈ f '' univ
<VAR>P : PFunctor.{u}<VAR>α : Type u<VAR>a : P.A<VAR>f : P.B a → α<VAR>x : α<GOAL>(∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) ↔ ∃ y, f y = x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : ProperSpace α<VAR>x : α<GOAL>comap (dist x) atTop = cocompact α
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsTrail<VAR>h : u ∈ c.support<GOAL>(c.rotate h).IsTrail
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w : V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>c : G.Walk v v<VAR>hc : c.IsTrail<VAR>h : u ∈ c.support<GOAL>c.edges.Nodup
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>H : X = 0<GOAL>False
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁵ : CommRing 𝒪<VAR>inst✝⁴ : IsDomain 𝒪<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra 𝒪 K<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>inst✝ : ValuationRing 𝒪<GOAL>IsFractionRing 𝒪 K ↔ (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁵ : CommRing 𝒪<VAR>inst✝⁴ : IsDomain 𝒪<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra 𝒪 K<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>inst✝ : ValuationRing 𝒪<VAR>h : IsFractionRing 𝒪 K<VAR>x : K<GOAL>∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a
<VAR>𝒪 : Type u<VAR>K : Type v<VAR>Γ : Type w<VAR>inst✝⁵ : CommRing 𝒪<VAR>inst✝⁴ : IsDomain 𝒪<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra 𝒪 K<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>hh : v.Integers 𝒪<VAR>inst✝ : ValuationRing 𝒪<VAR>h : (∀ (x : K), ∃ a, x = (algebraMap 𝒪 K) a ∨ x⁻¹ = (algebraMap 𝒪 K) a) ∧ Function.Injective ⇑(algebraMap 𝒪 K)<GOAL>IsFractionRing 𝒪 K
<VAR>a✝ b✝ c✝ p q a b c : ℚ<GOAL>c + a ≤ c + b ↔ a ≤ b
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<GOAL>levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<GOAL>levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<VAR>dμν_finite : levyProkhorovEDist μ ν ≠ ⊤<GOAL>levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<VAR>dμν_finite : levyProkhorovEDist μ ν ≠ ⊤<VAR>dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤<GOAL>levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<VAR>dμν_finite : levyProkhorovEDist μ ν ≠ ⊤<VAR>dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤<GOAL>levyProkhorovDist μ ν + levyProkhorovDist ν κ = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<VAR>dμν_finite : levyProkhorovEDist μ ν ≠ ⊤<VAR>dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤<GOAL>levyProkhorovEDist μ κ ≠ ⊤
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : PseudoEMetricSpace Ω<VAR>inst✝³ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>inst✝² : IsFiniteMeasure μ<VAR>inst✝¹ : IsFiniteMeasure ν<VAR>inst✝ : IsFiniteMeasure κ<VAR>dμκ_finite : levyProkhorovEDist μ κ ≠ ⊤<VAR>dμν_finite : levyProkhorovEDist μ ν ≠ ⊤<VAR>dνκ_finite : levyProkhorovEDist ν κ ≠ ⊤<GOAL>levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>hs : NullMeasurableSet s μ<GOAL>μ s + μ sᶜ = μ univ
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : RCLike K<VAR>z w : K<VAR>A : Type u_3<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Module K A<VAR>inst✝² : StarModule K A<VAR>inst✝¹ : IsScalarTower K A A<VAR>inst✝ : SMulCommClass K A A<VAR>x y : A<VAR>c : K<VAR>hxy : c • x < c • y<VAR>hc : 0 < c<GOAL>x < y
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : RCLike K<VAR>z w : K<VAR>A : Type u_3<VAR>inst✝⁷ : NonUnitalRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Module K A<VAR>inst✝² : StarModule K A<VAR>inst✝¹ : IsScalarTower K A A<VAR>inst✝ : SMulCommClass K A A<VAR>x y : A<VAR>c : K<VAR>hxy : c • x < c • y<VAR>hc : 0 < c<VAR>this : c⁻¹ • c • x < c⁻¹ • c • y<GOAL>x < y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>A : Type u_1<VAR>inst✝ : Category.{?u.2919, u_1} A<VAR>S : C<VAR>E : PreOneHypercover S<VAR>i₁ i₂ : E.I₀<VAR>W : C<VAR>p₁ : W ⟶ E.X i₁<VAR>p₂ : W ⟶ E.X i₂<VAR>Z Z' : C<VAR>g : Z ⟶ W<VAR>j : E.I₁ i₁ i₂<VAR>h : Z ⟶ E.Y j<VAR>fac₁ : g ≫ p₁ = h ≫ E.p₁ j<VAR>fac₂ : g ≫ p₂ = h ≫ E.p₂ j<VAR>φ : Z' ⟶ Z<GOAL>∃ j h, (φ ≫ g) ≫ p₁ = h ≫ E.p₁ j ∧ (φ ≫ g) ≫ p₂ = h ≫ E.p₂ j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a b : α<GOAL>sInf s ⊔ b = ⨅ a ∈ s, a ⊔ b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Zero α<VAR>d₁ d₂ : n → α<VAR>h : diagonal d₁ = diagonal d₂<VAR>i : n<GOAL>d₁ i = d₂ i
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>p : Poly α<VAR>v : Option α → ℕ<GOAL>{v | (p (v ∘ some)).natAbs = v none} v ↔ (p (v ∘ some) - ↑(v none)) * (p (v ∘ some) + ↑(v none)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : β × γ → E<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : IntegrableOn f (s ×ˢ univ) ((κ ⊗ₖ η) a)<GOAL>∫ (z : β × γ) in s ×ˢ univ, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<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>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (x / c) = c • ∫ (x : ℝ) in a / c..b / c, f x
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<GOAL>sign (prodCongrRight σ) = ∏ k : α, sign (σ k)
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (x : α), x ∈ l<GOAL>sign (prodCongrRight σ) = ∏ k : α, sign (σ k)
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (x : α), x ∈ l<VAR>l_to_finset : l.toFinset = univ<GOAL>sign (prodCongrRight σ) = ∏ k : α, sign (σ k)
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>σ : α → Perm β<VAR>l : List α<VAR>hl : l.Nodup<VAR>mem_l : ∀ (x : α), x ∈ l<VAR>l_to_finset : l.toFinset = univ<GOAL>(List.map (⇑sign ∘ fun a => prodExtendRight a (σ a)) l).prod = (List.map (fun k => sign (σ k)) l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : a ∈ l<VAR>w : 0 < l.length<GOAL>a ≤ maximum_of_length_pos w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : a ∈ l<VAR>w : 0 < l.length<GOAL>↑a ≤ l.maximum
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>z : ℂ<GOAL>z ∈ spectrum ℂ ((gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a
<VAR>A : Type u_1<VAR>inst✝³ : NormedCommRing A<VAR>inst✝² : NormedAlgebra ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>I : Ideal A<VAR>inst✝ : I.IsMaximal<VAR>a : A<VAR>z : ℂ<GOAL>z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ ∃ f, f a = z
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' (f x)<VAR>hf : HasFDerivAt f f' x<VAR>hy : y = f x<GOAL>HasFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 < δ<VAR>x : E<GOAL>cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
<VAR>P : Type u_1<VAR>inst✝ : CompleteSemilatticeInf P<VAR>F✝ : PFilter P<VAR>x : P<VAR>F : (PFilter P)ᵒᵈ<GOAL>(fun x => toDual (principal x)) x ≤ F ↔ x ≤ (fun F => sInf ↑(ofDual F)) F
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<GOAL>range (enumerateCountable h default) ⊆ insert default s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>n : ℕ<GOAL>enumerateCountable h default n ∈ insert default s