ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : SMulCommClass ℂ 𝕜 E<VAR>V : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>inst✝ : CompleteSpace E<VAR>f : 𝓢(V, E)<VAR>x : V<GOAL>((fourierTransformCLE 𝕜).symm f) x = 𝓕⁻ (⇑f) x
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>ι : Type u_5<VAR>p : Filter ι<VAR>inst✝¹ : UniformSpace F<VAR>inst✝ : UniformAddGroup F<VAR>𝔖 : Set (Set E)<VAR>a : ι → UniformConvergenceCLM σ F 𝔖<VAR>a₀ : UniformConvergenceCLM σ F 𝔖<GOAL>Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x x_1 => (a x) x_1) (⇑a₀) p s
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>ι : Type u_5<VAR>p : Filter ι<VAR>inst✝¹ : UniformSpace F<VAR>inst✝ : UniformAddGroup F<VAR>𝔖 : Set (Set E)<VAR>a : ι → UniformConvergenceCLM σ F 𝔖<VAR>a₀ : UniformConvergenceCLM σ F 𝔖<GOAL>(∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) ∘ a) ((UniformOnFun.toFun 𝔖) ((⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) a₀)) p s) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun x x_1 => (a x) x_1) (⇑a₀) p s
<VAR>n✝ : ℕ<VAR>c✝ : Composition n✝<VAR>n : ℕ<VAR>c : Composition n<VAR>n' : ℕ<VAR>c' : Composition n'<VAR>H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks<GOAL>⟨n, c⟩ = ⟨n', c'⟩
<VAR>n✝ : ℕ<VAR>c✝ : Composition n✝<VAR>n : ℕ<VAR>c : Composition n<VAR>n' : ℕ<VAR>c' : Composition n'<VAR>H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks<VAR>this : n = n'<GOAL>⟨n, c⟩ = ⟨n', c'⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m n : ι →₀ ℕ<VAR>h : m < n<GOAL>(m.sum fun x => id) < n.sum fun x => id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m n : ι →₀ ℕ<VAR>h : m < n<GOAL>Multiset.card (toMultiset m) < Multiset.card (toMultiset n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m n : ι →₀ ℕ<VAR>h : m < n<GOAL>toMultiset m < toMultiset n
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>corec id tail s.tail = s.tail :: corec id tail s.tail.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<GOAL>id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>g : M' → M''<VAR>x : M<VAR>hf : ContMDiffAt I I' n f x<VAR>hg : ContMDiffAt I' I'' n g (f x)<GOAL>ContMDiffAt I I'' n (g ∘ f) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>∫⁻ (x : α), c ∂μ < ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>r : R<VAR>x✝¹ x✝ : R[X]<GOAL>X - C r ∣ x✝¹ * x✝ → X - C r ∣ x✝¹ ∨ X - C r ∣ x✝
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>r : R<VAR>x✝¹ x✝ : R[X]<GOAL>eval r x✝¹ = 0 ∨ eval r x✝ = 0 → eval r x✝¹ = 0 ∨ eval r x✝ = 0
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => ↑(Real.cos (2 * π * a * ↑x))) s (cosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>LSeries.term (fun x => ↑(Real.cos (2 * π * a * ↑x))) s n = ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeries.term (fun x => ↑(Real.cos (2 * π * a * ↑x))) s 0 = ↑(Real.cos (2 * π * a * ↑0)) / ↑0 ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LSeries.term (fun x => ↑(Real.cos (2 * π * a * ↑x))) s n = ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>ρ : Measure (α × β)<GOAL>ρ.snd univ = ρ univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedRing α<VAR>f g : ι → α<VAR>s : Set ι<VAR>a b c d : α<GOAL>MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<VAR>lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<VAR>lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<VAR>lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<VAR>lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))<VAR>lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝ : TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<VAR>lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))<VAR>lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a<GOAL>Tendsto f (comap g (𝓝 d)) (𝓝 a)
<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>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hfi : Integrable f μ<GOAL>0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜) = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)
<VAR>R✝ : Type u<VAR>inst✝² : Semiring R✝<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : CharZero R<GOAL>ringExpChar R = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ArithmeticFunction R<GOAL>⇑f ⍟ ⇑g = ⇑(f * g)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : SMulCommClass ℝ 𝕜 F<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : SMulCommClass ℝ 𝕜' F<VAR>k n : ℕ<VAR>c : 𝕜<VAR>f : 𝓢(E, F)<GOAL>SchwartzMap.seminormAux k n (c • f) ≤ ‖c‖ * SchwartzMap.seminormAux k n f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : SMulCommClass ℝ 𝕜 F<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : SMulCommClass ℝ 𝕜' F<VAR>k n : ℕ<VAR>c : 𝕜<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ‖c‖ * SchwartzMap.seminormAux k n f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : SMulCommClass ℝ 𝕜 F<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : SMulCommClass ℝ 𝕜' F<VAR>k n : ℕ<VAR>c : 𝕜<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>‖c‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖c‖ * SchwartzMap.seminormAux k n f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a b : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Ico a b ↔ x✝ ∈ Ico ⌈a⌉ ⌈b⌉
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>(fun m => m • Q) u x * Q z ^ 2 = Q x * (fun m => m • Q) u z ^ 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>↑u ^ 2 * Q x * Q z ^ 2 = Q x * (↑u * Q z) ^ 2
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u✝ v✝ w✝ : V<VAR>e : Sym2 V<VAR>v w u : V<GOAL>u ∈ ⊤.commonNeighbors v w ↔ u ∈ Set.univ \ {v, w}
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : Integrable f ρ<GOAL>Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : Integrable f ρ<VAR>hf_ae : AEStronglyMeasurable f ρ<GOAL>Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>mα : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>ρ : Measure (α × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : α × Ω → F<VAR>hf_int : (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst<VAR>hf_ae : AEStronglyMeasurable f ρ<GOAL>Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>h : a.factors ≤ b.factors<VAR>ha : ¬a = 0<GOAL>p.count a.factors ≤ p.count b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>h : a.factors ≤ b.factors<VAR>ha : ¬a = 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<GOAL>p.count a.factors ≤ p.count b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>h : a.factors ≤ b.factors<VAR>ha : ¬a = 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h_sb : b.factors = ↑sb<GOAL>p.count a.factors ≤ p.count b.factors
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>ha : ¬a = 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ↑sa ≤ ↑sb<VAR>h_sb : b.factors = ↑sb<GOAL>p.count ↑sa ≤ p.count ↑sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>ha : ¬a = 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : ↑sa ≤ ↑sb<VAR>h_sb : b.factors = ↑sb<GOAL>Multiset.count ⟨p, hp⟩ sa ≤ Multiset.count ⟨p, hp⟩ sb
<VAR>α : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : DecidableEq (Associates α)<VAR>inst✝ : (p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>ha : ¬a = 0<VAR>sa : Multiset { p // Irreducible p }<VAR>h_sa : a.factors = ↑sa<VAR>sb : Multiset { p // Irreducible p }<VAR>h : sa ≤ sb<VAR>h_sb : b.factors = ↑sb<GOAL>Multiset.count ⟨p, hp⟩ sa ≤ Multiset.count ⟨p, hp⟩ sb
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DecidableEq α<VAR>r : α → α → Prop<VAR>l : List α<VAR>hn : l.Nodup<VAR>hs : Symmetric r<VAR>this : IsSymm α r := { symm := hs }<GOAL>(↑l.toFinset).Pairwise r ↔ Pairwise r l
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>c : Con M<VAR>s : Multiset ι<VAR>f g : ι → M<VAR>a✝ : List ι<VAR>h : ∀ x ∈ Quot.mk Setoid.r a✝, c (f x) (g x)<GOAL>c (Multiset.map f (Quot.mk Setoid.r a✝)).prod (Multiset.map g (Quot.mk Setoid.r a✝)).prod
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ZMod 2<GOAL>Submodule.comap reverse (evenOdd Q n) = evenOdd Q n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : StructuredArrow S T<GOAL>(map (𝟙 S)).obj f = f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : StructuredArrow S T<GOAL>(map (𝟙 S)).obj (mk f.hom) = mk f.hom
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a b c d : α<VAR>hf : Antitone f<GOAL>f (max a b) = min (f a) (f b)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<GOAL>(Algebra.adjoin R s).op = Algebra.adjoin R (MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<GOAL>(Algebra.adjoin R s).op.toSubsemiring = (Algebra.adjoin R (MulOpposite.unop ⁻¹' s)).toSubsemiring
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<GOAL>Subsemiring.closure (MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ∪ MulOpposite.unop ⁻¹' s) = Subsemiring.closure (Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.unop ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<VAR>x : Aᵐᵒᵖ<GOAL>x ∈ MulOpposite.unop ⁻¹' Set.range ⇑(algebraMap R A) ↔ x ∈ Set.range ⇑(algebraMap R Aᵐᵒᵖ)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<VAR>x : Aᵐᵒᵖ<GOAL>(∃ y, (algebraMap R A) y = MulOpposite.unop x) ↔ ∃ y, MulOpposite.op ((algebraMap R A) y) = x
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set A<VAR>x : Aᵐᵒᵖ<VAR>x✝ : R<GOAL>(algebraMap R A) x✝ = MulOpposite.unop x ↔ MulOpposite.op ((algebraMap R A) x✝) = x
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>f (1 + x) = 1 + f x
<VAR>α : Type u<VAR>β✝ : α → Type v<VAR>β : α → Type u<VAR>κ : Cardinal.{u}<VAR>hκ : (sum fun a => κ ^ #(β a)) ≤ κ<GOAL>(sum fun a => κ ^ lift.{u, u} #(β a)) ≤ κ
<VAR>α : Type u<VAR>β✝ : α → Type v<VAR>β : α → Type u<VAR>κ : Cardinal.{u}<VAR>hκ : (sum fun a => κ ^ #(β a)) ≤ κ<GOAL>(sum fun a => κ ^ #(β a)) ≤ κ
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>val ⁻¹' (t ∩ s) = val ⁻¹' t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x y : B<VAR>r : R<VAR>hr : (algebraMap R B) r * y = 1<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R B) (x * y) p = 0<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x y : B<VAR>r : R<VAR>hr : (algebraMap R B) r * y = 1<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R B) (x * y) p = 0<GOAL>eval₂ (algebraMap R B) x (p.scaleRoots r) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x y : B<VAR>r : R<VAR>hr : (algebraMap R B) r * y = 1<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R B) (x * y) p = 0<GOAL>eval₂ (algebraMap R B) x = ⇑(aeval ((algebraMap R B) r * (x * y)))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x y : B<VAR>r : R<VAR>hr : y * (algebraMap R B) r = 1<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R B) (x * y) p = 0<GOAL>eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>x y : B<VAR>r : R<VAR>hr : y * (algebraMap R B) r = 1<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R B) (x * y) p = 0<GOAL>eval₂ (algebraMap R B) x = ⇑(aeval x)
<VAR>x : ℝ<VAR>hx✝ : cos x = 0<VAR>hx : Complex.cos ↑x = 0<GOAL>Tendsto (fun x => |tan x|) (𝓝[≠] x) atTop
<VAR>x : ℝ<VAR>hx✝ : cos x = 0<VAR>hx : Complex.cos ↑x = 0<GOAL>Tendsto (fun x => Complex.abs (Complex.tan ↑x)) (𝓝[≠] x) atTop
<VAR>x : ℝ<VAR>hx✝ : cos x = 0<VAR>hx : Complex.cos ↑x = 0<GOAL>Tendsto Complex.ofReal' (𝓝[≠] x) (𝓝[≠] ↑x)
<VAR>x : ℝ<VAR>hx✝ : cos x = 0<VAR>hx : Complex.cos ↑x = 0<GOAL>Tendsto Complex.ofReal' (𝓟 {x}ᶜ) (𝓟 {↑x}ᶜ)
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l✝ l₁ l₂ : List α<VAR>a✝ b a : α<VAR>l : List α<VAR>p : Chain R a l<GOAL>Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>f : G → F<VAR>inst✝ : μ.IsMulRightInvariant<VAR>hf : Integrable f μ<VAR>g : G<GOAL>Integrable (fun t => f (t / g)) μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>f : G → F<VAR>inst✝ : μ.IsMulRightInvariant<VAR>hf : Integrable f μ<VAR>g : G<GOAL>Integrable (fun t => f (t * g⁻¹)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<VAR>i : Fin L.length<GOAL>drop (Nat.sum (take (↑i) (map length L))) (take (Nat.sum (take (↑i + 1) (map length L))) L.join) = L.get i
<VAR>X : Type u<VAR>m₁ m₂ : X → X → X<VAR>e₁ e₂ : X<VAR>h₁ : IsUnital m₁ e₁<VAR>h₂ : IsUnital m₂ e₂<VAR>distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)<GOAL>m₁ = m₂