ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>i j : ι<VAR>hij : v i = v j<VAR>l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1<VAR>h_total : (Finsupp.total ι M R v) l = 0<VAR>h_single_eq : Finsupp.single i 1 = Finsupp.single j 1<GOAL>i = j
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹ : Monoid M<VAR>a : M<VAR>inst✝ : DecidableEq M<VAR>n : M<VAR>h : Function.Injective fun m => n ^ m<VAR>x✝¹ x✝ : Multiplicative ℕ<GOAL>{ toFun := fun m => pow n (Multiplicative.toAdd m), invFun := fun m => Multiplicative.ofAdd (log m), left_inv := ⋯, right_inv := ⋯ }.toFun (x✝¹ * x✝) = { toFun := fun m => pow n (Multiplicative.toAdd m), invFun := fun m => Multiplicative.ofAdd (log m), left_inv := ⋯, right_inv := ⋯ }.toFun x✝¹ * { toFun := fun m => pow n (Multiplicative.toAdd m), invFun := fun m => Multiplicative.ofAdd (log m), left_inv := ⋯, right_inv := ⋯ }.toFun x✝
<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✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<GOAL>IntervalIntegrable f volume a b ↔ IntervalIntegrable (fun x => f (-x)) 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✝ : NormedRing A<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<GOAL>IntervalIntegrable (fun x => f (-1 * x)) volume (a / -1) (b / -1) ↔ IntervalIntegrable (fun x => f (-x)) volume (-a) (-b)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>t : Multiset α<GOAL>∀ (s : Multiset α), count a (s - t) = count a s - count a t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>t✝ : Multiset α<VAR>b : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t<VAR>s : Multiset α<GOAL>count a (s - b ::ₘ t) = count a s - count a (b ::ₘ t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>t✝ : Multiset α<VAR>b : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t<VAR>s : Multiset α<GOAL>count a (s.erase b) - count a t = count a s - count a (b ::ₘ t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>t✝ t : Multiset α<VAR>IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t<VAR>s : Multiset α<GOAL>count a (s.erase a) - count a t = count a s - count a (a ::ₘ t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>t✝ : Multiset α<VAR>b : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), count a (s - t) = count a s - count a t<VAR>s : Multiset α<VAR>ab : a ≠ b<GOAL>count a (s.erase b) - count a t = count a s - count a (b ::ₘ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : CommSemigroup α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddCommGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>(circulant v * circulant w) i j = (circulant w * circulant v) i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : CommSemigroup α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddCommGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : CommSemigroup α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddCommGroup n<VAR>v w : n → α<VAR>i j : n<GOAL>∀ (x : n), v (i - x) * w (x - j) = w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : CommSemigroup α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddCommGroup n<VAR>v w : n → α<VAR>i j x : n<GOAL>v (i - x) * w (x - j) = w (i - ((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : CommSemigroup α<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : AddCommGroup n<VAR>v w : n → α<VAR>i j x : n<GOAL>v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
<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>hf : Injective2 f<GOAL>image2 f (↑s ∩ ↑s') ↑t = image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<GOAL>(p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p✝ : R<VAR>k✝ p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<GOAL>(p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun n => g n y₀<VAR>hy : y ∈ t<GOAL>HasDerivAt (fun z => ∑' (n : α), g n z) (∑' (n : α), g' n y) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun n => g n y₀<VAR>hy : y ∈ t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>HasFDerivAt (fun z => ∑' (n : α), g n z) (ContinuousLinearMap.smulRight 1 (∑' (n : α), g' n y)) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun n => g n y₀<VAR>hy : y ∈ t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>ContinuousLinearMap.smulRight 1 (∑' (n : α), g' n y) = ∑' (n : α), ContinuousLinearMap.smulRight 1 (g' n y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>ht : IsOpen t<VAR>h't : IsPreconnected t<VAR>hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n<VAR>hy₀ : y₀ ∈ t<VAR>hg0 : Summable fun n => g n y₀<VAR>hy : y ∈ t<VAR>hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.smulRight 1 (g' n y)) y<GOAL>∀ (n : α), ∀ x ∈ t, ‖ContinuousLinearMap.smulRight 1 (g' n x)‖ ≤ u n
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : s ⊆ t<GOAL>(condCount s) t = 1
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : s ⊆ t<VAR>this : IsProbabilityMeasure (condCount s)<GOAL>(condCount s) t = 1
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : s ⊆ t<VAR>this : IsProbabilityMeasure (condCount s)<GOAL>¬(condCount s) t < 1
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : s ⊆ t<VAR>this : IsProbabilityMeasure (condCount s)<GOAL>(condCount s) s ≤ (condCount s) t
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hfg : g ≤ f<VAR>f' : E →ₗ.[R] F<VAR>hf : f.graph.topologicalClosure = f'.graph<GOAL>g.IsClosable
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hfg : g ≤ f<VAR>f' : E →ₗ.[R] F<VAR>hf : f.graph.topologicalClosure = f'.graph<VAR>this : g.graph.topologicalClosure ≤ f'.graph<GOAL>g.IsClosable
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hfg : g ≤ f<VAR>f' : E →ₗ.[R] F<VAR>hf : f.graph.topologicalClosure = f'.graph<VAR>this : g.graph.topologicalClosure ≤ f'.graph<GOAL>g.graph.topologicalClosure = g.graph.topologicalClosure.toLinearPMap.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f g : E →ₗ.[R] F<VAR>hfg : g ≤ f<VAR>f' : E →ₗ.[R] F<VAR>hf : f.graph.topologicalClosure = f'.graph<VAR>this : g.graph.topologicalClosure ≤ f'.graph<GOAL>∀ x ∈ g.graph.topologicalClosure, x.1 = 0 → x.2 = 0
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f g : R →+* ZMod n<VAR>h : RingHom.ker f = RingHom.ker g<GOAL>f = g
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f g : R →+* ZMod n<VAR>h : RingHom.ker f = RingHom.ker g<VAR>this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = ↑⟨g, ⋯⟩<GOAL>f = g
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f g : R →+* ZMod n<VAR>h : RingHom.ker f = RingHom.ker g<VAR>this : ((f.liftOfRightInverse cast ⋯) ⟨g, ⋯⟩).comp f = g<GOAL>f = g
<VAR>a b c : ℕ<GOAL>Fintype.card ↑(Set.Iic b) = b + 1
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(tanh ↑x).im = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<GOAL>IsConnected (connectedComponentIn F x) ↔ x ∈ F
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : CharZero K<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : IsKilling K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>inst✝ : Nontrivial L<GOAL>chainLength 0 β = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : AddCommMonoid P<VAR>F : Type u_13<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : AddMonoidHomClass F M N<VAR>f : N →+ P<VAR>f₂ : M →+ N<GOAL>(⇑f ∘ ⇑f₂) 0 = 0
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>e : σ →₀ ℕ<VAR>s : S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>coeff d (rTensorAlgHom ((monomial e) s ⊗ₜ[R] n)) = if e = d then s ⊗ₜ[R] n else 0
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c : ℝ<VAR>hc_mem : c > 0<VAR>hc : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n
<VAR>r p : ℝ<VAR>hr : 0 ≤ r<VAR>hp : 0 ≤ p<GOAL>r.toNNReal = p.toNNReal ↔ r = p
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>v w : List (Symbol T g.NT)<VAR>hvw : g.Derives v w<VAR>p : List (Symbol T g.NT)<GOAL>g.Derives (v ++ p) (w ++ p)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x
<VAR>x y d m : ℕ<VAR>hd : x.gcd y = d<VAR>d0 : d.beq 0 = false<VAR>dm : x * y = d * m<GOAL>d * x.lcm y = d * m
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 ≤ g a.1}})
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {a | a.1 ∈ s}
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : StrongRankCondition R<VAR>ι : Type u_1<VAR>b : Basis ι R M<VAR>h : Module.rank R M < ℵ₀<GOAL>Nonempty (Fintype ι)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>i : n<GOAL>0 < ⋯.eigenvalues i
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosDef<VAR>i : n<GOAL>0 < RCLike.re (star ((WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i)) ⬝ᵥ A *ᵥ (WithLp.equiv 2 (n → 𝕜)) (⋯.eigenvectorBasis i))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : CompleteBooleanAlgebra α<VAR>a b : α<VAR>s : Set α<VAR>f : ι → α<GOAL>(sInf s)ᶜ = ⨆ i ∈ s, iᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))<VAR>𝓕 : Filter (β × β)<GOAL>𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<GOAL>induced Prod.fst (induced f inst✝⁴) ⊓ induced Prod.snd (induced g inst✝²) = induced (fun p => (f p.1, g p.2)) (induced Prod.fst inst✝⁴ ⊓ induced Prod.snd inst✝²)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<GOAL>induced (f ∘ Prod.fst) inst✝⁴ ⊓ induced (g ∘ Prod.snd) inst✝² = induced (Prod.fst ∘ fun p => (f p.1, g p.2)) inst✝⁴ ⊓ induced (Prod.snd ∘ fun p => (f p.1, g p.2)) inst✝²
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : Zero N<VAR>f : α ↪ β<VAR>l₁ l₂ : α →₀ M<VAR>h : embDomain f l₁ = embDomain f l₂<VAR>a : α<GOAL>l₁ a = l₂ a
<VAR>X : TopCat<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf CommRingCat X<VAR>G : F.SubmonoidPresheaf<VAR>S : (x : ↑X) → Submonoid ↑(F.stalk x)<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>s : (forget CommRingCat).obj (F.obj U)<VAR>hs : s ∈ (fun U => ⨅ x, Submonoid.comap (F.germ x) (S ↑x)) U<GOAL>s ∈ Submonoid.comap (F.map i) ((fun U => ⨅ x, Submonoid.comap (F.germ x) (S ↑x)) V)
<VAR>X : TopCat<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf CommRingCat X<VAR>G : F.SubmonoidPresheaf<VAR>S : (x : ↑X) → Submonoid ↑(F.stalk x)<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>s : (forget CommRingCat).obj (F.obj U)<VAR>hs : ∀ (i : ↥(unop U)), (F.germ i) s ∈ S ↑i<GOAL>∀ (i_1 : ↥(unop V)), (F.germ i_1) ((F.map i) s) ∈ S ↑i_1
<VAR>X : TopCat<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf CommRingCat X<VAR>G : F.SubmonoidPresheaf<VAR>S : (x : ↑X) → Submonoid ↑(F.stalk x)<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>s : (forget CommRingCat).obj (F.obj U)<VAR>hs : ∀ (i : ↥(unop U)), (F.germ i) s ∈ S ↑i<VAR>x : ↥(unop V)<GOAL>(F.map i.unop.op ≫ F.germ x) s ∈ S ↑x
<VAR>X : TopCat<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ConcreteCategory C<VAR>F : Presheaf CommRingCat X<VAR>G : F.SubmonoidPresheaf<VAR>S : (x : ↑X) → Submonoid ↑(F.stalk x)<VAR>U V : (Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>s : (forget CommRingCat).obj (F.obj U)<VAR>hs : ∀ (i : ↥(unop U)), (F.germ i) s ∈ S ↑i<VAR>x : ↥(unop V)<GOAL>(F.germ ((fun x => ⟨↑x, ⋯⟩) x)) s ∈ S ↑x
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : CompactSpace α<GOAL>Tendsto F p (𝓝 f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : CompactSpace α<GOAL>(∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K) ↔ TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p univ
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>degreeLE R ↑n = Submodule.span R ↑(image (fun n => X ^ n) (range (n + 1)))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>degreeLE R ↑n ≤ Submodule.span R ↑(image (fun n => X ^ n) (range (n + 1)))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>Submodule.span R ↑(image (fun n => X ^ n) (range (n + 1))) ≤ degreeLE R ↑n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n : ℕ<GOAL>↑(range (n + 1)) ⊆ (fun n => X ^ n) ⁻¹' ↑(degreeLE R ↑n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n k : ℕ<VAR>hk : k ∈ ↑(range (n + 1))<GOAL>k ∈ (fun n => X ^ n) ⁻¹' ↑(degreeLE R ↑n)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq R<VAR>n k : ℕ<VAR>hk : k ∈ ↑(range (n + 1))<GOAL>((fun n => X ^ n) k).degree ≤ ↑n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>l : List α<GOAL>count a ((c :: l).erase b) = count a (c :: l) - if a = b then 1 else 0
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>l : List α<GOAL>count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if a = b then 1 else 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hg : ∀ i ∈ s, 0 ≤ g i<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul α α<VAR>s t : Set α<VAR>a b : α<VAR>h : s ∈ 𝓝 b<GOAL>{a} * s ∈ 𝓝 (a * b)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul α α<VAR>s t : Set α<VAR>a b : α<VAR>h : s ∈ 𝓝 b<VAR>this : a • s ∈ 𝓝 (a • b)<GOAL>{a} * s ∈ 𝓝 (a * b)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ : ℝ≥0∞<GOAL>(x✝ ^ 0)⁻¹ = x✝⁻¹ ^ 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<GOAL>(⊤ ^ (n + 1))⁻¹ = ⊤⁻¹ ^ (n + 1)
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>n : ℕ<GOAL>(↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>n : ℕ<GOAL>(↑0 ^ (n + 1))⁻¹ = (↑0)⁻¹ ^ (n + 1)
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>p : (x : G) → x ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>mul_right_inv : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯<VAR>x : G<VAR>h : x ∈ closure s<VAR>m : Gᵐᵒᵖ<VAR>hm : m ∈ closure (MulOpposite.unop ⁻¹' s)<GOAL>MulOpposite.unop m ∈ closure s