ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (𝓝 0)
<GOAL>Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (𝓝[≠] 0)
<VAR>ι : Type u_1<VAR>f : ι → ℂ<VAR>a : ℂ<VAR>h : HasSum f a<GOAL>HasProd (Complex.exp ∘ f) (Complex.exp a)
<VAR>s : ℂ<GOAL>s.Gammaℝ = ↑π ^ (-s / 2) * Complex.Gamma (s / 2)
<VAR>s : ℂ<GOAL>s.Gammaℂ = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s
<GOAL>Complex.Gammaℂ 1 = 1 / ↑π
<GOAL>Filter.Tendsto (fun s => s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
<VAR>s : ℂ<GOAL>(1 - s).Gammaℝ * (1 + s).Gammaℝ = (Complex.cos (↑π * s / 2))⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)<GOAL>s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * Complex.cos (↑π * s / 2)
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>(1 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹
<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>(2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹
<VAR>c : ℝ<GOAL>MeasureTheory.IntegrableOn rexp (Set.Iic c) MeasureTheory.volume
<VAR>c : ℝ<GOAL>∫ (x : ℝ) in Set.Iic c, rexp x = rexp c
<GOAL>∫ (x : ℝ) in Set.Iic 0, rexp x = 1
<VAR>c : ℝ<GOAL>∫ (x : ℝ) in Set.Ioi c, rexp (-x) = rexp (-c)
<GOAL>∫ (x : ℝ) in Set.Ioi 0, rexp (-x) = 1
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>MeasureTheory.IntegrableOn (fun t => t ^ a) (Set.Ioi c) MeasureTheory.volume
<VAR>s t : ℝ<VAR>ht : 0 < t<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioi t) MeasureTheory.volume ↔ s < -1
<VAR>s : ℝ<GOAL>¬MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioi 0) MeasureTheory.volume
<VAR>s : ℝ<GOAL>∫ (x : ℝ) in Set.Ioi 0, x ^ s = 0
<VAR>a : ℝ<VAR>ha : a < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∫ (t : ℝ) in Set.Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>MeasureTheory.IntegrableOn (fun t => ↑t ^ a) (Set.Ioi c) MeasureTheory.volume
<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioi t) MeasureTheory.volume ↔ s.re < -1
<VAR>s : ℂ<GOAL>¬MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioi 0) MeasureTheory.volume
<VAR>s : ℂ<GOAL>∫ (x : ℝ) in Set.Ioi 0, ↑x ^ s = 0
<VAR>a : ℂ<VAR>ha : a.re < -1<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∫ (t : ℝ) in Set.Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)
<GOAL>MeasureTheory.Integrable (fun x => (1 + x ^ 2)⁻¹) MeasureTheory.volume
<VAR>i : ℝ<GOAL>∫ (x : ℝ) in Set.Iic i, (1 + x ^ 2)⁻¹ = Real.arctan i + π / 2
<VAR>i : ℝ<GOAL>∫ (x : ℝ) in Set.Ioi i, (1 + x ^ 2)⁻¹ = π / 2 - Real.arctan i
<GOAL>∫ (x : ℝ), (1 + x ^ 2)⁻¹ = π
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>x : E<GOAL>√(1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>x : E<GOAL>1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>(1 + ‖x‖ ^ 2) ^ (-r / 2) ≤ 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 0 < t<VAR>x : E<GOAL>t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 1 < t<GOAL>Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅
<VAR>r : ℝ<VAR>n : ℕ<VAR>hnr : ↑n < r<GOAL>∫⁻ (x : ℝ) in Set.Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(FiniteDimensional.finrank ℝ E) < r<GOAL>∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(FiniteDimensional.finrank ℝ E) < r<GOAL>MeasureTheory.Integrable (fun x => (1 + ‖x‖) ^ (-r)) μ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(FiniteDimensional.finrank ℝ E) < r<GOAL>MeasureTheory.Integrable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ
<VAR>x : ℂ<GOAL>HasStrictDerivAt Complex.sin (Complex.cos x) x
<VAR>x : ℂ<GOAL>HasDerivAt Complex.sin (Complex.cos x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℂ n Complex.sin
<VAR>x : ℂ<GOAL>DifferentiableAt ℂ Complex.sin x
<VAR>x : ℂ<GOAL>HasStrictDerivAt Complex.cos (-Complex.sin x) x
<VAR>x : ℂ<GOAL>HasDerivAt Complex.cos (-Complex.sin x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℂ n Complex.cos
<VAR>x : ℂ<GOAL>DifferentiableAt ℂ Complex.cos x
<VAR>x : ℂ<GOAL>deriv Complex.cos x = -Complex.sin x
<VAR>x : ℂ<GOAL>HasStrictDerivAt Complex.sinh (Complex.cosh x) x
<VAR>x : ℂ<GOAL>HasDerivAt Complex.sinh (Complex.cosh x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℂ n Complex.sinh
<VAR>x : ℂ<GOAL>DifferentiableAt ℂ Complex.sinh x
<VAR>x : ℂ<GOAL>HasStrictDerivAt Complex.cosh (Complex.sinh x) x
<VAR>x : ℂ<GOAL>HasDerivAt Complex.cosh (Complex.sinh x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℂ n Complex.cosh
<VAR>x : ℂ<GOAL>DifferentiableAt ℂ Complex.cosh x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>s : Set ℂ<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>derivWithin (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) * derivWithin f s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>hc : DifferentiableAt ℂ f x<GOAL>deriv (fun x => Complex.cos (f x)) x = -Complex.sin (f x) * deriv f x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) * f') s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>s : Set ℂ<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>derivWithin (fun x => Complex.sin (f x)) s x = Complex.cos (f x) * derivWithin f s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>hc : DifferentiableAt ℂ f x<GOAL>deriv (fun x => Complex.sin (f x)) x = Complex.cos (f x) * deriv f x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) * f') s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>s : Set ℂ<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>derivWithin (fun x => Complex.cosh (f x)) s x = Complex.sinh (f x) * derivWithin f s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>hc : DifferentiableAt ℂ f x<GOAL>deriv (fun x => Complex.cosh (f x)) x = Complex.sinh (f x) * deriv f x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') x
<VAR>f : ℂ → ℂ<VAR>f' x : ℂ<VAR>s : Set ℂ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) * f') s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>s : Set ℂ<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>derivWithin (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) * derivWithin f s x
<VAR>f : ℂ → ℂ<VAR>x : ℂ<VAR>hc : DifferentiableAt ℂ f x<GOAL>deriv (fun x => Complex.sinh (f x)) x = Complex.cosh (f x) * deriv f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<GOAL>DifferentiableWithinAt ℂ (fun x => Complex.cos (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>DifferentiableAt ℂ (fun x => Complex.cos (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>hc : DifferentiableOn ℂ f s<GOAL>DifferentiableOn ℂ (fun x => Complex.cos (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>hc : Differentiable ℂ f<GOAL>Differentiable ℂ fun x => Complex.cos (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>fderivWithin ℂ (fun x => Complex.cos (f x)) s x = -Complex.sin (f x) • fderivWithin ℂ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>fderiv ℂ (fun x => Complex.cos (f x)) x = -Complex.sin (f x) • fderiv ℂ f x
<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 => Complex.cos (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℂ n f x<GOAL>ContDiffAt ℂ n (fun x => Complex.cos (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℂ n f s<GOAL>ContDiffOn ℂ n (fun x => Complex.cos (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℂ n f s x<GOAL>ContDiffWithinAt ℂ n (fun x => Complex.cos (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Complex.sin (f x)) (Complex.cos (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<GOAL>DifferentiableWithinAt ℂ (fun x => Complex.sin (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>DifferentiableAt ℂ (fun x => Complex.sin (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>hc : DifferentiableOn ℂ f s<GOAL>DifferentiableOn ℂ (fun x => Complex.sin (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>hc : Differentiable ℂ f<GOAL>Differentiable ℂ fun x => Complex.sin (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>fderivWithin ℂ (fun x => Complex.sin (f x)) s x = Complex.cos (f x) • fderivWithin ℂ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>fderiv ℂ (fun x => Complex.sin (f x)) x = Complex.cos (f x) • fderiv ℂ f x
<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 => Complex.sin (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℂ n f x<GOAL>ContDiffAt ℂ n (fun x => Complex.sin (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℂ n f s<GOAL>ContDiffOn ℂ n (fun x => Complex.sin (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℂ n f s x<GOAL>ContDiffWithinAt ℂ n (fun x => Complex.sin (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<GOAL>DifferentiableWithinAt ℂ (fun x => Complex.cosh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>DifferentiableAt ℂ (fun x => Complex.cosh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>hc : DifferentiableOn ℂ f s<GOAL>DifferentiableOn ℂ (fun x => Complex.cosh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>hc : Differentiable ℂ f<GOAL>Differentiable ℂ fun x => Complex.cosh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>fderivWithin ℂ (fun x => Complex.cosh (f x)) s x = Complex.sinh (f x) • fderivWithin ℂ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>fderiv ℂ (fun x => Complex.cosh (f x)) x = Complex.sinh (f x) • fderiv ℂ f x
<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 => Complex.cosh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℂ n f x<GOAL>ContDiffAt ℂ n (fun x => Complex.cosh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℂ n f s<GOAL>ContDiffOn ℂ n (fun x => Complex.cosh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℂ n f s x<GOAL>ContDiffWithinAt ℂ n (fun x => Complex.cosh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>f' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<GOAL>DifferentiableWithinAt ℂ (fun x => Complex.sinh (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>DifferentiableAt ℂ (fun x => Complex.sinh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>hc : DifferentiableOn ℂ f s<GOAL>DifferentiableOn ℂ (fun x => Complex.sinh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>hc : Differentiable ℂ f<GOAL>Differentiable ℂ fun x => Complex.sinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hxs : UniqueDiffWithinAt ℂ s x<GOAL>fderivWithin ℂ (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) • fderivWithin ℂ f s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>hc : DifferentiableAt ℂ f x<GOAL>fderiv ℂ (fun x => Complex.sinh (f x)) x = Complex.cosh (f x) • fderiv ℂ f x
<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 => Complex.sinh (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℂ n f x<GOAL>ContDiffAt ℂ n (fun x => Complex.sinh (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℂ n f s<GOAL>ContDiffOn ℂ n (fun x => Complex.sinh (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℂ n f s x<GOAL>ContDiffWithinAt ℂ n (fun x => Complex.sinh (f x)) s x
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.sin (Real.cos x) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.sin (Real.cos x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.sin
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.sin x
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.cos (-Real.sin x) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.cos (-Real.sin x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.cos
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.cos x
<VAR>x : ℝ<GOAL>deriv Real.cos x = -Real.sin x
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.sinh (Real.cosh x) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.sinh (Real.cosh x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.sinh
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.sinh x
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.cosh (Real.sinh x) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.cosh (Real.sinh x) x
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.cosh
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.cosh x
<VAR>x y : ℝ<GOAL>Real.sinh x = Real.sinh y ↔ x = y
<VAR>x y : ℝ<GOAL>Real.sinh x ≤ Real.sinh y ↔ x ≤ y
<VAR>x y : ℝ<GOAL>Real.sinh x < Real.sinh y ↔ x < y
<VAR>x : ℝ<GOAL>Real.sinh x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>Real.sinh x ≠ 0 ↔ x ≠ 0
<VAR>x : ℝ<GOAL>0 < Real.sinh x ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.sinh x ≤ 0 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>Real.sinh x < 0 ↔ x < 0
<VAR>x : ℝ<GOAL>0 ≤ Real.sinh x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>|Real.sinh x| = Real.sinh |x|
<GOAL>StrictMonoOn Real.cosh (Set.Ici 0)
<VAR>x y : ℝ<GOAL>Real.cosh x ≤ Real.cosh y ↔ |x| ≤ |y|
<VAR>x y : ℝ<GOAL>Real.cosh x < Real.cosh y ↔ |x| < |y|
<VAR>x : ℝ<GOAL>1 ≤ Real.cosh x
<VAR>x : ℝ<GOAL>1 < Real.cosh x ↔ x ≠ 0
<VAR>x : ℝ<GOAL>x ≤ Real.sinh x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>Real.sinh x ≤ x ↔ x ≤ 0
<VAR>x : ℝ<GOAL>x < Real.sinh x ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.sinh x < x ↔ x < 0
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) * f') s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.cos (f x)) s x = -Real.sin (f x) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.cos (f x)) x = -Real.sin (f x) * deriv f x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.sin (f x)) s x = Real.cos (f x) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.sin (f x)) x = Real.cos (f x) * deriv f x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.cosh (f x)) (Real.sinh (f x) * f') s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.cosh (f x)) s x = Real.sinh (f x) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.cosh (f x)) x = Real.sinh (f x) * deriv f x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.sinh (f x)) (Real.cosh (f x) * f') s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => Real.sinh (f x)) s x = Real.cosh (f x) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.sinh (f x)) x = Real.cosh (f x) * deriv f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<GOAL>DifferentiableWithinAt ℝ (fun x => Real.cos (f x)) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>hc : DifferentiableAt ℝ f x<GOAL>DifferentiableAt ℝ (fun x => Real.cos (f x)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>hc : DifferentiableOn ℝ f s<GOAL>DifferentiableOn ℝ (fun x => Real.cos (f x)) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>hc : Differentiable ℝ f<GOAL>Differentiable ℝ fun x => Real.cos (f x)