ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>(setToL1 hT) ↑(indicatorConst 1 hs hμs x) = (T s) x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hc : c ≠ 0<VAR>h : a * c = b<GOAL>a = b / c
<VAR>n m : ℕ<VAR>p i : Fin n<VAR>h : i < p<VAR>hi : optParam (i.succ ≠ last n) ⋯<GOAL>p.predAbove i.succ = i.succ.castPred hi
<VAR>τ : ℍ<GOAL>jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
<VAR>τ : ℍ<VAR>h0 : ↑τ ≠ 0<GOAL>jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
<VAR>τ : ℍ<VAR>h0 : ↑τ ≠ 0<VAR>h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0<GOAL>jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
<VAR>τ : ℍ<VAR>h0 : ↑τ ≠ 0<VAR>h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0<GOAL>jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta₂ 0 ↑τ
<VAR>τ : ℍ<VAR>h0 : ↑τ ≠ 0<VAR>h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0<GOAL>jacobiTheta₂ 0 ↑(UpperHalfPlane.mk (-↑τ)⁻¹ ⋯) = (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * cexp (-↑π * I * 0 ^ 2 / ↑τ) * jacobiTheta₂ (0 / ↑τ) (-1 / ↑τ))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<VAR>x : α<GOAL>s ⊆ {x} ↔ s = ∅ ∨ s = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>x : α<GOAL>∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<VAR>x : α<VAR>hs : s.Nonempty<GOAL>s ⊆ {x} ↔ s = ∅ ∨ s = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>HasProd (fun b => f b / g b) (a₁ / a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>HasProd (fun b => f b * (g b)⁻¹) (a₁ * a₂⁻¹)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<GOAL>r ≤ (-pf).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f pf x r<GOAL>r ≤ pf.radius
<VAR>x y z : PGame<GOAL>⟦x * (y + -z)⟧ = ⟦x * y⟧ + -⟦x * z⟧
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>1 * 1 ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>univ = Finset.cons p (map p.succAboveEmb univ) ⋯
<VAR>x y : ℂ<GOAL>sin (2 * x) = 2 * sin x * cos x
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>i : Fin2 n<VAR>u : α i<VAR>h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>LiftP p x → p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>i : Fin2 n<VAR>u : α i<VAR>h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<GOAL>(∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) → p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>i : Fin2 n<VAR>u : α i<VAR>h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f⟩<VAR>h' : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)<GOAL>p i u
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F α<VAR>i✝ : Fin2 n<VAR>u : α i✝<VAR>h : ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i✝ '' univ<VAR>p : (i : Fin2 n) → α i → Prop<VAR>a : (P F).A<VAR>f : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f⟩<VAR>h' : ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)<VAR>i : (P F).B a i✝<VAR>left✝ : i ∈ univ<VAR>hi : f i✝ i = u<GOAL>p i✝ u
<VAR>a x✝ z x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(x / y).arg = ↑x.arg - ↑y.arg
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsLUB s b<GOAL>IsLUB ((fun b => b * a) '' s) (b * a)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>m : ℤ<VAR>h : Irrational (x * ↑m)<GOAL>Irrational (x * ↑↑m)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsOpen s<VAR>h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s<GOAL>TendstoLocallyUniformlyOn F f p (⋃₀ S)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsOpen s<VAR>h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s<GOAL>TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : α<GOAL>IsRelPrime (Associates.mk a) (Associates.mk b) ↔ IsRelPrime a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>hs : s.chainHeight ≠ ⊤<GOAL>(⇑ofDual ⁻¹' s).chainHeight ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>h : S ⊆ {∅, univ}<GOAL>⋃₀ S ∈ {∅, univ}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>h : S ⊆ {∅, univ}<GOAL>(∃ x, ∃ (_ : x ∈ S), ¬x = ∅) → ⋃₀ S = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>h : S ⊆ {∅, univ}<VAR>s : Set α<VAR>hs : s ∈ S<VAR>hne : ¬s = ∅<GOAL>⋃₀ S = univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>h : S ⊆ {∅, univ}<VAR>hs : univ ∈ S<VAR>hne : ¬univ = ∅<GOAL>⋃₀ S = univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ b ⇨ c ↔ b ⊓ a ≤ c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hc' : c ≠ 0<GOAL>mkMetric (c • m) = c • mkMetric m
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hc' : c ≠ 0<GOAL>⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => (c • m) (diam s)) = c • ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>Ico a b = 0 ↔ ¬a < b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : Infinite α<VAR>n : ℕ<GOAL>∃ s, s.card = n + 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k : ℕ<VAR>h : ↑‖x‖₊ < p.radius<GOAL>‖p.changeOrigin x k‖₊ ≤ ∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k : ℕ<VAR>h : ↑‖x‖₊ < p.radius<GOAL>HasSum (fun l => ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l) (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k : ℕ<VAR>h : ↑‖x‖₊ < p.radius<VAR>this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst<GOAL>HasSum (fun l => ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l) (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>k : ℕ<VAR>h : ↑‖x‖₊ < p.radius<VAR>this : Summable fun s => ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst<VAR>l : ℕ<GOAL>HasSum (fun c => ‖p (k + ⟨l, c⟩.fst)‖₊ * ‖x‖₊ ^ ⟨l, c⟩.fst) (∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Module R[X] A<VAR>D : Derivation R R[X] A<VAR>a : R<VAR>f : R[X]<VAR>this : C a • D f = D (C a * f)<GOAL>C a • D f = a • D f
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<VAR>hs : IsCompact s<VAR>hδ : 0 ≤ δ<GOAL>closedBall 1 δ * s = cthickening δ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p : G.Walk a b<VAR>hp : p.IsHamiltonian<GOAL>p.support.toFinset = univ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a b + toIcoDiv hp a b • p = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => b.join s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => ∫⁻ (μ : Measure α), μ s ∂b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<GOAL>adjoin R ⊥ = ⊥
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<GOAL>GaloisConnection (adjoin R) ?u
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s t : Set A<GOAL>Subalgebra R A → Set A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsIntegralClosure A R B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : NoZeroSMulDivisors R B<GOAL>NoZeroSMulDivisors R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsIntegralClosure A R B<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : IsScalarTower R A B<VAR>inst✝ : NoZeroSMulDivisors R B<VAR>x✝¹ : R<VAR>x✝ : A<GOAL>(algebraMap A B) (x✝¹ • x✝) = x✝¹ • (algebraMap A B) x✝
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>ha : a ∉ s<VAR>f : Finset α → β<GOAL>∏ t ∈ (cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (cons a ↑t ⋯)
<VAR>G₀ : Type u<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>G₀' : Type u_3<VAR>inst✝¹ : MulZeroClass M₀<VAR>inst✝ : NoZeroDivisors M₀<VAR>a b : M₀<GOAL>0 = a * b ↔ a = 0 ∨ b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a a₁ a₂ : α<VAR>g : γ → α<VAR>i : ↑(mulSupport g) → β<VAR>hi : Injective i<VAR>hf : mulSupport f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x<GOAL>∏' (x : β), f x = ∏' (y : γ), g y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a a₁ a₂ : α<VAR>g : γ → α<VAR>i : ↑(mulSupport g) → β<VAR>hi : Injective i<VAR>hf : mulSupport f ⊆ Set.range i<VAR>hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x<GOAL>∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>A : Set γ<VAR>hA : MeasurableSet A<VAR>h : Tendsto (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop (𝓝 (∫ (x : γ) in A, κ.density ν a x s ∂ν a))<GOAL>∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<VAR>hq_top : ¬q = ⊤<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<VAR>hq_top : ¬q = ⊤<VAR>hp_lt_top : p < ⊤<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<VAR>hq_top : ¬q = ⊤<VAR>hp_lt_top : p < ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>eLpNorm f p μ ≤ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<VAR>hq_top : ¬q = ⊤<VAR>hp_lt_top : p < ⊤<VAR>hp_pos : 0 < p.toReal<GOAL>eLpNorm' f p.toReal μ ≤ eLpNorm' f q.toReal μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>f : α → E<VAR>p q : ℝ≥0∞<VAR>hpq : p ≤ q<VAR>hf : AEStronglyMeasurable f μ<VAR>hp0 : p ≠ 0<VAR>hp0_lt : 0 < p<VAR>hq0_lt : 0 < q<VAR>hq_top : ¬q = ⊤<VAR>hp_lt_top : p < ⊤<VAR>hp_pos : 0 < p.toReal<VAR>hpq_real : p.toReal ≤ q.toReal<GOAL>eLpNorm' f p.toReal μ ≤ eLpNorm' f q.toReal μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal)
<VAR>R : Type u_1<VAR>M : Type v₁<VAR>N : Type v₂<VAR>S : Type v₃<VAR>inst✝³³ : AddCommMonoid M<VAR>inst✝³² : AddCommMonoid N<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : CommSemiring S<VAR>inst✝²⁹ : Algebra R S<VAR>inst✝²⁸ : Module R M<VAR>inst✝²⁷ : Module R N<VAR>inst✝²⁶ : Module S N<VAR>inst✝²⁵ : IsScalarTower R S N<VAR>f✝ : M →ₗ[R] N<VAR>h : IsBaseChange S f✝<VAR>P : Type u_2<VAR>Q : Type u_3<VAR>inst✝²⁴ : AddCommMonoid P<VAR>inst✝²³ : Module R P<VAR>inst✝²² : AddCommMonoid Q<VAR>inst✝²¹ : Module S Q<VAR>T : Type u_4<VAR>O : Type u_5<VAR>inst✝²⁰ : CommSemiring T<VAR>inst✝¹⁹ : Algebra R T<VAR>inst✝¹⁸ : Algebra S T<VAR>inst✝¹⁷ : IsScalarTower R S T<VAR>inst✝¹⁶ : AddCommMonoid O<VAR>inst✝¹⁵ : Module R O<VAR>inst✝¹⁴ : Module S O<VAR>inst✝¹³ : Module T O<VAR>inst✝¹² : IsScalarTower S T O<VAR>inst✝¹¹ : IsScalarTower R S O<VAR>inst✝¹⁰ : IsScalarTower R T O<VAR>R' : Type u_6<VAR>S' : Type u_7<VAR>inst✝⁹ : CommSemiring R'<VAR>inst✝⁸ : CommSemiring S'<VAR>inst✝⁷ : Algebra R R'<VAR>inst✝⁶ : Algebra S S'<VAR>inst✝⁵ : Algebra R' S'<VAR>inst✝⁴ : Algebra R S'<VAR>inst✝³ : IsScalarTower R R' S'<VAR>inst✝² : IsScalarTower R S S'<VAR>H✝ : IsPushout R S R' S'<VAR>A : Type u_8<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : S →ₐ[R] A<VAR>g : R' →ₐ[R] A<VAR>H : ∀ (x : S) (y : R'), f x * g y = g y * f x<VAR>x : R'<VAR>this : Module S A := Module.compHom A f.toRingHom<VAR>r : R<VAR>s : S<VAR>a : A<GOAL>f (r • s) * a = r • (f s * a)
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<GOAL>Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 ((closure E).indicator fun x => 1))
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_lim : Tendsto δseq atTop (𝓝 0)<VAR>E : Set α<GOAL>∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 ((closure E).indicator (fun x => 1) x))
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>x : M<VAR>hx : x ∈ closure s<GOAL>∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>(sort (fun x x_1 => x ≤ x_1) s).get ⟨0, h⟩ = s.min' H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>(sort (fun x x_1 => x ≤ x_1) s).get ⟨0, h⟩ ≤ s.min' H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<VAR>l : List α := sort (fun x x_1 => x ≤ x_1) s<GOAL>s.min' H ≤ (sort (fun x x_1 => x ≤ x_1) s).get ⟨0, h⟩
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(sum f fun a₁ b => (sum g fun a₂ b₂ => single (a₁ * a₂) (b * b₂)) x) = sum f fun a₁ b₁ => sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Semiring k<VAR>inst✝¹ : DecidableEq G<VAR>inst✝ : Mul G<VAR>f g : MonoidAlgebra k G<VAR>x x✝¹ : G<VAR>x✝ : k<GOAL>(sum g fun a₂ b₂ => single (x✝¹ * a₂) (x✝ * b₂)) x = sum g fun a₂ b₂ => if x✝¹ * a₂ = x then x✝ * b₂ else 0