ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<GOAL>intrinsicFrontier 𝕜 (⇑φ '' ∅) = ⇑φ '' intrinsicFrontier 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this✝ : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<VAR>this : ⇑φ.toAffineMap ∘ Subtype.val ∘ ⇑f.symm = Subtype.val<GOAL>intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>hm : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = (sum fun i => μ.restrict (s i)) t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<GOAL>(MonoidHom.fst M N).comp toProd = fst
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Field K<VAR>inst✝² : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>L : IntermediateField k K<VAR>inst✝ : Algebra.IsAlgebraic k ↥L<VAR>x : K<VAR>hx : x ∈ L<GOAL>x ∈ ⊥
<VAR>k✝ : Type u<VAR>inst✝⁵ : Field k✝<VAR>k : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : Field K<VAR>inst✝² : IsAlgClosed k<VAR>inst✝¹ : Algebra k K<VAR>L : IntermediateField k K<VAR>inst✝ : Algebra.IsAlgebraic k ↥L<VAR>x : K<VAR>hx : x ∈ L<VAR>y : k<VAR>hy : (algebraMap k ↥L) y = ⟨x, hx⟩<GOAL>x ∈ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : 1 < s.card<VAR>a : α<VAR>this : Nonempty α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>hs : 1 < s.card<VAR>a : α<VAR>this✝ : Nonempty α<VAR>this : ∀ b ∈ s, b = a<GOAL>False
<VAR>o : ONote<VAR>x✝ : NF 0<VAR>h₂ : o.NF<GOAL>(0 - o).repr = repr 0 - o.repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<GOAL>(e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>this : a₁.NF<GOAL>(e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>this✝ : a₁.NF<VAR>this : a₂.NF<GOAL>(e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>this✝ : a₁.NF<VAR>this : a₂.NF<VAR>h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr<GOAL>(match e₁.cmp e₂ with | Ordering.lt => 0 | Ordering.gt => e₁.oadd n₁ a₁ | Ordering.eq => match ↑n₁ - ↑n₂ with | 0 => if n₁ = n₂ then a₁.sub a₂ else 0 | k.succ => e₁.oadd k.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ e₂ : ONote<VAR>n₂ : ℕ+<VAR>a₂ : ONote<VAR>h₁ : (e₁.oadd n₁ a₁).NF<VAR>h₂ : (e₂.oadd n₂ a₂).NF<VAR>this✝ : a₁.NF<VAR>this : a₂.NF<VAR>h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr<VAR>ee : (e₁.cmp e₂).Compares e₁ e₂<GOAL>(match e₁.cmp e₂ with | Ordering.lt => 0 | Ordering.gt => e₁.oadd n₁ a₁ | Ordering.eq => match ↑n₁ - ↑n₂ with | 0 => if n₁ = n₂ then a₁.sub a₂ else 0 | k.succ => e₁.oadd k.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
<VAR>m n : ℕ<VAR>hmn : m.Coprime n<GOAL>↑(↑m)⁻¹.val * ↑m = 1
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (ULift.{v, u} X)<GOAL>IsClosed s ↔ IsClosed (up ⁻¹' s)
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(partialSups f) n ≤ x✝ ↔ (Finset.range (n + 1)).sup f ≤ x✝
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>j : E →* F<VAR>b : F<VAR>hb : b ∈ closure ↑j.range<VAR>f : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < f n<GOAL>∃ a, Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
<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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>j : E →* F<VAR>b : F<VAR>hb : b ∈ closure ↑j.range<VAR>f : ℕ → ℝ<VAR>b_pos : ∀ (n : ℕ), 0 < f n<VAR>v : ℕ → F<VAR>sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)<VAR>v_in : ∀ (n : ℕ), v n ∈ j.range<VAR>hv₀ : ‖v 0 / b‖ < f 0<VAR>hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n<GOAL>∃ a, Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
<VAR>α β : Type<VAR>n : ℕ<VAR>f g : (α → ℕ) → ℕ<VAR>df : DiophFn f<VAR>dg : DiophFn g<VAR>v : α → ℕ<GOAL>v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ ¬f v = g v
<VAR>θ : Angle<GOAL>-π < θ.toReal
<VAR>x✝ : ℝ<GOAL>-π < (↑x✝).toReal
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<GOAL>μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<GOAL>μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<GOAL>μ[f|⊥] = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<GOAL>(fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<VAR>h_integral : ∫ (x : α), (μ[f|⊥]) x ∂μ = ∫ (x : α), f x ∂μ<GOAL>(fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<VAR>h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ<GOAL>(fun x => c) = fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<VAR>h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ<GOAL>(μ Set.univ).toReal ≠ 0
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ g : α → F'<VAR>s : Set α<VAR>hμ : NeZero μ<VAR>f : α → F'<VAR>hμ_finite : IsFiniteMeasure μ<VAR>h_meas : StronglyMeasurable (μ[f|⊥])<VAR>c : F'<VAR>h_eq : μ[f|⊥] = fun x => c<VAR>h_integral : (μ Set.univ).toReal • c = ∫ (x : α), f x ∂μ<GOAL>¬μ Set.univ = 0 ∧ ¬μ Set.univ = ⊤
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n' = q<GOAL>((γ₁ + γ₂).rightShift a n' hn').v p q hpq = (γ₁.rightShift a n' hn').v p q hpq + (γ₂.rightShift a n' hn').v p q hpq
<VAR>p : ℝ<GOAL>‖↑(p / 2)‖ = |p| / 2
<GOAL>‖↑(0 / 2)‖ = |0| / 2
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>‖↑(p / 2)‖ = |p| / 2
<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 : Measurable f<GOAL>(mapₗ f) μ = 0 ↔ μ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasShift C ℤ<VAR>T₁ T₂ T₃ A B : Triangle C<VAR>e : A ≅ B<GOAL>e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α ι<VAR>i : ι<VAR>a x : α<VAR>l : Line (η → α) ι<VAR>C : (ι × η → α) → κ<GOAL>Subspace.IsMono C l.toSubspace ↔ IsMono (fun x => C fun x_1 => match x_1 with | (i, e) => x i e) l
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>(f ∘ ⇑σ) ∘ ⇑(sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f : Fin n → α<VAR>σ : Equiv.Perm (Fin n)<GOAL>f ∘ ⇑(σ * sort (f ∘ ⇑σ)) = f ∘ ⇑(sort f)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>f : α → β<VAR>comm : (↑l.toFinset).Pairwise fun a b => Commute (f a) (f b)<VAR>hl : l.Nodup<GOAL>l.toFinset.noncommProd f comm = (List.map f l).prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>f : α → β<VAR>comm : (↑l.toFinset).Pairwise fun a b => Commute (f a) (f b)<VAR>hl : l.dedup = l<GOAL>l.toFinset.noncommProd f comm = (List.map f l).prod
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>mellinInv σ f x = ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>|(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) = ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx0 : ↑x ≠ 0<GOAL>|(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I) = ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx0 : ↑x ≠ 0<GOAL>|(2 * π)⁻¹| • ↑x ^ (-↑σ) • ∫ (a : ℝ), ↑x ^ (-(↑a * I)) • f (↑σ + ↑a * I) = ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx0 : ↑x ≠ 0<GOAL>↑x ^ (-↑σ) • ∫ (x_1 : ℝ), ↑x ^ (-(↑(2 * π * x_1) * I)) • f (↑σ + ↑(2 * π * x_1) * I) = ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx0 : ↑x ≠ 0<VAR>x✝ : ℝ<GOAL>↑x ^ (-(↑(2 * π * x✝) * I)) • f (↑σ + ↑(2 * π * x✝) * I) = cexp (2 * ↑π * (↑x✝ * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑x✝ * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx0 : ↑x ≠ 0<VAR>x✝ : ℝ<GOAL>cexp (↑(Real.log x) * -(↑(2 * π * x✝) * I)) • f (↑σ + ↑(2 * π * x✝) * I) = cexp (2 * ↑π * (↑x✝ * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑x✝ * I)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>σ : ℝ<VAR>f : ℂ → E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I) = ↑x ^ (-↑σ) • 𝓕⁻ (fun y => f (↑σ + 2 * ↑π * ↑y * I)) (-Real.log x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace β<VAR>l l' : Filter α<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>h : AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable f (μ.restrict univ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>h : 0 < (minimalPeriod f x).gcd n<GOAL>minimalPeriod f^[n] x = minimalPeriod f x / (minimalPeriod f x).gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>h : 0 < (minimalPeriod f x).gcd n<GOAL>minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>h : 0 < (minimalPeriod f x).gcd n<GOAL>minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>p q : R<VAR>hpq : q ∣ p<VAR>hq : ¬q = 0<GOAL>p / q ∣ p
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>p q : R<VAR>hpq : q ∣ p<VAR>hq : ¬q = 0<GOAL>p = p / q * q
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝¹ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>UX UY : Scheme<VAR>iY : UY ⟶ Y<VAR>inst✝ : IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : IsPullback iX f' f iY<VAR>H : P f<GOAL>P f'
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝¹ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>UX UY : Scheme<VAR>iY : UY ⟶ Y<VAR>inst✝ : IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : IsPullback iX f' f iY<VAR>H : P f<GOAL>P (pullback.snd f iY)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁰ : CommSemiring C<VAR>inst✝⁹ : CommSemiring D<VAR>inst✝⁸ : CommSemiring E<VAR>inst✝⁷ : CommSemiring F<VAR>inst✝⁶ : Algebra C D<VAR>inst✝⁵ : Algebra C E<VAR>inst✝⁴ : Algebra C F<VAR>inst✝³ : Algebra D F<VAR>inst✝² : Algebra E F<VAR>inst✝¹ : IsScalarTower C D F<VAR>inst✝ : IsScalarTower C E F<VAR>S : Set D<VAR>T : Set E<VAR>hS : adjoin C S = ⊤<VAR>hT : adjoin C T = ⊤<GOAL>Subalgebra.restrictScalars C (adjoin E (⇑(algebraMap D F) '' S)) = Subalgebra.restrictScalars C (adjoin D (⇑(algebraMap E F) '' T))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : GroupWithZero G₀<VAR>inst✝ : ContinuousMul G₀<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>map (fun x => x * a) (𝓝 1) = 𝓝 a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hD : z ∈ verticalClosedStrip 0 1<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>‖f z‖ ≤ sSupNormIm f z.re
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hD : z ∈ verticalClosedStrip 0 1<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>BddAbove (norm ∘ f '' (re ⁻¹' {z.re}))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>z : ℂ<VAR>hD : z ∈ verticalClosedStrip 0 1<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<GOAL>‖f z‖ ∈ norm ∘ f '' (re ⁻¹' {z.re})
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hz : z ∈ lowerCentralSeries R L L 1<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<GOAL>((traceForm R L M) z) x = 0 x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hz : z ∈ lowerCentralSeries R L L 1<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<GOAL>(trace R M) (φ z ∘ₗ φ x) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hz : z ∈ lowerCentralSeries R L L 1<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<GOAL>(trace R M) (φ z ∘ₗ φ x) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hz : z ∈ lowerCentralSeries R L L 1<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<GOAL>(algebraMap R A) ((trace R M) (φ z ∘ₗ φ x)) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>z : L<VAR>hz : z ∈ lowerCentralSeries R L L 1<VAR>hzc : z ∈ LieAlgebra.center R L<VAR>x : L<VAR>A : Type u_1 := AlgebraicClosure (FractionRing R)<GOAL>(trace A (A ⊗[R] M)) ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x)) = 0