ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁷ : EMetricSpace X<VAR>inst✝⁶ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ<VAR>hd : ↑(finrank ℝ E) < d<GOAL>μH[d] = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁷ : EMetricSpace X<VAR>inst✝⁶ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ≥0<VAR>hd : ↑(finrank ℝ E) < ↑d<GOAL>μH[↑d] = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁷ : EMetricSpace X<VAR>inst✝⁶ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ≥0<VAR>hd : ↑(finrank ℝ E) < ↑d<GOAL>μH[↑d] univ = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁷ : EMetricSpace X<VAR>inst✝⁶ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ≥0<VAR>hd : ↑(finrank ℝ E) < ↑d<GOAL>dimH univ < ↑d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁷ : EMetricSpace X<VAR>inst✝⁶ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>E : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ≥0<VAR>hd : ↑(finrank ℝ E) < ↑d<GOAL>↑(finrank ℝ E) < ↑d
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : ¬x + y = 0<GOAL>min x.orderTop y.orderTop ≤ (x + y).orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hxy : ¬x + y = 0<GOAL>min (⋯.min ⋯) (⋯.min ⋯) ≤ ⋯.min ⋯
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>f : R'[A]<GOAL>supDegree D (-f) = supDegree D f
<VAR>V : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup V<VAR>inst✝⁶ : InnerProductSpace ℝ V<VAR>inst✝⁵ : MeasurableSpace V<VAR>inst✝⁴ : BorelSpace V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>f : V → E<VAR>inst✝ : CompleteSpace E<VAR>h : Continuous f<VAR>hf : Integrable f volume<VAR>h'f : Integrable (𝓕 f) volume<VAR>v : V<GOAL>𝓕 (𝓕⁻ f) v = f v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁹ : Countable ι<VAR>f✝ g : α → β<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PseudoMetrizableSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this✝¹ : MeasurableSpace α := borel α<VAR>this✝ : BorelSpace α<GOAL>StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁹ : Countable ι<VAR>f✝ g : α → β<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PseudoMetrizableSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this✝¹ : MeasurableSpace α := borel α<VAR>this✝ : BorelSpace α<GOAL>IsSeparable (range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁹ : Countable ι<VAR>f✝ g : α → β<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : TopologicalSpace Y<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : OpensMeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace Y<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PseudoMetrizableSpace α<VAR>f : X × Y → α<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>this✝¹ : MeasurableSpace α := borel α<VAR>this✝ : BorelSpace α<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<GOAL>IsSeparable (range f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Semigroup R<VAR>inst✝ : StarMul R<VAR>x : R<VAR>hx : IsSelfAdjoint x<GOAL>Commute (star x) x
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : NonUnitalSemiring A<VAR>inst✝¹⁴ : StarRing A<VAR>inst✝¹³ : Module R A<VAR>inst✝¹² : IsScalarTower R A A<VAR>inst✝¹¹ : SMulCommClass R A A<VAR>inst✝¹⁰ : StarModule R A<VAR>inst✝⁹ : NonUnitalSemiring B<VAR>inst✝⁸ : StarRing B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : IsScalarTower R B B<VAR>inst✝⁵ : SMulCommClass R B B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : FunLike F A B<VAR>inst✝² : NonUnitalAlgHomClass F R A B<VAR>inst✝¹ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalStarSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(iSup K)<VAR>hx : ↑x ∈ K i<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩
<VAR>α✝ : Type u_1<VAR>α : Type u<VAR>r : CommRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalRing α<GOAL>SeparationQuotient α = (α ⧸ ⊥.closure)
<VAR>α✝ : Type u_1<VAR>α : Type u<VAR>r : CommRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalRing α<GOAL>Quotient (Submodule.quotientRel ⊥.closure) = (α ⧸ ⊥.closure)
<VAR>s : Finset ℕ<VAR>m✝ n✝ p m n : ℕ<VAR>hmn : m.Coprime n<GOAL>Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n
<VAR>s : Finset ℕ<VAR>m✝ n✝ p m n : ℕ<VAR>hmn : m.Coprime n<GOAL>(∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n
<VAR>s : Finset ℕ<VAR>m✝ n✝ p✝ m n : ℕ<VAR>hmn : m.Coprime n<VAR>p : ℕ<VAR>hp : Prime p<GOAL>¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hy : y ∈ nonZeroDivisorsLeft R<GOAL>IsNilpotent (x * y) ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hy : y ∈ nonZeroDivisorsLeft R<GOAL>IsNilpotent (x * y) → IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hy : y ∈ nonZeroDivisorsLeft R<VAR>k : ℕ<VAR>hk : (x * y) ^ k = 0<GOAL>IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>hy : y ∈ nonZeroDivisorsLeft R<VAR>k : ℕ<VAR>hk : x ^ k * y ^ k = 0<GOAL>IsNilpotent x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>h : 0 ≤ n<VAR>x : Step k 0<GOAL>(toStepOfLE k 0 (n + 1) ⋯) x = ((toStepSucc k n).comp (toStepOfLE k 0 n h)) x
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>h : 0 ≤ n<VAR>x : Step k 0<GOAL>(toStepOfLE k 0 (n + 1) ⋯) x = (toStepSucc k n) ((toStepOfLE k 0 n h) x)
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>h : 0 ≤ n<VAR>x : Step k 0<GOAL>AlgebraicClosure.toStepOfLE' k 0 (n + 1) ⋯ x = (toStepSucc k n) (AlgebraicClosure.toStepOfLE' k 0 n h x)
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>n : ℕ<VAR>h : 0 ≤ n<VAR>x : Step k 0<GOAL>AlgebraicClosure.toStepOfLE' k 0 (n + 1) ⋯ x = (⇑(toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k 0 n h) x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>F : J ⥤ Type u<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>x : t.pt<GOAL>∃ j y, t.ι.app j y = x
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>F : J ⥤ Type u<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>x : t.pt<VAR>hx : ¬∃ j y, t.ι.app j y = x<GOAL>False
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F✝ : J ⥤ Type u<VAR>inst✝ : HasColimit F✝<VAR>F : J ⥤ Type u<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>x : t.pt<VAR>hx : ∀ (x_1 : J) (x_2 : F.obj x_1), ¬t.ι.app x_1 x_2 = x<GOAL>False
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : IndepSets {s | MeasurableSet s} {T} μ<GOAL>∀ {f : Ω → ℝ≥0∞}, Measurable f → ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : IndepSets {s | MeasurableSet s} {T} μ<VAR>h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a<GOAL>∀ {f : Ω → ℝ≥0∞}, Measurable f → ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : IndepSets {s | MeasurableSet s} {T} μ<VAR>h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a<GOAL>∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄, MeasurableSet s → ∫⁻ (ω : Ω), s.indicator (fun x => c_1) ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), s.indicator (fun x => c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : IndepSets {s | MeasurableSet s} {T} μ<VAR>h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a<GOAL>∀ ⦃f g : Ω → ℝ≥0∞⦄, Disjoint (Function.support f) (Function.support g) → Measurable f → Measurable g → ∫⁻ (ω : Ω), f ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ → ∫⁻ (ω : Ω), g ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ → ∫⁻ (ω : Ω), (f + g) ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), (f + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>Ω : Type u_1<VAR>mΩ✝ : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>Mf mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>hMf : Mf ≤ mΩ<VAR>c : ℝ≥0∞<VAR>T : Set Ω<VAR>h_meas_T : MeasurableSet T<VAR>h_ind : IndepSets {s | MeasurableSet s} {T} μ<VAR>h_mul_indicator : ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable fun a => g a * T.indicator (fun x => c) a<GOAL>∀ ⦃f : ℕ → Ω → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), ∫⁻ (ω : Ω), f n ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ) → ∫⁻ (ω : Ω), (fun x => ⨆ n, f n x) ω * T.indicator (fun x => c) ω ∂μ = (∫⁻ (ω : Ω), (fun x => ⨆ n, f n x) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun x => c) ω ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Fintype α<VAR>i : α<VAR>m : M<GOAL>∑ j : α, (single j m) i = m
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Fintype α<VAR>i : α<VAR>m : M<GOAL>∑ x : α, Pi.single x m i = m
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeSup ι<VAR>inst✝¹ : NoMaxOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s μ<VAR>t : Set Ω<VAR>ht_tail : MeasurableSet t<GOAL>μ t = 0 ∨ μ t = 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>t : R<VAR>h : ‖t‖ < ‖↑x⁻¹‖⁻¹<GOAL>‖-(↑x⁻¹ * t)‖ < 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>t : R<VAR>h : ‖t‖ < ‖↑x⁻¹‖⁻¹<VAR>a✝ : Nontrivial R<GOAL>‖-(↑x⁻¹ * t)‖ < 1
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : Rˣ<VAR>t : R<VAR>h : ‖t‖ < ‖↑x⁻¹‖⁻¹<VAR>a✝ : Nontrivial R<VAR>hpos : 0 < ‖↑x⁻¹‖<GOAL>‖-(↑x⁻¹ * t)‖ < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : Sym2 α<GOAL>e = s((Quot.out e).1, (Quot.out e).2)
<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>dual A K 0 = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>x : α<VAR>xs : List α<GOAL>foldl f b (xs ++ [x]) = f (foldl f b xs) x
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommRing R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>hpq : Disjoint p.vars q.vars<GOAL>(p - q).vars = p.vars ∪ q.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommRing R<VAR>p q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>hpq : Disjoint p.vars (-q).vars<GOAL>(p - q).vars = p.vars ∪ q.vars
<VAR>R : Type u_1<VAR>inst✝⁴ : Semiring R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module R S<VAR>inst✝¹ : IsScalarTower R S S<VAR>inst✝ : SMulCommClass R S S<VAR>x y : S<VAR>hc : Commute x y<GOAL>Commute (p.smeval x) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>n : ℕ<VAR>a' : α<VAR>l : List α<VAR>this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)<GOAL>Tendsto (fun p => insertNth (n + 1) p.1 p.2) (𝓝 a ×ˢ 𝓝 (a' :: l)) (𝓝 (insertNth (n + 1) a (a' :: l)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>n : ℕ<VAR>a' : α<VAR>l : List α<VAR>this : 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)<GOAL>Tendsto ((fun p => insertNth (n + 1) p.1 p.2) ∘ fun p => (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l) (𝓝 (insertNth (n + 1) a (a' :: l)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² : OrderedCommRing S<VAR>inst✝¹ : Ring R<VAR>abv : AbsoluteValue R S<VAR>inst✝ : NoZeroDivisors S<VAR>a : R<VAR>ha : ¬a = 0<GOAL>abv (-a) = abv a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² : OrderedCommRing S<VAR>inst✝¹ : Ring R<VAR>abv : AbsoluteValue R S<VAR>inst✝ : NoZeroDivisors S<VAR>a : R<VAR>ha : ¬a = 0<GOAL>¬abv (-a) = -abv a
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<GOAL>G.chromaticNumber ≤ ↑n ↔ G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : G.chromaticNumber ≤ ↑n<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : G.chromaticNumber ≤ ↑n<VAR>this : G.chromaticNumber ≠ ⊤<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : G.chromaticNumber ≤ ↑n<VAR>this : ∃ n, G.Colorable n<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : G.chromaticNumber ≤ ↑n<VAR>m : ℕ<VAR>hm : G.Colorable m<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : sInf {n' | G.Colorable n'} ≤ n<VAR>m : ℕ<VAR>hm : G.Colorable m<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : sInf {n' | G.Colorable n'} ≤ n<VAR>m : ℕ<VAR>hm : G.Colorable m<VAR>this : sInf {n' | G.Colorable n'} ∈ {n' | G.Colorable n'}<GOAL>G.Colorable n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>h : sInf {n' | G.Colorable n'} ≤ n<VAR>m : ℕ<VAR>hm : G.Colorable m<VAR>this : G.Colorable (sInf {n' | G.Colorable n'})<GOAL>G.Colorable n
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>inst✝ : Nonempty ι<VAR>m : ι → OuterMeasure α<VAR>s : Set α<GOAL>(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>inst✝ : Nonempty ι<VAR>m : ι → OuterMeasure α<VAR>s : Set α<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ range m, μ (t n) = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i, (m i) (t n)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>lt_hf' : ∀ x ∈ interior D, deriv f x < C<VAR>x✝ : ℝ<VAR>hx✝ : x✝ ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x✝ < y<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>-C < deriv (fun y => -f y) x
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>lt_hf' : ∀ x ∈ interior D, deriv f x < C<VAR>x✝ : ℝ<VAR>hx✝ : x✝ ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x✝ < y<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>deriv f x < C
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>C : ℝ<VAR>lt_hf' : ∀ x ∈ interior D, deriv f x < C<VAR>x : ℝ<VAR>hx : x ∈ D<VAR>y : ℝ<VAR>hy : y ∈ D<VAR>hxy : x < y<VAR>hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x<GOAL>f y - f x < C * (y - x)
<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>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<VAR>s : Set (X × Y)<GOAL>s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<GOAL>(sumLexLift f₁ f₂ g₁ g₂ a b).Nonempty ↔ (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f₁ a₁ b₁).Nonempty) ∨ (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ ((g₁ a₁ b₂).Nonempty ∨ (g₂ a₁ b₂).Nonempty)) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (f₂ a₂ b₂).Nonempty
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : StarRing R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>inst✝ : StarMemClass S A<VAR>s : S<GOAL>(unitization s).range = StarAlgebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : StarRing R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>inst✝ : StarMemClass S A<VAR>s : S<GOAL>StarAlgebra.adjoin R ↑(NonUnitalStarAlgHom.range (NonUnitalStarSubalgebraClass.subtype s)) = StarAlgebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : StarRing R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>inst✝ : StarMemClass S A<VAR>s : S<GOAL>StarAlgebra.adjoin R {x | x ∈ s} = StarAlgebra.adjoin R ↑s
<VAR>R✝ : Type u_1<VAR>p✝ m n : ℕ<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : ExpChar R✝ p✝<VAR>inst✝⁴ : PerfectRing R✝ p✝<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : R[X]<GOAL>¬Irreducible ((expand R p) f)
<VAR>R✝ : Type u_1<VAR>p✝ m n : ℕ<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : ExpChar R✝ p✝<VAR>inst✝⁴ : PerfectRing R✝ p✝<VAR>R : Type u_2<VAR>p : ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP R p<VAR>inst✝ : PerfectRing R p<VAR>f : R[X]<GOAL>¬Irreducible (map (↑(frobeniusEquiv R p).symm) f ^ p)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<GOAL>y ∈ posTangentConeAt s x
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝[>] 0, x + x_1 • y ∈ s
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]x + y] ⊆ s<GOAL>∀ᶠ (x_1 : ℝ) in 𝓝 0, x_1 ∈ Ioi 0 → x + x_1 • y ∈ s