ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n c : ℕ<VAR>w : n ≤ n + c<VAR>m : M<GOAL>(f ^ (n + c)) m ∈ (fun n => range (f ^ n)) n
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n c : ℕ<VAR>w : n ≤ n + c<VAR>m : M<GOAL>∃ y, (f ^ n) y = (f ^ (n + c)) m
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₗ[R] M<VAR>n c : ℕ<VAR>w : n ≤ n + c<VAR>m : M<GOAL>(f ^ n) ((f ^ c) m) = (f ^ (n + c)) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<GOAL>(∀ (a : α), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates α), Irreducible a ↔ Prime a
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure s \ closure t = (closure t)ᶜ ∩ closure s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>closure ((closure t)ᶜ ∩ s) = closure (s \ closure t)
<VAR>s : ℝ<VAR>hs : 0 ≤ s<GOAL>0 ≤ Gamma s
<VAR>hs : 0 ≤ 0<GOAL>0 ≤ Gamma 0
<VAR>s : ℝ<VAR>hs : 0 ≤ s<VAR>h : 0 < s<GOAL>0 ≤ Gamma s
<VAR>α : Type u_1<VAR>m n : Num<GOAL>↑(ofZNum (m.sub' n)) = ↑m - ↑n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : f.degree ≠ ↑i<GOAL>f.integralNormalization.coeff i = f.coeff i * f.leadingCoeff ^ (f.natDegree - 1 - i)
<VAR>K : Type u_1<VAR>n : ℤ<VAR>inst✝ : Field K<GOAL>↑↑n.negOnePow = (-1) ^ n
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>k : ℤ<GOAL>↑↑(2 * k).negOnePow = (-1) ^ (2 * k)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>k : ℤ<GOAL>↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)
<VAR>α : Type u_1<VAR>a : α<VAR>inst✝ : SemilatticeSup α<VAR>x y : ↑(Iic a)<GOAL>Codisjoint x y ↔ ↑x ⊔ ↑y = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ a<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a a)<VAR>hx : x ∈ Icc a a<VAR>hC : ∀ y ∈ Icc a a, ‖iteratedDerivWithin (n + 1) f (Icc a a) y‖ ≤ C<GOAL>‖f x - taylorWithinEval f n (Icc a a) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<VAR>A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<VAR>A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t<VAR>this : ‖taylorWithinEval f n (Icc a b) x x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<VAR>A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t<VAR>this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)<GOAL>‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<VAR>A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t<VAR>this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)<GOAL>(↑n !)⁻¹ * |x - a| ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b C x : ℝ<VAR>n : ℕ<VAR>hab : a ≤ b<VAR>hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)<VAR>hx : x ∈ Icc a b<VAR>hC : ∀ y ∈ Icc a b, ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ C<VAR>h : a < b<VAR>hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)<VAR>h' : ∀ y ∈ Ico a x, ‖((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C<VAR>A : ∀ t ∈ Icc a x, HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) (((↑n !)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a x) t<VAR>this : ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ (↑n !)⁻¹ * |x - a| ^ n * C * (x - a)<GOAL>(↑n !)⁻¹ * (x - a) ^ n * C * (x - a) = C * (x - a) ^ (n + 1) / ↑n !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0<VAR>huv : Tendsto (u / v) l (𝓝 1)<GOAL>u ~[l] v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedField β<VAR>t u v w : α → β<VAR>l : Filter α<VAR>hz : ∀ᶠ (x : α) in l, v x = 0 → u x = 0<VAR>huv : Tendsto (u / v) l (𝓝 1)<GOAL>∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>ρ : PartitionOfUnity ι X<VAR>x₀ : X<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>ρ : PartitionOfUnity ι X<VAR>x₀ : X<VAR>I : Finset ι<VAR>H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I<GOAL>∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set X<VAR>f : PartitionOfUnity ι X s<VAR>ρ : PartitionOfUnity ι X<VAR>x₀ : X<VAR>I : Finset ι<VAR>H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I<GOAL>∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f✝ : α → 𝕜<VAR>f : α → ℝ<VAR>hf : Integrable f μ<GOAL>Integrable (fun x => ↑(f x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : RCLike 𝕜<VAR>f✝ : α → 𝕜<VAR>f : α → ℝ<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp (fun x => ↑(f x)) 1 μ
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>x✝ : IsCoprime x x<VAR>a b : R<VAR>h : a * x + b * x = 1<GOAL>x * (a + b) = 1
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>h : IsUnit x<VAR>b : R<VAR>hb : b * x = 1<GOAL>b * x + 0 * x = 1
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j : N →* P<VAR>x✝ : N<GOAL>(f.lift ⋯) x✝ = j x✝
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j : N →* P<VAR>x✝ : N<GOAL>(j.comp f.toMap) (f.sec x✝).1 = (j.comp f.toMap) ↑(f.sec x✝).2 * j x✝
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>j : N →* P<VAR>x✝ : N<GOAL>j (f.toMap (f.sec x✝).1) = j (f.toMap ↑(f.sec x✝).2) * j x✝
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>-log b r⁻¹ = clog b r
<VAR>X : Type u<VAR>inst✝ : TopologicalSpace X<VAR>x y : X<VAR>γ : Path x y<GOAL>delayReflLeft 1 γ = γ
<VAR>b x y : ℕ<VAR>hy : y ≠ 0<VAR>h : x ≤ log b y<GOAL>b ^ x ≤ y
<VAR>b x y : ℕ<VAR>hy : y ≠ 0<VAR>h : x ≤ log b y<VAR>hb : b ≤ 1<GOAL>b ^ x ≤ y
<VAR>b x y : ℕ<VAR>hy : y ≠ 0<VAR>h : x = 0<VAR>hb : b ≤ 1<GOAL>b ^ x ≤ y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : 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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H K : LieSubalgebra R L<VAR>h₁ : H ≤ K<VAR>h₂ : K ≤ H.normalizer<GOAL>∃ I, lieIdealSubalgebra R (↥K) I = ofLe h₁
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : 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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>H K : LieSubalgebra R L<VAR>h₁ : H ≤ K<VAR>h₂ : K ≤ H.normalizer<GOAL>∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f [[a, b]]<GOAL>f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f [[a, b]]<GOAL>sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f [[a, b]]<GOAL>BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f [[a, b]]<GOAL>BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
<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>h : IsClosed s<GOAL>x ∈ s ↔ infEdist x s = 0
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m✝ m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<VAR>this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x<GOAL>HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m✝ m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<VAR>this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x<VAR>hm : m < 0<GOAL>HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m✝ m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<VAR>this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x<VAR>hm : m = 0<GOAL>HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>𝕜 : Type u<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x✝ : 𝕜<VAR>s : Set 𝕜<VAR>m✝ m : ℤ<VAR>x : 𝕜<VAR>h : x ≠ 0 ∨ 0 ≤ m<VAR>this : ∀ (m : ℤ), 0 < m → HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x<VAR>hm : 0 < m<GOAL>HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (m - 1)) x
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t)) = (1 / r) ^ a * Gamma a
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = (↑1 / ↑r) ^ ↑a * Complex.Gamma ↑a
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>↑(∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * rexp (-(r * t))) = ∫ (t : ℝ) in Ioi 0, ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ (↑a - 1) * cexp (-(↑r * ↑t))
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑(t ^ (a - 1) * rexp (-(r * t))) = ↑t ^ ↑(a - 1) * ↑(rexp (-(r * t)))
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑(t ^ (a - 1)) * ↑(rexp (-(r * t))) = ↑(t ^ (a - 1)) * ↑(rexp (-(r * t)))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x ε : ℝ<GOAL>TotallyBounded (ball x ε)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x ε : ℝ<GOAL>TotallyBounded (Ioo (x - ε) (x + ε))
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<GOAL>χ a ∈ Algebra.adjoin ℤ {μ}
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<GOAL>χ 0 ∈ Algebra.adjoin ℤ {μ}
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>inst✝² : Finite F<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>χ : MulChar F R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hχ : χ ^ n = 1<VAR>μ : R<VAR>hμ : IsPrimitiveRoot μ n<VAR>a : F<VAR>h : a ≠ 0<GOAL>χ a ∈ Algebra.adjoin ℤ {μ}
<VAR>a b m n p✝ p : ℕ<VAR>hp : Prime p<VAR>q : ℕ<GOAL>p.factorization q = (single p 1) q
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p : ℕ<VAR>hc : CharP R p<VAR>hp : 2 ≤ p<VAR>d : ℕ<VAR>hdvd : ∃ e, p = d * e<VAR>e : ℕ<VAR>hmul : p = d * p<VAR>this✝³ : ↑p = 0<VAR>this✝² : ↑d * ↑e = 0<VAR>he : ↑e = 0<VAR>this✝¹ : p ∣ e<VAR>this✝ : e ∣ p<VAR>this : e = p<VAR>h₀ : 0 < p<GOAL>d * p = 1 * p
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p : ℕ<VAR>hc : CharP R p<VAR>hp : 2 ≤ p<VAR>d : ℕ<VAR>hdvd : ∃ e, p = d * e<VAR>e : ℕ<VAR>hmul : p = d * p<VAR>this✝³ : ↑p = 0<VAR>this✝² : ↑d * ↑e = 0<VAR>he : ↑e = 0<VAR>this✝¹ : p ∣ e<VAR>this✝ : e ∣ p<VAR>this : e = p<VAR>h₀ : 0 < p<GOAL>d * p = p
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M →[L] N<VAR>s : L.Substructure M<VAR>hs : s.CG<VAR>t : Set M<VAR>ht : t.Countable ∧ (closure L).toFun t = s<GOAL>(closure L).toFun (⇑f '' t) = Substructure.map f s
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>h : M.Basis I X<GOAL>X ⊆ M.closure I
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<GOAL>‖soln - a‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s t : 𝕜 → 𝕜<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<VAR>h_eq : Set.EqOn f g U<VAR>hu : IsOpen U<GOAL>MeromorphicOn g U
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s t : 𝕜 → 𝕜<VAR>f g : 𝕜 → E<VAR>U : Set 𝕜<VAR>hs : MeromorphicOn s U<VAR>ht : MeromorphicOn t U<VAR>hf : MeromorphicOn f U<VAR>hg : MeromorphicOn g U<VAR>h_eq : Set.EqOn f g U<VAR>hu : IsOpen U<VAR>x : 𝕜<VAR>hx : x ∈ U<GOAL>f =ᶠ[𝓝 x] g
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>s t : Set E<VAR>x : E<VAR>hs : s ⊆ t<VAR>r : ℝ≥0∞<VAR>hr : HasFPowerSeriesWithinOnBall f p t x r<GOAL>HasFPowerSeriesWithinAt f p s x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>List.foldr (fun x x_1 => x ⊔ x_1) ⊥ l = l.toFinset.sup id
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝² : SemilatticeSup α<VAR>inst✝¹ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<GOAL>Multiset.fold (fun x x_1 => x ⊔ x_1) ⊥ (↑l).dedup = (↑l).dedup.sup
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<GOAL>𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<GOAL>𝓝[≠] x ≤ 𝓝[≠] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x y : X<VAR>hy : x ≠ y<GOAL>𝓝[≠] x ≤ 𝓝[{y}ᶜ] x