ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p✝ q✝ : R[X]<VAR>x : R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<VAR>p q : R[X]<VAR>H : p.IsRoot a<GOAL>(p * q).IsRoot a
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : Aˣ<GOAL>0 ∈ resolventSet R ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<GOAL>m (⋃ n, s n) = ⨆ n, m (s n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<GOAL>Tendsto (fun k => m ((⋃ n, s n) \ s k)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<GOAL>m ((⋃ n, s n) \ s n) ≤ ∑' (k : ℕ), m (s (k + n + 1) \ s (k + n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<GOAL>(⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<GOAL>(⋃ n, s n) \ s n ⊆ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<GOAL>∀ (i : ℕ), s i ⊆ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<GOAL>x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<VAR>hjn : j ≤ n<GOAL>x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<VAR>hnj : n < j<GOAL>x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this✝ : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<VAR>hnj : n < j<VAR>this : j - (n + 1) + n + 1 = j<GOAL>x ∈ s n ∪ ⋃ i, s (i + n + 1) \ s (i + n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this✝ : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<VAR>hnj : n < j<VAR>this : j - (n + 1) + n + 1 = j<GOAL>x ∈ s (j - (n + 1) + n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ m : OuterMeasure α<VAR>s : ℕ → Set α<VAR>h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)<VAR>h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ⊤<VAR>n : ℕ<VAR>h' : Monotone s<VAR>x : α<VAR>this✝ : ∃ i, x ∈ s i<VAR>j : ℕ<VAR>hj : x ∈ s j<VAR>hlt : ∀ m < j, x ∉ s m<VAR>hnj : n < j<VAR>this : j - (n + 1) + n + 1 = j<GOAL>j - (n + 1) + n < j
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>(∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) = sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>(∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) = (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<GOAL>(f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<GOAL>(fun t => ((lsmul ℝ ℝ) (f t)) (g (x - t))) ≤ fun t => ((lsmul ℝ ℝ) (f t)) (g' (x - t))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<GOAL>(fun t => f t * g (x - t)) ≤ fun t => f t * g' (x - t)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>f g g' : G → ℝ<VAR>hfg : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ<VAR>hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ<VAR>hf : ∀ (x : G), 0 ≤ f x<VAR>hg : ∀ (x : G), g x ≤ g' x<VAR>t : G<GOAL>(fun t => f t * g (x - t)) t ≤ (fun t => f t * g' (x - t)) t
<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>hs : s ⊆ t<VAR>h : μ.restrict t = ν.restrict t<GOAL>μ.restrict s = ν.restrict s
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>T : Set (Set β)<VAR>hf : Inducing f<VAR>h : IsTopologicalBasis T<VAR>a : α<GOAL>(𝓝 a).HasBasis (fun t => t ∈ preimage f '' T ∧ a ∈ t) id
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>β : Type u_2<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>T : Set (Set β)<VAR>hf : Inducing f<VAR>h : IsTopologicalBasis T<VAR>a : α<VAR>s : Set α<GOAL>s ∈ preimage f '' T ∧ a ∈ s ↔ s ∈ (preimage f ∘ fun t => t) '' {i | i ∈ T ∧ f a ∈ i}
<VAR>α : Type u_2<VAR>I : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<GOAL>(↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : V<VAR>i : ι<VAR>hi : i ≠ j<GOAL>IsZero (if i = j then A else 0)
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : V<VAR>i : ι<VAR>hi : i ≠ j<GOAL>IsZero 0
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxz : x < z<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<GOAL>f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f (a • x + b • z) ≤ a • f x + b • f z<GOAL>f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y ≤ a • f x + b • f z<GOAL>f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : (z - x) * f y ≤ (z - x) * (a • f x + b • f z)<GOAL>f y / (y - x) + f y / (z - y) ≤ f x / (y - x) + f z / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z<GOAL>(f y * (z - y) + f y * (y - x)) / ((y - x) * (z - y)) ≤ (f x * (z - y) + f z * (y - x)) / ((y - x) * (z - y))
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z<GOAL>f y * (z - y) + f y * (y - x) ≤ f x * (z - y) + f z * (y - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : 0 < y - x<VAR>hyz : 0 < z - y<VAR>hxz : 0 < z - x<VAR>a : 𝕜 := (z - y) / (z - x)<VAR>b : 𝕜 := (y - x) / (z - x)<VAR>hy : a • x + b • z = y<VAR>key : f y * (z - x) ≤ (z - y) * f x + (y - x) * f z<GOAL>0 < (y - x) * (z - y)
<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>inst✝ : DecidableEq σ<VAR>s s' : σ<VAR>n : ℕ<GOAL>coeff (Finsupp.single s' n) (X s) = if n = 1 ∧ s = s' then 1 else 0
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>s : S<VAR>r : R<VAR>y : ↑Y<GOAL>s • f r • y = f r • s • y
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>s₁ s₂ : S<VAR>y : ↑Y<GOAL>(s₁ + s₂) • y = s₁ • y + s₂ • y
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>r : R<VAR>s : S<VAR>y : ↑Y<GOAL>(f r • s) • y = f r • s • y
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>x✝¹ x✝ : ↑((restrictScalars f ⋙ extendScalars f).obj Y)<GOAL>(lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (x✝¹ + x✝) = (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) x✝¹ + (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) x✝
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>s : S<VAR>z : ↑((restrictScalars f ⋙ extendScalars f).obj Y)<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>(lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • z) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) z
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>s : S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<GOAL>(lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • 0) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) 0
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>s : S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>s' : ↑((restrictScalars f).obj (mk S))<VAR>y : ↑((restrictScalars f).obj Y)<GOAL>(lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • s' ⊗ₜ[R] y) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s' ⊗ₜ[R] y)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>Y : ModuleCat S<VAR>s : S<VAR>m1 : Module R S := Module.compHom S f<VAR>m2 : Module R ↑Y := Module.compHom (↑Y) f<VAR>z1 z2 : ↑((restrictScalars f).obj (mk S)) ⊗[R] ↑((restrictScalars f).obj Y)<VAR>ih1 : (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • z1) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) z1<VAR>ih2 : (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • z2) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) z2<GOAL>(lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (s • (z1 + z2)) = (RingHom.id S) s • (lift { toFun := fun s => { toFun := fun y => s • y, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }) (z1 + z2)
<VAR>i j : ℤ<GOAL>0 < (i - j).natAbs ↔ i ≠ j
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>H₁ H₂ K : Subgroup G<GOAL>H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>inst✝ : IsSuccArchimedean α<VAR>b : α<VAR>hb : b ≤ a<GOAL>IsSuccLimit a → a ≤ b
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>inst✝ : IsSuccArchimedean α<VAR>b : α<VAR>hb : b ≤ a<VAR>c : α<VAR>x✝ : b ≤ c<VAR>H : IsSuccLimit c → c ≤ b<VAR>hc : IsSuccLimit (succ c)<GOAL>succ c ≤ b
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>inst✝ : IsSuccArchimedean α<VAR>b : α<VAR>hb : b ≤ a<VAR>c : α<VAR>x✝ : b ≤ c<VAR>H : IsSuccLimit c → c ≤ b<VAR>hc : IsSuccLimit (succ c)<VAR>this : succ c = c<GOAL>succ c ≤ b
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>s : Submonoid R<VAR>a : R<VAR>ha : a ≠ 0<VAR>hfac : ∀ b ∈ factors a, b ∈ s<VAR>hunit : ∀ (c : Rˣ), ↑c ∈ s<GOAL>a ∈ s
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>s : Submonoid R<VAR>a : R<VAR>ha : a ≠ 0<VAR>hfac : ∀ b ∈ factors a, b ∈ s<VAR>hunit : ∀ (c : Rˣ), ↑c ∈ s<VAR>c : Rˣ<VAR>hc : (factors a).prod * ↑c = a<GOAL>a ∈ s
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>s : Submonoid R<VAR>a : R<VAR>ha : a ≠ 0<VAR>hfac : ∀ b ∈ factors a, b ∈ s<VAR>hunit : ∀ (c : Rˣ), ↑c ∈ s<VAR>c : Rˣ<VAR>hc : (factors a).prod * ↑c = a<GOAL>(factors a).prod * ↑c ∈ s
<VAR>n : ℕ<VAR>ζ : ℂ<VAR>h : IsPrimitiveRoot ζ n<VAR>hn : n ≠ 0<GOAL>∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n
<VAR>n : ℕ<VAR>ζ : ℂ<VAR>h : ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ<VAR>hn : n ≠ 0<GOAL>∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<GOAL>∃ i_1, (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))).arg = ↑i_1 / ↑n * (2 * Real.pi) ∧ IsCoprime i_1 ↑n ∧ i_1.natAbs < n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<GOAL>∃ i_1, (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg = ↑i_1 / ↑n * (2 * Real.pi) ∧ IsCoprime i_1 ↑n ∧ i_1.natAbs < n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>(Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg = ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>(Complex.cos (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi) * Complex.I).arg = ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>↑i / ↑n * (2 * ↑Real.pi) - 2 * ↑Real.pi = ↑(↑(↑i - ↑n) / ↑n * (2 * Real.pi))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>↑(↑i - ↑n) / ↑n * (2 * Real.pi) ∈ Set.Ioc (-Real.pi) Real.pi
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>-Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n ∧ (↑i - ↑n) * (2 * Real.pi) / ↑n ≤ Real.pi
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>-Real.pi < (↑i - ↑n) * (2 * Real.pi) / ↑n
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>(↑i - ↑n) * (2 * Real.pi) / ↑n ≤ 0
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>↑n * (2 - 1) < ↑i * 2
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>i : ℕ<VAR>h : i < n<VAR>hin : i.Coprime n<VAR>h₂ : ¬i * 2 ≤ n<GOAL>0 < ↑n
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>φ (p ^ n) = p ^ (n - 1) * (p - 1)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>m : ℕ<VAR>hn : 0 < m.succ<GOAL>φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n<VAR>A B : Matrix m n α<VAR>x : n → α<VAR>x✝ : m<GOAL>((A + B) *ᵥ x) x✝ = (A *ᵥ x + B *ᵥ x) x✝
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>x : α<VAR>E : Set α<GOAL>0 < infEdist x E ↔ x ∉ closure E
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : Type w<VAR>inst✝¹ : SmallCategory J<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : J ⥤ C<VAR>c₁ : Cofan fun f => F.obj f.fst.1<VAR>c₂ : Cofan F.obj<VAR>s t : c₁.pt ⟶ c₂.pt<VAR>hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }<VAR>ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }<VAR>i : Cofork s t<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<GOAL>F.map f ≫ c₂.ι.app { as := j₂ } ≫ i.π = (c₂.ι.app { as := j₁ } ≫ i.π) ≫ 𝟙 i.pt