ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x y : ℝ<GOAL>Real.arsinh x = Real.arsinh y ↔ x = y
<VAR>x y : ℝ<GOAL>Real.arsinh x ≤ Real.arsinh y ↔ x ≤ y
<VAR>x y : ℝ<GOAL>Real.arsinh x < Real.arsinh y ↔ x < y
<VAR>x : ℝ<GOAL>Real.arsinh x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>0 ≤ Real.arsinh x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>Real.arsinh x ≤ 0 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>0 < Real.arsinh x ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.arsinh x < 0 ↔ x < 0
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.arsinh (√(1 + x ^ 2))⁻¹ x
<VAR>x : ℝ<GOAL>HasDerivAt Real.arsinh (√(1 + x ^ 2))⁻¹ x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.arsinh
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<VAR>a : ℝ<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun x => Real.arsinh (f x)) l (𝓝 (Real.arsinh a))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X → ℝ<VAR>a : X<VAR>h : ContinuousAt f a<GOAL>ContinuousAt (fun x => Real.arsinh (f x)) a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X → ℝ<VAR>s : Set X<VAR>a : X<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => Real.arsinh (f x)) s a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X → ℝ<VAR>s : Set X<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun x => Real.arsinh (f x)) s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>f : X → ℝ<VAR>h : Continuous f<GOAL>Continuous fun x => Real.arsinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasStrictFDerivAt f f' a<GOAL>HasStrictFDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasFDerivAt f f' a<GOAL>HasFDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>f' : E →L[ℝ] ℝ<VAR>hf : HasFDerivWithinAt f f' s a<GOAL>HasFDerivWithinAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') s a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : DifferentiableAt ℝ f a<GOAL>DifferentiableAt ℝ (fun x => Real.arsinh (f x)) a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>h : DifferentiableWithinAt ℝ f s a<GOAL>DifferentiableWithinAt ℝ (fun x => Real.arsinh (f x)) s a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>h : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.arsinh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>h : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.arsinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>n : ℕ∞<VAR>h : ContDiffAt ℝ n f a<GOAL>ContDiffAt ℝ n (fun x => Real.arsinh (f x)) a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt ℝ n f s a<GOAL>ContDiffWithinAt ℝ n (fun x => Real.arsinh (f x)) s a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>n : ℕ∞<VAR>h : ContDiff ℝ n f<GOAL>ContDiff ℝ n fun x => Real.arsinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>h : ContDiffOn ℝ n f s<GOAL>ContDiffOn ℝ n (fun x => Real.arsinh (f x)) s
<VAR>f : ℝ → ℝ<VAR>a f' : ℝ<VAR>hf : HasStrictDerivAt f f' a<GOAL>HasStrictDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
<VAR>f : ℝ → ℝ<VAR>a f' : ℝ<VAR>hf : HasDerivAt f f' a<GOAL>HasDerivAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') a
<VAR>f : ℝ → ℝ<VAR>s : Set ℝ<VAR>a f' : ℝ<VAR>hf : HasDerivWithinAt f f' s a<GOAL>HasDerivWithinAt (fun x => Real.arsinh (f x)) ((√(1 + f a ^ 2))⁻¹ • f') s a
<VAR>s : Set ℂ<GOAL>ContinuousOn Complex.sin s
<VAR>s : Set ℂ<GOAL>ContinuousOn Complex.cos s
<VAR>s : Set ℝ<GOAL>ContinuousOn Real.sin s
<VAR>s : Set ℝ<GOAL>ContinuousOn Real.cos s
<GOAL>0 ∈ Real.cos '' Set.Icc 1 2
<VAR>x : ℝ<GOAL>Real.sin (x + Real.pi) = -Real.sin x
<VAR>x : ℝ<GOAL>Real.sin (x + 2 * Real.pi) = Real.sin x
<VAR>x : ℝ<GOAL>Real.sin (x - Real.pi) = -Real.sin x
<VAR>x : ℝ<GOAL>Real.sin (x - 2 * Real.pi) = Real.sin x
<VAR>x : ℝ<GOAL>Real.sin (Real.pi - x) = Real.sin x
<VAR>x : ℝ<GOAL>Real.sin (2 * Real.pi - x) = -Real.sin x
<VAR>n : ℕ<GOAL>Real.sin (↑n * Real.pi) = 0
<VAR>n : ℤ<GOAL>Real.sin (↑n * Real.pi) = 0
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (x + ↑n * (2 * Real.pi)) = Real.sin x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (↑n * (2 * Real.pi) - x) = -Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (x + ↑n * Real.pi) = (-1) ^ n * Real.sin x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (x + ↑n * Real.pi) = (-1) ^ n * Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (x - ↑n * Real.pi) = (-1) ^ n * Real.sin x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (x - ↑n * Real.pi) = (-1) ^ n * Real.sin x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.sin (↑n * Real.pi - x) = -((-1) ^ n * Real.sin x)
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.sin (↑n * Real.pi - x) = -((-1) ^ n * Real.sin x)
<VAR>x : ℝ<GOAL>Real.cos (x + Real.pi) = -Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (x + 2 * Real.pi) = Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (x - Real.pi) = -Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (x - 2 * Real.pi) = Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (Real.pi - x) = -Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (2 * Real.pi - x) = Real.cos x
<VAR>n : ℕ<GOAL>Real.cos (↑n * (2 * Real.pi)) = 1
<VAR>n : ℤ<GOAL>Real.cos (↑n * (2 * Real.pi)) = 1
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (x + ↑n * (2 * Real.pi)) = Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (x + ↑n * (2 * Real.pi)) = Real.cos x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (x - ↑n * (2 * Real.pi)) = Real.cos x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (x + ↑n * Real.pi) = (-1) ^ n * Real.cos x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (x + ↑n * Real.pi) = (-1) ^ n * Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (x - ↑n * Real.pi) = (-1) ^ n * Real.cos x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (x - ↑n * Real.pi) = (-1) ^ n * Real.cos x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.cos (↑n * Real.pi - x) = (-1) ^ n * Real.cos x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.cos (↑n * Real.pi - x) = (-1) ^ n * Real.cos x
<VAR>n : ℕ<GOAL>Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1
<VAR>n : ℤ<GOAL>Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1
<VAR>n : ℕ<GOAL>Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1
<VAR>n : ℤ<GOAL>Real.cos (↑n * (2 * Real.pi) - Real.pi) = -1
<VAR>x : ℝ<VAR>h0x : 0 < x<VAR>hxp : x < Real.pi<GOAL>0 < Real.sin x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioo 0 Real.pi<GOAL>0 < Real.sin x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 Real.pi<GOAL>0 ≤ Real.sin x
<VAR>x : ℝ<VAR>h0x : 0 ≤ x<VAR>hxp : x ≤ Real.pi<GOAL>0 ≤ Real.sin x
<VAR>x : ℝ<VAR>hx0 : x < 0<VAR>hpx : -Real.pi < x<GOAL>Real.sin x < 0
<VAR>x : ℝ<VAR>hx0 : x ≤ 0<VAR>hpx : -Real.pi ≤ x<GOAL>Real.sin x ≤ 0
<VAR>x : ℝ<GOAL>Real.sin (x + Real.pi / 2) = Real.cos x
<VAR>x : ℝ<GOAL>Real.sin (x - Real.pi / 2) = -Real.cos x
<VAR>x : ℝ<GOAL>Real.sin (Real.pi / 2 - x) = Real.cos x
<VAR>x : ℝ<GOAL>Real.cos (x + Real.pi / 2) = -Real.sin x
<VAR>x : ℝ<GOAL>Real.cos (x - Real.pi / 2) = Real.sin x
<VAR>x : ℝ<GOAL>Real.cos (Real.pi / 2 - x) = Real.sin x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)<GOAL>0 < Real.cos x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)<GOAL>0 ≤ Real.cos x
<VAR>x : ℝ<VAR>hl : -(Real.pi / 2) ≤ x<VAR>hu : x ≤ Real.pi / 2<GOAL>0 ≤ Real.cos x
<VAR>x : ℝ<VAR>hx₁ : Real.pi / 2 < x<VAR>hx₂ : x < Real.pi + Real.pi / 2<GOAL>Real.cos x < 0
<VAR>x : ℝ<VAR>hx₁ : Real.pi / 2 ≤ x<VAR>hx₂ : x ≤ Real.pi + Real.pi / 2<GOAL>Real.cos x ≤ 0
<VAR>x : ℝ<VAR>hl : 0 ≤ x<VAR>hu : x ≤ Real.pi<GOAL>Real.sin x = √(1 - Real.cos x ^ 2)
<VAR>x : ℝ<VAR>hl : -(Real.pi / 2) ≤ x<VAR>hu : x ≤ Real.pi / 2<GOAL>Real.cos x = √(1 - Real.sin x ^ 2)
<VAR>x : ℝ<VAR>hl : -Real.pi ≤ x<VAR>hr : x ≤ Real.pi<GOAL>Real.cos (x / 2) = √((1 + Real.cos x) / 2)
<VAR>x : ℝ<GOAL>|Real.sin (x / 2)| = √((1 - Real.cos x) / 2)
<VAR>x : ℝ<VAR>hl : 0 ≤ x<VAR>hr : x ≤ 2 * Real.pi<GOAL>Real.sin (x / 2) = √((1 - Real.cos x) / 2)
<VAR>x : ℝ<VAR>hl : -(2 * Real.pi) ≤ x<VAR>hr : x ≤ 0<GOAL>Real.sin (x / 2) = -√((1 - Real.cos x) / 2)
<VAR>x : ℝ<VAR>hx₁ : -Real.pi < x<VAR>hx₂ : x < Real.pi<GOAL>Real.sin x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>Real.sin x = 0 ↔ ∃ n, ↑n * Real.pi = x
<VAR>x : ℝ<GOAL>Real.sin x ≠ 0 ↔ ∀ (n : ℤ), ↑n * Real.pi ≠ x
<VAR>x : ℝ<GOAL>Real.sin x = 0 ↔ Real.cos x = 1 ∨ Real.cos x = -1
<VAR>x : ℝ<GOAL>Real.cos x = 1 ↔ ∃ n, ↑n * (2 * Real.pi) = x
<VAR>x : ℝ<VAR>hx₁ : -(2 * Real.pi) < x<VAR>hx₂ : x < 2 * Real.pi<GOAL>Real.cos x = 1 ↔ x = 0
<VAR>x y : ℝ<VAR>hx₁ : -(Real.pi / 2) ≤ x<VAR>hy₂ : y ≤ Real.pi / 2<VAR>hxy : x < y<GOAL>Real.sin x < Real.sin y
<GOAL>StrictMonoOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y ≤ Real.pi<VAR>hxy : x < y<GOAL>Real.cos y < Real.cos x
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y ≤ Real.pi / 2<VAR>hxy : x < y<GOAL>Real.cos y < Real.cos x
<GOAL>StrictAntiOn Real.cos (Set.Icc 0 Real.pi)
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y ≤ Real.pi<VAR>hxy : x ≤ y<GOAL>Real.cos y ≤ Real.cos x
<VAR>x y : ℝ<VAR>hx₁ : -(Real.pi / 2) ≤ x<VAR>hy₂ : y ≤ Real.pi / 2<VAR>hxy : x ≤ y<GOAL>Real.sin x ≤ Real.sin y
<GOAL>Set.InjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
<GOAL>Set.InjOn Real.cos (Set.Icc 0 Real.pi)
<GOAL>Set.SurjOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
<GOAL>Set.SurjOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
<VAR>x : ℝ<GOAL>Real.sin x ∈ Set.Icc (-1) 1
<VAR>x : ℝ<GOAL>Real.cos x ∈ Set.Icc (-1) 1
<VAR>s : Set ℝ<GOAL>Set.MapsTo Real.sin s (Set.Icc (-1) 1)
<VAR>s : Set ℝ<GOAL>Set.MapsTo Real.cos s (Set.Icc (-1) 1)
<GOAL>Set.BijOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) (Set.Icc (-1) 1)
<GOAL>Set.BijOn Real.cos (Set.Icc 0 Real.pi) (Set.Icc (-1) 1)
<GOAL>Set.range Real.cos = Set.Icc (-1) 1
<GOAL>Set.range Real.sin = Set.Icc (-1) 1
<VAR>x : ℝ<GOAL>x.sqrtTwoAddSeries 0 = x
<GOAL>Real.sqrtTwoAddSeries 0 1 = √2
<GOAL>Real.sqrtTwoAddSeries 0 2 = √(2 + √2)
<VAR>n : ℕ<GOAL>0 ≤ Real.sqrtTwoAddSeries 0 n
<VAR>x : ℝ<VAR>h : 0 ≤ x<VAR>n : ℕ<GOAL>0 ≤ x.sqrtTwoAddSeries n
<VAR>n : ℕ<GOAL>Real.sqrtTwoAddSeries 0 n < 2
<VAR>x : ℝ<VAR>n : ℕ<GOAL>x.sqrtTwoAddSeries (n + 1) = (√(2 + x)).sqrtTwoAddSeries n
<VAR>x y : ℝ<VAR>h : x ≤ y<VAR>n : ℕ<GOAL>x.sqrtTwoAddSeries n ≤ y.sqrtTwoAddSeries n
<VAR>n : ℕ<GOAL>Real.cos (Real.pi / 2 ^ (n + 1)) = Real.sqrtTwoAddSeries 0 n / 2
<VAR>n : ℕ<GOAL>Real.sin (Real.pi / 2 ^ (n + 1)) ^ 2 = 1 - (Real.sqrtTwoAddSeries 0 n / 2) ^ 2
<VAR>n : ℕ<GOAL>Real.sin (Real.pi / 2 ^ (n + 2)) ^ 2 = 1 / 2 - Real.sqrtTwoAddSeries 0 n / 4
<VAR>n : ℕ<GOAL>Real.sin (Real.pi / 2 ^ (n + 2)) = √(2 - Real.sqrtTwoAddSeries 0 n) / 2
<GOAL>Real.cos (Real.pi / 4) = √2 / 2
<GOAL>Real.sin (Real.pi / 4) = √2 / 2
<GOAL>Real.cos (Real.pi / 8) = √(2 + √2) / 2
<GOAL>Real.sin (Real.pi / 8) = √(2 - √2) / 2
<GOAL>Real.cos (Real.pi / 16) = √(2 + √(2 + √2)) / 2
<GOAL>Real.sin (Real.pi / 16) = √(2 - √(2 + √2)) / 2
<GOAL>Real.cos (Real.pi / 32) = √(2 + √(2 + √(2 + √2))) / 2
<GOAL>Real.sin (Real.pi / 32) = √(2 - √(2 + √(2 + √2))) / 2
<GOAL>Real.cos (Real.pi / 3) = 1 / 2
<GOAL>Real.cos (Real.pi / 6) = √3 / 2
<GOAL>Real.cos (Real.pi / 6) ^ 2 = 3 / 4
<GOAL>Real.sin (Real.pi / 6) = 1 / 2
<GOAL>Real.sin (Real.pi / 3) ^ 2 = 3 / 4
<GOAL>Real.sin (Real.pi / 3) = √3 / 2
<VAR>x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))<GOAL>↑(Real.sinOrderIso x) = Real.sin ↑x
<VAR>x : ↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2))<GOAL>Real.sinOrderIso x = ⟨Real.sin ↑x, ⋯⟩
<GOAL>Real.tan (Real.pi / 6) = 1 / √3
<VAR>x : ℝ<VAR>h0x : 0 < x<VAR>hxp : x < Real.pi / 2<GOAL>0 < Real.tan x
<VAR>x : ℝ<VAR>h0x : 0 ≤ x<VAR>hxp : x ≤ Real.pi / 2<GOAL>0 ≤ Real.tan x
<VAR>x : ℝ<VAR>hx0 : x < 0<VAR>hpx : -(Real.pi / 2) < x<GOAL>Real.tan x < 0
<VAR>x : ℝ<VAR>hx0 : x ≤ 0<VAR>hpx : -(Real.pi / 2) ≤ x<GOAL>Real.tan x ≤ 0
<GOAL>StrictMonoOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
<VAR>x y : ℝ<VAR>hx₁ : -(Real.pi / 2) < x<VAR>hy₂ : y < Real.pi / 2<VAR>hxy : x < y<GOAL>Real.tan x < Real.tan y
<VAR>x y : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hy₂ : y < Real.pi / 2<VAR>hxy : x < y<GOAL>Real.tan x < Real.tan y
<GOAL>Set.InjOn Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))
<VAR>x y : ℝ<VAR>hx₁ : -(Real.pi / 2) < x<VAR>hx₂ : x < Real.pi / 2<VAR>hy₁ : -(Real.pi / 2) < y<VAR>hy₂ : y < Real.pi / 2<VAR>hxy : Real.tan x = Real.tan y<GOAL>x = y
<VAR>x : ℝ<GOAL>Real.tan (x + Real.pi) = Real.tan x
<VAR>x : ℝ<GOAL>Real.tan (x - Real.pi) = Real.tan x
<VAR>x : ℝ<GOAL>Real.tan (Real.pi - x) = -Real.tan x
<VAR>x : ℝ<GOAL>Real.tan (Real.pi / 2 - x) = (Real.tan x)⁻¹
<VAR>n : ℕ<GOAL>Real.tan (↑n * Real.pi) = 0
<VAR>n : ℤ<GOAL>Real.tan (↑n * Real.pi) = 0
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.tan (x + ↑n * Real.pi) = Real.tan x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.tan (x + ↑n * Real.pi) = Real.tan x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.tan (x - ↑n * Real.pi) = Real.tan x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.tan (x - ↑n * Real.pi) = Real.tan x
<VAR>x : ℝ<VAR>n : ℕ<GOAL>Real.tan (↑n * Real.pi - x) = -Real.tan x
<VAR>x : ℝ<VAR>n : ℤ<GOAL>Real.tan (↑n * Real.pi - x) = -Real.tan x
<GOAL>Filter.Tendsto Real.sin (𝓝[<] (Real.pi / 2)) (𝓝 1)
<GOAL>Filter.Tendsto Real.cos (𝓝[<] (Real.pi / 2)) (𝓝[>] 0)
<GOAL>Filter.Tendsto Real.tan (𝓝[<] (Real.pi / 2)) Filter.atTop
<GOAL>Filter.Tendsto Real.sin (𝓝[>] (-(Real.pi / 2))) (𝓝 (-1))
<GOAL>Filter.Tendsto Real.cos (𝓝[>] (-(Real.pi / 2))) (𝓝[>] 0)
<GOAL>Filter.Tendsto Real.tan (𝓝[>] (-(Real.pi / 2))) Filter.atBot
<VAR>z : ℂ<GOAL>Complex.sin z = 0 ↔ Complex.cos z = 1 ∨ Complex.cos z = -1
<GOAL>Complex.sin (2 * ↑Real.pi) = 0
<GOAL>Complex.cos (2 * ↑Real.pi) = 1
<GOAL>Function.Periodic Complex.sin (2 * ↑Real.pi)
<VAR>x : ℂ<GOAL>Complex.sin (x + ↑Real.pi) = -Complex.sin x
<VAR>x : ℂ<GOAL>Complex.sin (x + 2 * ↑Real.pi) = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.sin (x - ↑Real.pi) = -Complex.sin x
<VAR>x : ℂ<GOAL>Complex.sin (x - 2 * ↑Real.pi) = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.sin (↑Real.pi - x) = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.sin (2 * ↑Real.pi - x) = -Complex.sin x
<VAR>n : ℕ<GOAL>Complex.sin (↑n * ↑Real.pi) = 0
<VAR>n : ℤ<GOAL>Complex.sin (↑n * ↑Real.pi) = 0
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.sin (x + ↑n * (2 * ↑Real.pi)) = Complex.sin x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.sin (x - ↑n * (2 * ↑Real.pi)) = Complex.sin x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.sin (↑n * (2 * ↑Real.pi) - x) = -Complex.sin x
<GOAL>Function.Periodic Complex.cos (2 * ↑Real.pi)
<VAR>x : ℂ<GOAL>Complex.cos (x + ↑Real.pi) = -Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (x + 2 * ↑Real.pi) = Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (x - ↑Real.pi) = -Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (x - 2 * ↑Real.pi) = Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (↑Real.pi - x) = -Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (2 * ↑Real.pi - x) = Complex.cos x
<VAR>n : ℕ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi)) = 1
<VAR>n : ℤ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi)) = 1
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.cos (x + ↑n * (2 * ↑Real.pi)) = Complex.cos x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.cos (x - ↑n * (2 * ↑Real.pi)) = Complex.cos x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x
<VAR>n : ℕ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
<VAR>n : ℤ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
<VAR>n : ℕ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
<VAR>n : ℤ<GOAL>Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
<VAR>x : ℂ<GOAL>Complex.sin (x + ↑Real.pi / 2) = Complex.cos x
<VAR>x : ℂ<GOAL>Complex.sin (x - ↑Real.pi / 2) = -Complex.cos x
<VAR>x : ℂ<GOAL>Complex.sin (↑Real.pi / 2 - x) = Complex.cos x
<VAR>x : ℂ<GOAL>Complex.cos (x + ↑Real.pi / 2) = -Complex.sin x
<VAR>x : ℂ<GOAL>Complex.cos (x - ↑Real.pi / 2) = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.cos (↑Real.pi / 2 - x) = Complex.sin x
<VAR>x : ℂ<GOAL>Complex.tan (x + ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<GOAL>Complex.tan (x - ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<GOAL>Complex.tan (↑Real.pi - x) = -Complex.tan x
<VAR>x : ℂ<GOAL>Complex.tan (↑Real.pi / 2 - x) = (Complex.tan x)⁻¹
<VAR>n : ℕ<GOAL>Complex.tan (↑n * ↑Real.pi) = 0
<VAR>n : ℤ<GOAL>Complex.tan (↑n * ↑Real.pi) = 0
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.tan (x + ↑n * ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.tan (x - ↑n * ↑Real.pi) = Complex.tan x
<VAR>x : ℂ<VAR>n : ℕ<GOAL>Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x
<VAR>x : ℂ<VAR>n : ℤ<GOAL>Complex.tan (↑n * ↑Real.pi - x) = -Complex.tan x
<GOAL>Function.Antiperiodic Complex.exp (↑Real.pi * Complex.I)
<GOAL>Function.Periodic Complex.exp (2 * ↑Real.pi * Complex.I)
<GOAL>Function.Antiperiodic (fun x => Complex.exp (x * Complex.I)) ↑Real.pi
<GOAL>Function.Periodic (fun x => Complex.exp (x * Complex.I)) (2 * ↑Real.pi)
<GOAL>Complex.exp (↑Real.pi * Complex.I) = -1
<GOAL>Complex.exp (2 * ↑Real.pi * Complex.I) = 1
<VAR>n : ℕ<GOAL>Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1
<VAR>n : ℤ<GOAL>Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1
<VAR>z : ℂ<GOAL>Complex.exp (z + ↑Real.pi * Complex.I) = -Complex.exp z
<VAR>z : ℂ<GOAL>Complex.exp (z - ↑Real.pi * Complex.I) = -Complex.exp z
<VAR>a b : ℝ<VAR>ha : a ≤ 0<VAR>z : ℂ<VAR>hz : |z.im| ≤ b<VAR>hb : b ≤ Real.pi / 2<GOAL>Complex.abs (Complex.exp (↑a * (Complex.exp z + Complex.exp (-z)))) ≤ Real.exp (a * Real.cos b * Real.exp |z.re|)
<VAR>x z : ℂ<VAR>hz : ‖z‖ ≤ 1<GOAL>‖Complex.exp (x + z) - Complex.exp x - z • Complex.exp x‖ ≤ ‖Complex.exp x‖ * ‖z‖ ^ 2
<VAR>r : ℝ<VAR>hr_nonneg : 0 ≤ r<VAR>hr_le : r ≤ 1<VAR>x y : ℂ<VAR>hyx : ‖y - x‖ < r<GOAL>‖Complex.exp y - Complex.exp x‖ ≤ (1 + r) * ‖Complex.exp x‖ * ‖y - x‖
<VAR>s : Set ℂ<GOAL>ContinuousOn Complex.exp s
<VAR>n : ℕ<GOAL>(fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>n : ℕ<GOAL>(fun x => Complex.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i !) =o[𝓝 0] fun x => x ^ n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<VAR>z : ℂ<VAR>hf : Filter.Tendsto f l (𝓝 z)<GOAL>Filter.Tendsto (fun x => Complex.exp (f x)) l (𝓝 (Complex.exp z))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun y => Complex.exp (f y)) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>x : α<VAR>h : ContinuousAt f x<GOAL>ContinuousAt (fun y => Complex.exp (f y)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun y => Complex.exp (f y)) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℂ<VAR>h : Continuous f<GOAL>Continuous fun y => Complex.exp (f y)
<VAR>s : Set ℝ<GOAL>ContinuousOn Real.exp s
<VAR>n : ℕ<GOAL>(fun x => Real.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>n : ℕ<GOAL>(fun x => Real.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i !) =o[𝓝 0] fun x => x ^ n
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<VAR>z : ℝ<VAR>hf : Filter.Tendsto f l (𝓝 z)<GOAL>Filter.Tendsto (fun x => Real.exp (f x)) l (𝓝 (Real.exp z))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (fun y => Real.exp (f y)) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>x : α<VAR>h : ContinuousAt f x<GOAL>ContinuousAt (fun y => Real.exp (f y)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : ContinuousOn f s<GOAL>ContinuousOn (fun y => Real.exp (f y)) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>f : α → ℝ<VAR>h : Continuous f<GOAL>Continuous fun y => Real.exp (f y)
<VAR>x : ℝ<GOAL>Real.exp (x / 2) = √(Real.exp x)
<GOAL>Filter.Tendsto (fun x => Real.exp (-x)) Filter.atTop (𝓝 0)
<GOAL>Filter.Tendsto Real.exp (𝓝 0) (𝓝 1)
<GOAL>Filter.Tendsto Real.exp Filter.atBot (𝓝 0)
<GOAL>Filter.Tendsto Real.exp Filter.atBot (𝓝[>] 0)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun x => Real.exp (f x)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>(Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => Real.exp (f x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => Real.exp x / x ^ n) Filter.atTop Filter.atTop
<VAR>n : ℕ<GOAL>Filter.Tendsto (fun x => x ^ n * Real.exp (-x)) Filter.atTop (𝓝 0)
<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 < b<GOAL>Filter.Tendsto (fun x => (b * Real.exp x + c) / x ^ n) Filter.atTop Filter.atTop
<VAR>b c : ℝ<VAR>n : ℕ<VAR>hb : 0 ≠ b<GOAL>Filter.Tendsto (fun x => x ^ n / (b * Real.exp x + c)) Filter.atTop (𝓝 0)
<VAR>x : ℝ<GOAL>↑(Real.expOrderIso x) = Real.exp x
<GOAL>Subtype.val ∘ ⇑Real.expOrderIso = Real.exp
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Filter.Tendsto (fun x => Real.exp (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : ℝ → α<GOAL>Filter.Tendsto (fun x => f (Real.exp x)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
<GOAL>Filter.map Real.exp Filter.atBot = 𝓝[>] 0
<GOAL>Filter.comap Real.exp (𝓝[>] 0) = Filter.atBot
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : ℝ → α<GOAL>Filter.Tendsto (fun x => f (Real.exp x)) Filter.atBot l ↔ Filter.Tendsto f (𝓝[>] 0) l
<GOAL>Filter.comap Real.exp (𝓝 0) = Filter.atBot
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Filter.Tendsto (fun x => Real.exp (f x)) l (𝓝 0) ↔ Filter.Tendsto f l Filter.atBot
<VAR>x : ℝ<GOAL>Filter.map Real.exp (𝓝 x) = 𝓝 (Real.exp x)
<VAR>x : ℝ<GOAL>Filter.comap Real.exp (𝓝 (Real.exp x)) = 𝓝 x
<VAR>n : ℕ<GOAL>(fun x => x ^ n) =o[Filter.atTop] Real.exp
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>((fun x => Real.exp (f x)) =O[l] fun x => Real.exp (g x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (f - g)
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>((fun x => Real.exp (f x)) =Θ[l] fun x => Real.exp (g x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x - g x|
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>((fun x => Real.exp (f x)) =o[l] fun x => Real.exp (g x)) ↔ Filter.Tendsto (fun x => g x - f x) l Filter.atTop
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => 1) =o[l] fun x => Real.exp (f x)) ↔ Filter.Tendsto f l Filter.atTop
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => 1) =O[l] fun x => Real.exp (f x)) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => Real.exp (f x)) =O[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>((fun x => Real.exp (f x)) =Θ[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x|
<VAR>a : ℝ<GOAL>(Summable fun n => Real.exp (↑n * a)) ↔ a < 0
<VAR>k : ℕ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Summable fun n => ↑n ^ k * Real.exp (-r * ↑n)
<VAR>ι : Type u_1<VAR>f : ι → ℝ<VAR>a : ℝ<VAR>h : HasSum f a<GOAL>HasProd (Real.exp ∘ f) (Real.exp a)
<GOAL>Filter.comap Complex.exp (Bornology.cobounded ℂ) = Filter.comap Complex.re Filter.atTop
<GOAL>Filter.comap Complex.exp (𝓝 0) = Filter.comap Complex.re Filter.atBot
<GOAL>Filter.comap Complex.exp (𝓝[≠] 0) = Filter.comap Complex.re Filter.atBot
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℂ<GOAL>Filter.Tendsto (fun x => Complex.exp (f x)) l (𝓝 0) ↔ Filter.Tendsto (fun x => (f x).re) l Filter.atBot
<GOAL>Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atTop) (Bornology.cobounded ℂ)