ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>p : α ⟹ repeat n Prop<VAR>f : β ⟹ Subtype_ p<GOAL>toSubtype p ⊚ ofSubtype p ⊚ f = f
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>p : α ⟹ repeat n Prop<VAR>f : β ⟹ Subtype_ p<GOAL>id ⊚ f = f
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l t₁ t₂ : List α<VAR>h : t₁ ~ t₂<GOAL>l ∪ t₁ ~ l ∪ t₂
<VAR>m n : ℤ<VAR>k : ℕ<GOAL>(m.land n).testBit k = (m.testBit k && n.testBit k)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>φ : R⟦X⟧<VAR>u : Rˣ<GOAL>(constantCoeff R) (φ.invOfUnit u) = ↑u⁻¹
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Set.range ⇑(comap (algebraMap R S)) = ↑(basicOpen r)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>{p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} = ↑(basicOpen r)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>x : PrimeSpectrum R<GOAL>x ∈ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} ↔ x ∈ ↑(basicOpen r)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S✝<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>x : PrimeSpectrum R<GOAL>↑(Submonoid.powers r) ⊓ ↑x.asIdeal ≤ ⊥ ↔ r ∉ x.asIdeal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>U✝ : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝¹ : R1Space α<VAR>inst✝ : OpensMeasurableSpace α<VAR>h : μ.InnerRegular<VAR>U : Set α<VAR>hU : IsOpen U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<GOAL>∃ K ⊆ U, IsClosed K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>U✝ : Set α<VAR>ε : ℝ≥0∞<VAR>inst✝¹ : R1Space α<VAR>inst✝ : OpensMeasurableSpace α<VAR>h : μ.InnerRegular<VAR>U : Set α<VAR>hU : IsOpen U<VAR>r : ℝ≥0∞<VAR>hr : r < μ U<VAR>K : Set α<VAR>KU : K ⊆ U<VAR>K_comp : IsCompact K<VAR>hK : r < μ K<GOAL>∃ K ⊆ U, IsClosed K ∧ r < μ K
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>n : ℤ<VAR>x : α<GOAL>x ∈ {x | (p ^ n) x ≠ x} → x ∈ {x | p x ≠ x}
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>n : ℤ<VAR>x : α<GOAL>¬(p ^ n) x = x → ¬p x = x
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>n : ℤ<VAR>x : α<VAR>hx : ¬(p ^ n) x = x<VAR>H : p x = x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b : α<VAR>inst✝ : LT α<GOAL>⊥ < ↑b ↔ ∀ (a : α), ⊥ = ↑a → a < b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<GOAL>k ∣ l
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<GOAL>k.gcd l = k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<GOAL>k.gcd l ≤ k ∧ ¬k.gcd l < k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<GOAL>¬k.gcd l < k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<VAR>h' : k.gcd l < k<GOAL>False
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l✝ : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<VAR>l : ℕ<VAR>hl : ζ ^ l = 1<VAR>h' : k.gcd l < k<GOAL>ζ ^ k.gcd l = 1
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>x : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>x : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>∑ c : m, (∑ j : n, stdBasisMatrix c j (x c j)) i j = x i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>x : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>∀ (x_1 : m), x_1 ≠ i → (∑ j : n, stdBasisMatrix x_1 j (x x_1 j)) i j = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Semiring α<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>x : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
<VAR>a x : ℝ<GOAL>↑(oddKernel (↑a) x) = jacobiTheta₂'' (↑a) (I * ↑x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<GOAL>{ toFun := toClassFun, map_zero' := ⋯ }.toFun (zero + zero) = { toFun := toClassFun, map_zero' := ⋯ }.toFun zero + { toFun := toClassFun, map_zero' := ⋯ }.toFun zero
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₂ y₂ : F<VAR>h₂ : W.Nonsingular x₂ y₂<GOAL>{ toFun := toClassFun, map_zero' := ⋯ }.toFun (zero + some h₂) = { toFun := toClassFun, map_zero' := ⋯ }.toFun zero + { toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<GOAL>{ toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₁ + zero) = { toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₁) + { toFun := toClassFun, map_zero' := ⋯ }.toFun zero
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>x₂ y₂ : F<VAR>h₂ : W.Nonsingular x₂ y₂<GOAL>{ toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₁ + some h₂) = { toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₁) + { toFun := toClassFun, map_zero' := ⋯ }.toFun (some h₂)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ y₁ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>x₂ y₂ : F<VAR>h₂ : W.Nonsingular x₂ y₂<GOAL>(match some h₁ + some h₂ with | zero => 0 | some h => Additive.ofMul (ClassGroup.mk (CoordinateRing.XYIdeal' h))) = Additive.ofMul (ClassGroup.mk (CoordinateRing.XYIdeal' h₁)) + Additive.ofMul (ClassGroup.mk (CoordinateRing.XYIdeal' h₂))
<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✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' f : ℝ → E<VAR>hderiv : deriv f = f'<VAR>hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x<VAR>hcont : ContinuousOn f' [[a, b]]<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f 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✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' f : ℝ → E<VAR>hderiv : deriv f = f'<VAR>hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x<VAR>hcont : ContinuousOn f' [[a, b]]<GOAL>IntervalIntegrable (deriv f) volume a b
<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✝¹ : NormedSpace ℝ E<VAR>f✝¹ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f✝ f' f : ℝ → E<VAR>hderiv : deriv f = f'<VAR>hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x<VAR>hcont : ContinuousOn f' [[a, b]]<GOAL>IntervalIntegrable f' volume a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>s.einfsep = ⨅ d, uncurry edist ↑d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>x✝ : ℝ≥0∞<GOAL>x✝ ≤ s.einfsep ↔ x✝ ≤ ⨅ d, uncurry edist ↑d
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<GOAL>∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ
<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>ν : Measure α<VAR>f : α → G<VAR>hG : CompleteSpace G<GOAL>∫ (x : α), f x ∂⊤ • μ = ⊤.toReal • ∫ (x : α), f x ∂μ
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<VAR>hc : c ≠ ⊤<GOAL>∫ (x : α), f x ∂c • μ = c.toReal • ∫ (x : α), f x ∂μ
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<VAR>hc : c ≠ ⊤<GOAL>setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<VAR>hc : c ≠ ⊤<VAR>hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal<GOAL>setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<VAR>hc : c ≠ ⊤<VAR>hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal<VAR>hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1<GOAL>setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f
<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>ν : Measure α<VAR>f : α → G<VAR>c : ℝ≥0∞<VAR>hG : CompleteSpace G<VAR>hc : c ≠ ⊤<VAR>hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ)) c.toReal<VAR>hdfma_smul : DominatedFinMeasAdditive (c • μ) (weightedSMul (c • μ)) 1<GOAL>setToFun μ (weightedSMul (c • μ)) hdfma f = setToFun μ (fun s => c.toReal • weightedSMul μ s) ⋯ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>fromRel ⋯ = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>∀ (e : Sym2 α), e ∈ fromRel ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>∀ (x y : α), s(x, y) ∈ fromRel ⋯
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<GOAL>∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<VAR>N2 : ℕ<VAR>hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2<GOAL>∃ N, ∀ i ≥ N, padicNormE (Padic.lim f - ↑f i) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<VAR>N2 : ℕ<VAR>hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2<VAR>i : ℕ<VAR>hi : i ≥ max N N2<GOAL>padicNormE (Padic.lim f - ↑f i) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<VAR>N2 : ℕ<VAR>hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2<VAR>i : ℕ<VAR>hi : i ≥ max N N2<GOAL>padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<VAR>N2 : ℕ<VAR>hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2<VAR>i : ℕ<VAR>hi : i ≥ max N N2<GOAL>padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 2<VAR>N2 : ℕ<VAR>hN2 : ∀ i ≥ N2, padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2<VAR>i : ℕ<VAR>hi : i ≥ max N N2<GOAL>padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>hx : x ∈ nonunits R<VAR>h₁ : x ∈ Metric.ball 1 1<GOAL>‖1 - x‖ < 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : ι → ℝ≥0<VAR>hf_sum : Summable fun a => f a ^ p<VAR>hg_sum : Summable fun a => g a ^ q<GOAL>(Summable fun a => f a * g a) ∧ ∑' (a : ι), f a * g a ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) * (∑' (a : ι), g a ^ q) ^ (1 / q)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f : Filter α<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>π < 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>(√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2) = 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / 4 ^ n
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>1 / (2 ^ n) ^ 3 / 4 * 2 ^ (n + 2) = 1 / 4 ^ n
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>1 / 2 ^ (n * 3 + 2) * 2 ^ (n + 2) = 1 / 2 ^ (2 * n)
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>2 ^ (n * 3 + 2) = 2 ^ (n + 2 + 2 * n)
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>2 ^ (2 * n) ≠ 0
<VAR>n : ℕ<VAR>this : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n + 2)<GOAL>2 ^ (n * 3 + 2) ≠ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : 0 < G<GOAL>False
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : 0 < G<VAR>h' : -G < -0<GOAL>False
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>h : 0 < G<VAR>h' : G < 0<GOAL>False
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<GOAL>support ↑f = ball c f.rOut
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<GOAL>(fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) = ball c f.rOut
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>x : E<GOAL>x ∈ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) ↔ x ∈ ball c f.rOut
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>-(p₁ -ᵥ p₂) = p₂ -ᵥ p₁
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<GOAL>p₁ -ᵥ p₂ + (p₂ -ᵥ p₁) +ᵥ p₁ = 0 +ᵥ p₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : NoMinOrder α<VAR>hs : IsLUB s a<VAR>a' : α<VAR>ha' : a' < a<VAR>h : s = ∅<GOAL>a' ∈ upperBounds s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : NoMinOrder α<VAR>hs : IsLUB s a<VAR>a' : α<VAR>ha' : a' < a<VAR>h : s = ∅<GOAL>a' ∈ univ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>hp : p ≠ 0<VAR>a : R<GOAL>∃ q, p = (X - C a) ^ rootMultiplicity a p * q ∧ ¬X - C a ∣ q
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Submodule R M<VAR>hs : IsCoatom s<GOAL>IsClosed ↑s ∨ Dense ↑s
<VAR>R R' : Type u<VAR>M M' : Type v<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Ring R'<VAR>inst✝⁸ : TopologicalSpace M<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : ContinuousConstSMul R M<VAR>inst✝² : Module R' M'<VAR>inst✝¹ : ContinuousConstSMul R' M'<VAR>inst✝ : ContinuousAdd M<VAR>s : Submodule R M<VAR>hs : IsCoatom s<GOAL>s.topologicalClosure = s → IsClosed ↑s
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>index ((fun h => g * h) '' K) V = index K V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>index K V ≤ index ((fun h => g * h) '' K) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>K = (fun h => g⁻¹ * h) '' ((fun b => g * b) '' K)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>K = (fun x => g⁻¹ * (g * x)) '' K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>(fun x => g⁻¹ * (g * x)) '' K = K
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K : Set G<VAR>hK : IsCompact K<VAR>g : G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>h : G<GOAL>g⁻¹ * (g * h) = h