ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<VAR>hp0 : 0 ≤ p<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<VAR>hp0 : 0 ≤ p<VAR>hq0_lt : 0 < q<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<VAR>hp0 : 0 ≤ p<VAR>hq0_lt : 0 < q<VAR>hq0_ne : q ≠ 0<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<VAR>hp0 : 0 ≤ p<VAR>hq0_lt : 0 < q<VAR>hq0_ne : q ≠ 0<VAR>h_one_div_r : 1 / r = 1 / p - 1 / q<VAR>p2 : ℝ := q / p<VAR>q2 : ℝ := p2.conjExponent<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>p q r : ℝ<VAR>hp0_lt : 0 < p<VAR>hpq : p < q<VAR>hpqr : 1 / p = 1 / q + 1 / r<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>hp0_ne : p ≠ 0<VAR>hp0 : 0 ≤ p<VAR>hq0_lt : 0 < q<VAR>hq0_ne : q ≠ 0<VAR>h_one_div_r : 1 / r = 1 / p - 1 / q<VAR>p2 : ℝ := q / p<VAR>q2 : ℝ := p2.conjExponent<VAR>hp2q2 : p2.IsConjExponent q2<GOAL>(∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>arccos (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)) = arccos (⟪y, x⟫_ℝ / (‖y‖ * ‖x‖))
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 _root_.id s x = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderiv 𝕜 _root_.id x = ContinuousLinearMap.id 𝕜 E
<VAR>r : ℝ<VAR>c : ℂ<GOAL>{ toFun := __src✝.toFun, map_add' := ⋯ }.toFun (r • c) = (RingHom.id ℝ) r • { toFun := __src✝.toFun, map_add' := ⋯ }.toFun c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ<GOAL>a⁺ᵐ / a⁻ᵐ ≤ b⁺ᵐ / b⁻ᵐ
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x + a) ⁻¹' Ioc b c = Ioc (b - a) (c - a)
<VAR>m : ℕ<VAR>_h : 0 < m + 1<GOAL>ack 0 0 < ack (m + 1) 0
<VAR>m n : ℕ<VAR>h : 0 < m + 1<GOAL>ack 0 (n + 1) < ack (m + 1) (n + 1)
<VAR>m n : ℕ<VAR>h : 0 < m + 1<GOAL>n + 1 + 1 < ack m (ack (m + 1) n)
<VAR>m n : ℕ<VAR>h : 0 < m + 1<GOAL>n + 1 + 1 ≤ m + (m + 1 + n + 1)
<VAR>m₁ m₂ : ℕ<VAR>h : m₁ + 1 < m₂ + 1<GOAL>ack (m₁ + 1) 0 < ack (m₂ + 1) 0
<VAR>m₁ m₂ n : ℕ<VAR>h : m₁ + 1 < m₂ + 1<GOAL>ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)
<VAR>m₁ m₂ n : ℕ<VAR>h : m₁ + 1 < m₂ + 1<GOAL>ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<GOAL>append l₁ (mk l₂) = mk (l₁ ++ l₂)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>multiplicity p n ! ≤ ↑(n / (p - 1))
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>∑ i ∈ Ico 1 (log p n).succ, n / p ^ i ≤ n / (p - 1)
<VAR>v : PrimeMultiset<GOAL>Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v
<VAR>v : PrimeMultiset<GOAL>Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v
<VAR>a b n : ℕ<VAR>n0 : n ≠ 0<GOAL>a ^ n ∣ b ^ n ↔ a ∣ b
<VAR>a b n : ℕ<VAR>n0 : n ≠ 0<VAR>h : a ^ n ∣ b ^ n<GOAL>a ∣ b
<VAR>a b n : ℕ<VAR>n0 : n ≠ 0<VAR>h : a ^ n ∣ b ^ n<VAR>g0 : a.gcd b = 0<GOAL>a ∣ b
<VAR>a b n : ℕ<VAR>n0 : n ≠ 0<VAR>h : a ^ n ∣ b ^ n<VAR>g0 : a.gcd b > 0<GOAL>a ∣ b
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>g a' b' : ℕ<VAR>g0' : 0 < g<VAR>co : a'.Coprime b'<VAR>h : (a' * g) ^ n ∣ (b' * g) ^ n<VAR>g0 : (a' * g).gcd (b' * g) > 0<GOAL>a' * g ∣ b' * g
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>g a' b' : ℕ<VAR>g0' : 0 < g<VAR>co : a'.Coprime b'<VAR>h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n<VAR>g0 : (a' * g).gcd (b' * g) > 0<GOAL>a' * g ∣ b' * g
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>g a' b' : ℕ<VAR>g0' : 0 < g<VAR>co : a'.Coprime b'<VAR>g0 : (a' * g).gcd (b' * g) > 0<VAR>h : a' ^ n ∣ b' ^ n<GOAL>a' * g ∣ b' * g
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>g a' b' : ℕ<VAR>g0' : 0 < g<VAR>co : a'.Coprime b'<VAR>g0 : (a' * g).gcd (b' * g) > 0<VAR>h : a' ^ n ∣ b' ^ n<VAR>this : a' ^ succ 0 ∣ a' ^ n<GOAL>a' * g ∣ b' * g
<VAR>n : ℕ<VAR>n0 : n ≠ 0<VAR>g a' b' : ℕ<VAR>g0' : 0 < g<VAR>co : a'.Coprime b'<VAR>g0 : (a' * g).gcd (b' * g) > 0<VAR>h : a' ^ n ∣ b' ^ n<VAR>this : a' ∣ 1<GOAL>a' * g ∣ b' * g
<VAR>x : ONote<VAR>inst✝ : x.NF<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<GOAL>(x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
<VAR>x : ONote<VAR>inst✝ : x.NF<VAR>e : ONote<VAR>n : ℕ+<VAR>a : ONote<VAR>h : (e.oadd n a).NF<VAR>this : a.NF<GOAL>(x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>SpecializingMap f ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(∀ ⦃a : X⦄ ⦃b : Y⦄, b ∈ closure {f a} → ∃ a' ∈ closure {a}, f a' = b) ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<GOAL>(∀ n > 3, P.toPoly.coeff n = 0) ∧ P.toPoly.coeff 3 = P.a ∧ P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<GOAL>(∀ n > 3, ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0) ∧ ((((if True then P.a else 0) + if 3 = 2 then P.b else 0) + if 3 = 1 then P.c else 0) + if False then P.d else 0) = P.a ∧ ((((if 2 = 3 then P.a else 0) + if True then P.b else 0) + if 2 = 1 then P.c else 0) + if False then P.d else 0) = P.b ∧ ((((if 1 = 3 then P.a else 0) + if 1 = 2 then P.b else 0) + if True then P.c else 0) + if False then P.d else 0) = P.c ∧ ((((if False then P.a else 0) + if False then P.b else 0) + if False then P.c else 0) + if True then P.d else 0) = P.d
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>0 + 0 + 0 + 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>¬n = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>¬n = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>¬n = 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 3 < n<GOAL>¬n = 3
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-y < -x ↔ x < y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>b : Basis ι ℝ E<GOAL>b.addHaar (_root_.parallelepiped ⇑b) = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>b : Basis ι ℝ E<GOAL>(addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : Monic 0<GOAL>p %ₘ 0 = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this✝ : DecidableEq R := Classical.decEq R<VAR>h : Monic 0<VAR>this : Subsingleton R<GOAL>p %ₘ 0 = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>h : ¬Monic 0<GOAL>(if h : Monic 0 then (if h_1 : degree 0 ≤ p.degree ∧ p ≠ 0 then let z := C p.leadingCoeff * X ^ (p.natDegree - natDegree 0); let_fun _wf := ⋯; let dm := (p - 0 * z).divModByMonicAux ⋯; (z + dm.1, dm.2) else (0, p)).2 else p) = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : Mul α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a₁ a₂ b₁ b₂ : α<GOAL>a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M →ₗ[R] M'<VAR>h : Surjective ⇑f<GOAL>Module.rank R ↥(LinearMap.range f) = Module.rank R M'
<VAR>α : Type u_1<VAR>l : List α<VAR>x y : α<VAR>hne : x ≠ y<GOAL>x ∈+ y :: l ↔ x ∈+ l
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<VAR>i✝ j✝ : Fin 2<GOAL>↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<VAR>i✝ j✝ : Fin 2<VAR>this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]<GOAL>↑A⁻¹ i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>A : SL(2, R)<VAR>i✝ j✝ : Fin 2<VAR>this : (↑A).adjugate = !![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0]<GOAL>!![↑A 1 1, -↑A 0 1; -↑A 1 0, ↑A 0 0] i✝ j✝ = ↑⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩ i✝ j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>L : Type u_3<VAR>M✝ : Type u_4<VAR>N : Type u_5<VAR>inst✝⁸ : AddCommMonoid L<VAR>inst✝⁷ : TopologicalSpace L<VAR>inst✝⁶ : AddCommMonoid M✝<VAR>inst✝⁵ : TopologicalSpace M✝<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : TopologicalSpace N<VAR>v✝ : VectorMeasure α M✝<VAR>w✝ : VectorMeasure α N<VAR>M : Type u_6<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : TopologicalAddGroup M<VAR>v : VectorMeasure α M<VAR>w : VectorMeasure α N<VAR>h : v ≪ᵥ w<VAR>s : Set α<VAR>hs : ↑w s = 0<GOAL>↑(-v) s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : UpperSet α<VAR>t t₁ t₂ : UpperSet β<VAR>x : α × β<GOAL>s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s s₁ s₂ : UpperSet α<VAR>t t₁ t₂ : UpperSet β<VAR>x : α × β<GOAL>↑(s ×ˢ t) = ↑⊤ ↔ ↑s = ↑⊤ ∨ ↑t = ↑⊤
<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>s : Multiset α<VAR>comm : {x | x ∈ s}.Pairwise Commute<VAR>p : α → Prop<VAR>hom : ∀ (a b : α), p a → p b → p (a * b)<VAR>unit : p 1<VAR>base : ∀ x ∈ s, p x<GOAL>p (s.noncommProd comm)
<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>p : α → Prop<VAR>hom : ∀ (a b : α), p a → p b → p (a * b)<VAR>unit : p 1<VAR>l : List α<VAR>comm : {x | x ∈ ⟦l⟧}.Pairwise Commute<VAR>base : ∀ x ∈ ⟦l⟧, p x<GOAL>p (noncommProd ⟦l⟧ comm)
<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>p : α → Prop<VAR>hom : ∀ (a b : α), p a → p b → p (a * b)<VAR>unit : p 1<VAR>l : List α<VAR>comm : {x | x ∈ ⟦l⟧}.Pairwise Commute<VAR>base : ∀ x ∈ l, p x<GOAL>p l.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1).succ<VAR>h : j ≤ i<GOAL>i.cycleRange j = if j = i then 0 else j + 1
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1).succ<VAR>h : j ≤ i<VAR>this : j = castLE ⋯ ⟨↑j, ⋯⟩<GOAL>i.cycleRange j = if j = i then 0 else j + 1
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1).succ<VAR>h : j ≤ i<VAR>this : j = castLE ⋯ ⟨↑j, ⋯⟩<GOAL>↑(i.cycleRange j) = ↑(if j = i then 0 else j + 1)
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1).succ<VAR>h : j ≤ i<VAR>this : j = castLE ⋯ ⟨↑j, ⋯⟩<GOAL>(if ⟨↑j, ⋯⟩ = last ↑i then 0 else ↑⟨↑j, ⋯⟩ + 1) = ↑(if castLE ⋯ ⟨↑j, ⋯⟩ = i then 0 else castLE ⋯ ⟨↑j, ⋯⟩ + 1)
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1).succ<VAR>h : j ≤ i<VAR>this : j = castLE ⋯ ⟨↑j, ⋯⟩<GOAL>(if ↑j = ↑i then 0 else ↑j + 1) = ↑(if ↑j = ↑i then 0 else j + 1)
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>f (↑n + x) ≤ f ↑n + x * log ↑n
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>hn' : 0 < ↑n<GOAL>f (↑n + x) ≤ f ↑n + x * log ↑n
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_conv : ConvexOn ℝ (Ioi 0) f<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<VAR>hn' : 0 < ↑n<VAR>this : f ↑n + x * log ↑n = (1 - x) * f ↑n + x * f (↑n + 1)<GOAL>f ((1 - x) * ↑n + x * (↑n + 1)) ≤ (1 - x) * f ↑n + x * f (↑n + 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : Irreducible J<VAR>n : ℕ<GOAL>J ^ n ⊔ I = J ^ min (count J (normalizedFactors I)) n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>this : s.diag.card + s.offDiag.card = s.card * s.card<GOAL>s.offDiag.card = s.card * s.card - s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<VAR>this : s.card + s.offDiag.card = s.card * s.card<GOAL>s.offDiag.card = s.card * s.card - s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>s.diag.card + s.offDiag.card = s.card * s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>(filter (fun a => a.1 = a.2) (s ×ˢ s)).card + (filter (fun a => a.1 ≠ a.2) (s ×ˢ s)).card = (s ×ˢ s).card
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>a b : X<GOAL>orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>a b : X<GOAL>¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<GOAL>(α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv = X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<GOAL>(α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv = (α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X Y Z : ModuleCat R<GOAL>∀ (x : ↑X) (y : ↑Y) (z : ↑Z), ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ ((X ⊗ Y).braiding Z).hom ≫ (α_ Z X Y).inv) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) = ((α_ X Y Z).hom ≫ X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>x : σ →₀ ℕ<GOAL>x ∈ ((map f) p).support → x ∈ p.support
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>x : σ →₀ ℕ<GOAL>coeff x ((map f) p) ≠ 0 → coeff x p ≠ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>x : σ →₀ ℕ<GOAL>coeff x p = 0 → coeff x ((map f) p) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>x : σ →₀ ℕ<GOAL>coeff x p = 0 → f (coeff x p) = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>p : MvPolynomial σ R<VAR>x : σ →₀ ℕ<VAR>hx : coeff x p = 0<GOAL>f 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>(eval x) (Polynomial.eval q ((finSuccEquiv R n) f)) = (eval fun i => Fin.cases ((eval x) q) x i) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>eval₂ ((eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C))) (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f = (eval fun i => Fin.cases ((eval x) q) x i) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>eval₂ (RingHom.id R) (fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f = (eval fun i => Fin.cases ((eval x) q) x i) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>(eval fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) f = (eval fun i => Fin.cases ((eval x) q) x i) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<GOAL>(fun s => (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) s))) = fun i => Fin.cases ((eval x) q) x i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>n : ℕ<VAR>x : Fin n → R<VAR>inst✝ : CommSemiring R<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>q : MvPolynomial (Fin n) R<VAR>i : Fin (n + 1)<GOAL>(eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i)) = Fin.cases ((eval x) q) x i
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C S0<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<GOAL>C S
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>C : Set α → Prop<VAR>S : Set α<VAR>h : S.Finite<VAR>S0 : Set α<VAR>hS0 : S0 ⊆ S<VAR>H0 : C S0<VAR>H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)<VAR>this : Finite ↑S<GOAL>C S