ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : p ≠ 0<GOAL>weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>hp : ∃ a, ↑a = weightedTotalDegree' w p<GOAL>weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>m : M<VAR>hm : ↑m = weightedTotalDegree' w p<GOAL>weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>m : M<VAR>hm : ↑m = weightedTotalDegree' w p<GOAL>weightedTotalDegree' w p ≤ ↑(weightedTotalDegree w p)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<VAR>m : M<VAR>hm : ↑m = weightedTotalDegree' w p<GOAL>↑(weightedTotalDegree w p) ≤ weightedTotalDegree' w p
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>g₁ g₂ : StoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit<GOAL>g₁ = g₂
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>g₁ g₂ : StoneCech α → β<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit<GOAL>EqOn g₁ g₂ (range stoneCechUnit)
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>s : Set E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>μ (closedBall x r) = μ (ball x r)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : i < (ofFn f).length<GOAL>(ofFn f)[i]? = ofFnNthVal f i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : i < (ofFn f).length<GOAL>some (f ⟨i, ⋯⟩) = ofFnNthVal f i
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>i : ℕ<VAR>h : ¬i < (ofFn f).length<GOAL>(ofFn f)[i]? = ofFnNthVal f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : BEq α<VAR>a : α<VAR>l : AssocList α β<GOAL>find? a l = Option.map (fun x => x.snd) (findEntry? a l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : BEq α<VAR>a key✝ : α<VAR>value✝ : β<VAR>tail✝ : AssocList α β<VAR>tail_ih✝ : find? a tail✝ = Option.map (fun x => x.snd) (findEntry? a tail✝)<GOAL>(match key✝ == a with | true => some value✝ | false => find? a tail✝) = Option.map (fun x => x.snd) (match key✝ == a with | true => some (key✝, value✝) | false => List.find? (fun x => x.fst == a) tail✝.toList)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<VAR>Z : D<VAR>g g' : F.obj X ⟶ Z<GOAL>α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'
<VAR>n : Nat<GOAL>range' 0 (0 + n) = range' 0 n
<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 : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑1) f p u<GOAL>DifferentiableWithinAt 𝕜 f (insert x 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<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑1) f p u<VAR>t : Set E<VAR>t_open : IsOpen t<VAR>xt : x ∈ t<VAR>tu : t ∩ insert x s ⊆ u<GOAL>DifferentiableWithinAt 𝕜 f (insert x 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<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑1) f p u<VAR>t : Set E<VAR>t_open : IsOpen t<VAR>xt : x ∈ t<VAR>tu : insert x s ∩ t ⊆ u<GOAL>DifferentiableWithinAt 𝕜 f (insert x 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<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hn : 1 ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑1) f p u<VAR>t : Set E<VAR>t_open : IsOpen t<VAR>xt : x ∈ t<VAR>tu : insert x s ∩ t ⊆ u<VAR>this : DifferentiableWithinAt 𝕜 f (insert x s ∩ t) x<GOAL>DifferentiableWithinAt 𝕜 f (insert x s) x
<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>1 < p.toNNReal
<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<GOAL>p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<GOAL>Function.Injective ⇑(mulRight R x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<VAR>this : IsDomain A := NoZeroDivisors.to_isDomain A<GOAL>Function.Injective ⇑(mulRight R x)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>a : A<GOAL>(shiftFunctorComm C a 0).hom.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁷ : DecidableEq n<VAR>inst✝⁶ : DecidableEq p<VAR>inst✝⁵ : DecidableEq q<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype p<VAR>inst✝¹ : Fintype q<VAR>inst✝ : Fintype l<GOAL>(PD l R)ᵀ * JD l R * PD l R = 2 • S l R
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁷ : DecidableEq n<VAR>inst✝⁶ : DecidableEq p<VAR>inst✝⁵ : DecidableEq q<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype p<VAR>inst✝¹ : Fintype q<VAR>inst✝ : Fintype l<VAR>h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)<GOAL>(PD l R)ᵀ * JD l R * PD l R = 2 • S l R
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁷ : DecidableEq n<VAR>inst✝⁶ : DecidableEq p<VAR>inst✝⁵ : DecidableEq q<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : CommRing R<VAR>inst✝² : Fintype p<VAR>inst✝¹ : Fintype q<VAR>inst✝ : Fintype l<VAR>h : (PD l R)ᵀ * JD l R = fromBlocks 1 1 1 (-1)<GOAL>fromBlocks (1 * 1 + 1 * 1) (1 * -1 + 1 * 1) (1 * 1 + -1 * 1) (1 * -1 + -1 * 1) = fromBlocks (2 • 1) (2 • 0) (2 • 0) (2 • -1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<VAR>a : α<GOAL>[a].alternatingProd = a * [].alternatingProd⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup α<VAR>a b : α<VAR>l : List α<GOAL>(a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹
<VAR>n : ℕ<GOAL>↑n.succ • bernoulli n = (monomial n) ↑n.succ - ∑ k ∈ range n, ↑((n + 1).choose k) • bernoulli k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>s ∈ ae (Measure.map f μ) ↔ f ⁻¹' s ∈ ae μ
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝ : CanonicallyOrderedCommSemiring α<VAR>a b c d : α<GOAL>0 < a * b ↔ 0 < a ∧ 0 < b
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>c : ℝ<GOAL>Measure.map (fun ω => X ω * c) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>Ω : Type<VAR>inst✝ : MeasureSpace Ω<VAR>X : Ω → ℝ<VAR>hX : Measure.map X ℙ = gaussianReal μ v<VAR>c : ℝ<GOAL>Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>ι : Type u_5<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<GOAL>trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm
<VAR>n m k l : ℕ<VAR>h : n + m = k + l<GOAL>n.dist k = (n + m).dist (k + m)
<VAR>n m k l : ℕ<VAR>h : n + m = k + l<GOAL>(k + l).dist (k + m) = l.dist m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<GOAL>UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hpzero : p ≠ 0<GOAL>UnifIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hpzero : p ≠ 0<VAR>hμ : ¬μ univ = 0<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hpzero : p ≠ 0<VAR>hμ : ¬μ univ = 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hCpos : 0 < C<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ℕ → α → β<VAR>g : α → β<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), StronglyMeasurable (f i)<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ C, 0 < C ∧ ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>hpzero : p ≠ 0<VAR>hμ : ¬μ univ = 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>C : ℝ≥0<VAR>hCpos : 0 < C<VAR>hC : ∀ (i : ι), eLpNorm ({x | C ≤ ‖f i x‖₊}.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)<VAR>i : ι<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≤ ENNReal.ofReal ((ε / (2 * ↑C)) ^ p.toReal)<GOAL>eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<GOAL>r * a ≤ b ↔ a ≤ r⁻¹ * b
<VAR>a b r : ℝ≥0<VAR>hr : r ≠ 0<VAR>this : 0 < r<GOAL>r * a ≤ b ↔ a ≤ r⁻¹ * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>a : α<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = (κ a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>a : α<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (κ.condKernel (a, x)) {y | (x, y) ∈ s} ∂κ.fst a = ((κ.fst ⊗ₖ κ.condKernel) a) s
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>S : Finset ι<VAR>s✝ s : ι → Set Ω<VAR>μ : Measure Ω<GOAL>iIndepSet s μ ↔ ∀ (s' : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s', MeasurableSet (f i)) → μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i)
<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>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>∃ x q, ∃ (h' : G.Adj x w), cons h p = q.concat h'
<VAR>R : Type u_1<VAR>p m n : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : PerfectRing R p<VAR>x : R<GOAL>(iterateFrobeniusEquiv R p 1) x = x ^ p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizationMonoid R<GOAL>X = normalize X
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<GOAL>0 < m
<VAR>x : ℝ<GOAL>(↑x).tan = Real.tan x
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>z n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<GOAL>z ≤ { num := n, den := d, den_nz := h, reduced := c }.floor ↔ ↑z ≤ { num := n, den := d, den_nz := h, reduced := c }
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>z n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<GOAL>z ≤ n / ↑d ↔ ↑z ≤ { num := n, den := d, den_nz := h, reduced := c }
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>z n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<GOAL>z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>z n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>h' : ↑0 < ↑d<GOAL>z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>z n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>h' : ↑0 < ↑d<GOAL>z ≤ n / ↑d ↔ z * ↑d ≤ n
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a✝ a' a₁ a₂ : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>s : σ<VAR>a : R<VAR>n : ℕ<GOAL>C a * X s ^ n = (monomial (Finsupp.single s n)) a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>ha : a₂ ≤ a₁<VAR>hb : b₁ ≤ b₂<GOAL>Icc a₁ b₁ ⊆ Icc a₂ b₂
<VAR>α : Type u<VAR>a : ℕ<VAR>l : List ℕ<GOAL>(a :: l).ranges.join = range (Nat.sum (a :: l))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>(map f p).support = p.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>e : ↑s ≃ ↑t<GOAL>s.encard = t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ {x : Fin n → ℕ} ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<GOAL>x₁ = x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<GOAL>x₁ = x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<VAR>i : Fin (n + 1)<GOAL>x₁ i = x₂ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x✝ x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<VAR>i : Fin (n + 1)<VAR>x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)<GOAL>x₁ i = x₂ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x✝¹ x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<VAR>i : Fin (n + 1)<VAR>x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)<VAR>x✝ : Fin n<GOAL>x₁ x✝.succ < d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n✝ d k N n : ℕ<VAR>ih : ∀ ⦃x₁ : Fin n → ℕ⦄, x₁ ∈ {x | ∀ (i : Fin n), x i < d} → ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂<VAR>x✝¹ x₁ : Fin (n + 1) → ℕ<VAR>hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>x₂ : Fin (n + 1) → ℕ<VAR>hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}<VAR>h : (map d) x₁ = (map d) x₂<VAR>i : Fin (n + 1)<VAR>x : x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)<VAR>x✝ : Fin n<GOAL>x₂ x✝.succ < d
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<GOAL>P f ↔ ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<GOAL>(∀ (i : ↑Y.affineOpens), P (f ∣_ ↑i)) ↔ ∀ (i : 𝒰.J) (i_1 : ↑Y.affineOpens), P ((𝒰.map i ≫ f) ∣_ ↑i_1)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<GOAL>(∀ (i : ↑Y.affineOpens), P (f ∣_ ↑i)) ↔ ∀ (b : ↑Y.affineOpens) (a : 𝒰.J), P ((𝒰.map a ≫ f) ∣_ ↑b)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<VAR>U : ↑Y.affineOpens<GOAL>P (f ∣_ ↑U) ↔ ∀ (a : 𝒰.J), P ((𝒰.map a ≫ f) ∣_ ↑U)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<VAR>U : ↑Y.affineOpens<GOAL>Q (f ∣_ ↑U) ↔ ∀ (a : 𝒰.J), Q (𝒰.map a ∣_ f ⁻¹ᵁ ↑U ≫ f ∣_ ↑U)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Limits.image.ι f ≫ cokernel.π f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 = (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0
<VAR>q : ℚ<VAR>n : ℤ<VAR>hn : n ≠ 0<GOAL>n /. n = 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>μ : R<GOAL>(f - (algebraMap R (End R M)) μ).IsSemisimple ↔ f.IsSemisimple
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>μ : R<GOAL>∀ (p : Submodule R M), p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p ↔ p ≤ Submodule.comap f p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>μ : R<VAR>p : Submodule R M<VAR>h : p ≤ Submodule.comap (f - (algebraMap R (End R M)) μ) p<VAR>x : M<VAR>hx : x ∈ p<GOAL>x ∈ Submodule.comap f p