ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra ℝ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>n : ℕ<VAR>a : A<VAR>ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x<VAR>ha₁ : autoParam (IsSelfAdjoint a) _auto✝<VAR>this : ∀ x ∈ spectrum ℝ a, x ≠ 0<VAR>ha₂' : ContinuousOn Real.log (spectrum ℝ a)<VAR>ha₂'' : ContinuousOn Real.log ((fun x => x ^ n) '' spectrum ℝ a)<GOAL>cfc (fun x => Real.log (x ^ n)) a = n • cfc Real.log a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hfp : eLpNorm f p μ < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ < ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hfp : eLpNorm f p μ < ⊤<GOAL>0 < p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hfp : eLpNorm f p μ < ⊤<GOAL>eLpNorm' f p.toReal μ < ⊤
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m k : ι<VAR>hk₁ : k < hitting u s n m ω<VAR>hk₂ : n ≤ k<GOAL>u k ω ∉ s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f g : R<GOAL>↑(basicOpen (f * g)) = ↑(basicOpen f ⊓ basicOpen g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Ι (e x) (e y) = Ι x y
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Icc x y ∈ (vitaliFamily volume 1).setsAt x
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt x
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<GOAL>TendstoInMeasure μ f atTop g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0∞<VAR>hδ : δ > 0<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : ↑δ > 0<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ENNReal.ofReal ↑δ<VAR>hunif : TendstoUniformlyOn f g atTop tᶜ<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : TendstoUniformlyOn f g atTop tᶜ<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<GOAL>∃ N, ∀ n ≥ N, μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>{x | ε ≤ dist (f n x) (g x)} ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<GOAL>tᶜ ⊆ {x | ε ≤ dist (f n x) (g x)}ᶜ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>x : α<VAR>hx : x ∈ tᶜ<GOAL>x ∈ {x | ε ≤ dist (f n x) (g x)}ᶜ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : MetricSpace E<VAR>f : ℕ → α → E<VAR>g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : ∀ (n : ℕ), StronglyMeasurable (f n)<VAR>hg : StronglyMeasurable g<VAR>hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < ↑δ<VAR>t : Set α<VAR>left✝ : MeasurableSet t<VAR>ht : μ t ≤ ↑δ<VAR>hunif : ∀ ε > 0, ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ tᶜ, dist (g x) (f n x) < ε<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ∀ x ∈ tᶜ, dist (g x) (f b x) < ε<VAR>n : ℕ<VAR>hn : n ≥ N<VAR>x : α<VAR>hx : x ∈ tᶜ<GOAL>dist (g x) (f n x) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<GOAL>c • closedBall x r = closedBall (c • x) (‖c‖ * r)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>y D (-x) = y D x
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>∀ᵐ (x : E) ∂μ, w D (-x) = w D x
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<GOAL>∀ᵐ (x : E) ∂μ, φ (-x) = φ x
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))<GOAL>∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))<GOAL>ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>htendsto : Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))<GOAL>I < max 1 (I + 1)
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>inst✝ : UCompactlyGeneratedSpace X<GOAL>t = compactlyGenerated X
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>inst✝ : UCompactlyGeneratedSpace X<GOAL>t ≤ compactlyGenerated X
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>inst✝ : UCompactlyGeneratedSpace X<GOAL>compactlyGenerated X ≤ t
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type v<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>hM : Module.IsTorsionBySet R M ↑I<VAR>P : Multiset (Ideal R) := factors I<GOAL>DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type v<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>hM : Module.IsTorsionBySet R M ↑I<VAR>P : Multiset (Ideal R) := factors I<VAR>prime_of_mem : ∀ p ∈ P.toFinset, Prime p<GOAL>DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type v<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>hM : Module.IsTorsionBySet R M ↑I<VAR>P : Multiset (Ideal R) := factors I<VAR>prime_of_mem : ∀ p ∈ P.toFinset, Prime p<GOAL>Module.IsTorsionBySet R M ↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>M : Type v<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ ⊥<VAR>hM : Module.IsTorsionBySet R M ↑I<VAR>P : Multiset (Ideal R) := factors I<VAR>prime_of_mem : ∀ p ∈ P.toFinset, Prime p<GOAL>(↑(factors I).toFinset).Pairwise fun i j => (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤
<VAR>M : Type u_1<VAR>inst✝ : MulOneClass M<VAR>a b : M<VAR>h : 1 * a = b<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : α ≃ β<VAR>e'✝ : β ≃ γ<VAR>e : α ≃ β<VAR>e' : β ≃ γ<VAR>f'' : PartialEquiv γ δ<GOAL>(e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : L.Structure N<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(Equiv_iSup S).symm ((Substructure.inclusion ⋯) x) = (of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : L.Structure N<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(Equiv_iSup S) ((Equiv_iSup S).symm ((Substructure.inclusion ⋯) x)) = (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : Nonempty ι<VAR>inst✝² : IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : L.Structure M<VAR>inst✝ : L.Structure N<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(Substructure.inclusion ⋯) x = (Equiv_iSup S) ((of L ι (fun x => ↥(S x)) (fun x x_1 h => Substructure.inclusion ⋯) i) x)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<GOAL>comap (g.comp f) = comap f ∘ comap g
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R<VAR>g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R<VAR>x : υ → R<GOAL>comap (g.comp f) x = (comap f ∘ comap g) x
<VAR>X Y : Scheme<VAR>inst✝¹ : IsAffine X<VAR>inst✝ : IsAffine Y<VAR>f : X ⟶ Y<GOAL>X.isoSpec.hom ≫ Spec.map (Hom.app f ⊤) = f ≫ Y.isoSpec.hom
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<GOAL>H ≤ zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<GOAL>H.toLieSubmodule ≤ rootSpace H 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>e : o.pred = o<VAR>x✝ : ∃ a, o = succ a<VAR>a : Ordinal.{u_4}<VAR>e' : o = succ a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>x✝ : ∃ a, o = succ a<VAR>a : Ordinal.{u_4}<VAR>e : a = succ a<VAR>e' : o = succ a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<GOAL>Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'
<GOAL>HasSum (fun n => 1 / ↑n ^ 2) (π ^ 2 / 6)
<GOAL>π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!
<GOAL>π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!
<GOAL>π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(1 / 6) / ↑2!
<VAR>a b : EReal<GOAL>-a ≤ b ↔ -b ≤ a
<GOAL>4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).sin = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).sin = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).sin = ‖x‖ / ‖y + x‖
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<GOAL>f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>m n : ℕ<VAR>h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n<VAR>hmn : m.Coprime n<GOAL>f (m * n) = f m * f n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>n : ℕ<VAR>h : 0 ≠ 0 → n ≠ 0 → Coprime 0 n → f (0 * n) = f 0 * f n<VAR>hmn : Coprime 0 n<GOAL>f (0 * n) = f 0 * f n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>m n : ℕ<VAR>h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n<VAR>hmn : m.Coprime n<VAR>hm : m ≠ 0<GOAL>f (m * n) = f m * f n
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>m : ℕ<VAR>hm : m ≠ 0<VAR>h : m ≠ 0 → 0 ≠ 0 → m.Coprime 0 → f (m * 0) = f m * f 0<VAR>hmn : m.Coprime 0<GOAL>f (m * 0) = f m * f 0
<VAR>R : Type u_1<VAR>inst✝ : MonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>m n : ℕ<VAR>h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n<VAR>hmn : m.Coprime n<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<GOAL>f (m * n) = f m * f n
<VAR>f✝ g : CircleDeg1Lift<VAR>f : CircleDeg1Liftˣ<VAR>x : ℝ<GOAL>↑f (↑f⁻¹ x) = x
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<GOAL>restriction 0 = 0
<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>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.addXYZ P Q = -(Q x * P z) • P
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝ : Mul α<VAR>x y : α<GOAL>of x * of y = of (x * y)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIciTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<GOAL>sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIciTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<VAR>h : ∀ x ∈ K, f x < y<GOAL>sSup (f '' K) < y
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIciTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<VAR>h : ∀ x ∈ K, f x < y<VAR>x : β<VAR>hx : x ∈ K<VAR>h2x : IsMaxOn f K x<GOAL>sSup (f '' K) < y
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIciTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<VAR>h : ∀ x ∈ K, f x < y<VAR>x : β<VAR>hx : x ∈ K<VAR>h2x : IsMaxOn f K x<GOAL>∀ b ∈ f '' K, b ≤ f x
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : NormedDivisionRing α<VAR>inst✝¹ : NormedAlgebra ℝ α<VAR>inst✝ : CompleteSpace α<VAR>a : α<GOAL>a * Matrix.unitOf a = (algebraMap ℝ α) ↑‖a‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : NormedDivisionRing α<VAR>inst✝¹ : NormedAlgebra ℝ α<VAR>inst✝ : CompleteSpace α<VAR>a : α<GOAL>(a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α) ‖a‖
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v a : V<VAR>ha : a ∈ (G.singletonSubgraph v).verts<VAR>b : V<VAR>hb : b ∈ (G.singletonSubgraph v).verts<GOAL>(G.singletonSubgraph v).coe.Reachable ⟨a, ha⟩ ⟨b, hb⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v a : V<VAR>ha✝ : a ∈ (G.singletonSubgraph v).verts<VAR>b : V<VAR>hb✝ : b ∈ (G.singletonSubgraph v).verts<VAR>ha : a = v<VAR>hb : b = v<GOAL>(G.singletonSubgraph v).coe.Reachable ⟨a, ha✝⟩ ⟨b, hb✝⟩