ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : R<VAR>n : ℤ<GOAL>(algebraMap R A) (Polynomial.eval x (Polynomial.Chebyshev.T R n)) = Polynomial.eval ((algebraMap R A) x) (Polynomial.Chebyshev.T A n)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>x : R<VAR>n : ℤ<GOAL>(algebraMap R A) (Polynomial.eval x (Polynomial.Chebyshev.U R n)) = Polynomial.eval ((algebraMap R A) x) (Polynomial.Chebyshev.U A n)
<VAR>x : ℝ<VAR>n : ℤ<GOAL>↑(Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.T ℂ n)
<VAR>x : ℝ<VAR>n : ℤ<GOAL>↑(Polynomial.eval x (Polynomial.Chebyshev.U ℝ n)) = Polynomial.eval (↑x) (Polynomial.Chebyshev.U ℂ n)
<VAR>θ : ℂ<VAR>n : ℤ<GOAL>Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.T ℂ n) = Complex.cos (↑n * θ)
<VAR>θ : ℂ<VAR>n : ℤ<GOAL>Polynomial.eval (Complex.cos θ) (Polynomial.Chebyshev.U ℂ n) * Complex.sin θ = Complex.sin ((↑n + 1) * θ)
<VAR>θ : ℝ<VAR>n : ℤ<GOAL>Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.T ℝ n) = Real.cos (↑n * θ)
<VAR>θ : ℝ<VAR>n : ℤ<GOAL>Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.U ℝ n) * Real.sin θ = Real.sin ((↑n + 1) * θ)
<VAR>x : ℝ<VAR>h : Real.cos x ≠ 0<GOAL>HasStrictDerivAt Real.tan (1 / Real.cos x ^ 2) x
<VAR>x : ℝ<VAR>h : Real.cos x ≠ 0<GOAL>HasDerivAt Real.tan (1 / Real.cos x ^ 2) x
<VAR>x : ℝ<VAR>hx : Real.cos x = 0<GOAL>Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin x {x}ᶜ) Filter.atTop
<VAR>k : ℤ<GOAL>Filter.Tendsto (fun x => |Real.tan x|) (nhdsWithin ((2 * ↑k + 1) * Real.pi / 2) {(2 * ↑k + 1) * Real.pi / 2}ᶜ) Filter.atTop
<VAR>x : ℝ<GOAL>ContinuousAt Real.tan x ↔ Real.cos x ≠ 0
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.tan x ↔ Real.cos x ≠ 0
<VAR>x : ℝ<GOAL>deriv Real.tan x = 1 / Real.cos x ^ 2
<VAR>n : ℕ∞<VAR>x : ℝ<GOAL>ContDiffAt ℝ n Real.tan x ↔ Real.cos x ≠ 0
<VAR>x : ℝ<VAR>h : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)<GOAL>HasDerivAt Real.tan (1 / Real.cos x ^ 2) x
<VAR>x : ℝ<VAR>h : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)<GOAL>DifferentiableAt ℝ Real.tan x
<VAR>x : ℝ<GOAL>HasStrictDerivAt Real.arctan (1 / (1 + x ^ 2)) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.arctan (1 / (1 + x ^ 2)) x
<VAR>x : ℝ<GOAL>HasDerivAt Real.arctan (1 + x ^ 2)⁻¹ x
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.arctan x
<GOAL>deriv Real.arctan = fun x => 1 / (1 + x ^ 2)
<VAR>n : ℕ∞<GOAL>ContDiff ℝ n Real.arctan
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
<VAR>f : ℝ → ℝ<VAR>f' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * 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.arctan (f x)) s x = 1 / (1 + f x ^ 2) * derivWithin f s x
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>hc : DifferentiableAt ℝ f x<GOAL>deriv (fun x => Real.arctan (f x)) x = 1 / (1 + f x ^ 2) * 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.arctan (f x)) ((1 / (1 + f x ^ 2)) • 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.arctan (f x)) ((1 / (1 + f x ^ 2)) • 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.arctan (f x)) ((1 / (1 + f x ^ 2)) • 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<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>fderivWithin ℝ (fun x => Real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) • 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 => Real.arctan (f x)) x = (1 / (1 + f x ^ 2)) • fderiv ℝ 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<GOAL>DifferentiableWithinAt ℝ (fun x => Real.arctan (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.arctan (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.arctan (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.arctan (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>h : ContDiffAt ℝ n f x<GOAL>ContDiffAt ℝ n (fun x => Real.arctan (f x)) 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 => Real.arctan (f x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>h : ContDiffWithinAt ℝ n f s x<GOAL>ContDiffWithinAt ℝ n (fun x => Real.arctan (f x)) s 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.arctan (f x)) s
<VAR>x : ℝ<GOAL>Real.arcsin x ∈ Set.Icc (-(π / 2)) (π / 2)
<GOAL>Set.range Real.arcsin = Set.Icc (-(π / 2)) (π / 2)
<VAR>x : ℝ<GOAL>Real.arcsin x ≤ π / 2
<VAR>x : ℝ<GOAL>-(π / 2) ≤ Real.arcsin x
<VAR>x : ℝ<GOAL>Real.arcsin ↑(Set.projIcc (-1) 1 ⋯ x) = Real.arcsin x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc (-1) 1<GOAL>Real.sin (Real.arcsin x) = x
<VAR>x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>Real.sin (Real.arcsin x) = x
<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc (-(π / 2)) (π / 2)<GOAL>Real.arcsin (Real.sin x) = x
<VAR>x : ℝ<VAR>hx₁ : -(π / 2) ≤ x<VAR>hx₂ : x ≤ π / 2<GOAL>Real.arcsin (Real.sin x) = x
<GOAL>StrictMonoOn Real.arcsin (Set.Icc (-1) 1)
<GOAL>Set.InjOn Real.arcsin (Set.Icc (-1) 1)
<VAR>x y : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<VAR>hy₁ : -1 ≤ y<VAR>hy₂ : y ≤ 1<GOAL>Real.arcsin x = Real.arcsin y ↔ x = y
<VAR>x : ℝ<GOAL>ContinuousAt Real.arcsin x
<VAR>x y : ℝ<VAR>h₁ : Real.sin x = y<VAR>h₂ : x ∈ Set.Icc (-(π / 2)) (π / 2)<GOAL>Real.arcsin y = x
<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>Real.arcsin x = π / 2
<VAR>x : ℝ<VAR>hx : x ≤ -1<GOAL>Real.arcsin x = -(π / 2)
<VAR>x : ℝ<GOAL>Real.arcsin (-x) = -Real.arcsin x
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Icc (-1) 1<VAR>hy : y ∈ Set.Icc (-(π / 2)) (π / 2)<GOAL>Real.arcsin x ≤ y ↔ x ≤ Real.sin y
<VAR>x y : ℝ<VAR>hy : y ∈ Set.Ico (-(π / 2)) (π / 2)<GOAL>Real.arcsin x ≤ y ↔ x ≤ Real.sin y
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Icc (-(π / 2)) (π / 2)<VAR>hy : y ∈ Set.Icc (-1) 1<GOAL>x ≤ Real.arcsin y ↔ Real.sin x ≤ y
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Ioc (-(π / 2)) (π / 2)<GOAL>x ≤ Real.arcsin y ↔ Real.sin x ≤ y
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Icc (-1) 1<VAR>hy : y ∈ Set.Icc (-(π / 2)) (π / 2)<GOAL>Real.arcsin x < y ↔ x < Real.sin y
<VAR>x y : ℝ<VAR>hy : y ∈ Set.Ioc (-(π / 2)) (π / 2)<GOAL>Real.arcsin x < y ↔ x < Real.sin y
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Icc (-(π / 2)) (π / 2)<VAR>hy : y ∈ Set.Icc (-1) 1<GOAL>x < Real.arcsin y ↔ Real.sin x < y
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Ico (-(π / 2)) (π / 2)<GOAL>x < Real.arcsin y ↔ Real.sin x < y
<VAR>x y : ℝ<VAR>hy : y ∈ Set.Ioo (-(π / 2)) (π / 2)<GOAL>Real.arcsin x = y ↔ x = Real.sin y
<VAR>x : ℝ<GOAL>0 ≤ Real.arcsin x ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>Real.arcsin x ≤ 0 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>Real.arcsin x = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>0 = Real.arcsin x ↔ x = 0
<VAR>x : ℝ<GOAL>0 < Real.arcsin x ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.arcsin x < 0 ↔ x < 0
<VAR>x : ℝ<GOAL>Real.arcsin x < π / 2 ↔ x < 1
<VAR>x : ℝ<GOAL>-(π / 2) < Real.arcsin x ↔ -1 < x
<VAR>x : ℝ<GOAL>Real.arcsin x = π / 2 ↔ 1 ≤ x
<VAR>x : ℝ<GOAL>π / 2 = Real.arcsin x ↔ 1 ≤ x
<VAR>x : ℝ<GOAL>π / 2 ≤ Real.arcsin x ↔ 1 ≤ x
<VAR>x : ℝ<GOAL>Real.arcsin x = -(π / 2) ↔ x ≤ -1
<VAR>x : ℝ<GOAL>-(π / 2) = Real.arcsin x ↔ x ≤ -1
<VAR>x : ℝ<GOAL>Real.arcsin x ≤ -(π / 2) ↔ x ≤ -1
<VAR>x : ℝ<GOAL>π / 4 ≤ Real.arcsin x ↔ √2 / 2 ≤ x
<GOAL>Set.MapsTo Real.sin (Set.Ioo (-(π / 2)) (π / 2)) (Set.Ioo (-1) 1)
<VAR>x : ℝ<GOAL>0 ≤ Real.cos (Real.arcsin x)
<VAR>x : ℝ<GOAL>Real.cos (Real.arcsin x) = √(1 - x ^ 2)
<VAR>x : ℝ<GOAL>Real.tan (Real.arcsin x) = x / √(1 - x ^ 2)
<VAR>x : ℝ<GOAL>Real.arccos x = π / 2 - Real.arcsin x
<VAR>x : ℝ<GOAL>Real.arcsin x = π / 2 - Real.arccos x
<VAR>x : ℝ<GOAL>Real.arccos x ≤ π
<VAR>x : ℝ<GOAL>0 ≤ Real.arccos x
<VAR>x : ℝ<GOAL>0 < Real.arccos x ↔ x < 1
<VAR>x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>Real.cos (Real.arccos x) = x
<VAR>x : ℝ<VAR>hx₁ : 0 ≤ x<VAR>hx₂ : x ≤ π<GOAL>Real.arccos (Real.cos x) = x
<VAR>x y : ℝ<VAR>hy₀ : 0 ≤ y<VAR>hy₁ : y ≤ π<VAR>hxy : x = Real.cos y<GOAL>Real.arccos x = y
<GOAL>StrictAntiOn Real.arccos (Set.Icc (-1) 1)
<GOAL>Set.InjOn Real.arccos (Set.Icc (-1) 1)
<VAR>x y : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<VAR>hy₁ : -1 ≤ y<VAR>hy₂ : y ≤ 1<GOAL>Real.arccos x = Real.arccos y ↔ x = y
<VAR>x : ℝ<GOAL>Real.arccos x = 0 ↔ 1 ≤ x
<VAR>x : ℝ<GOAL>Real.arccos x = π / 2 ↔ x = 0
<VAR>x : ℝ<GOAL>Real.arccos x = π ↔ x ≤ -1
<VAR>x : ℝ<GOAL>Real.arccos (-x) = π - Real.arccos x
<VAR>x : ℝ<VAR>hx : 1 ≤ x<GOAL>Real.arccos x = 0
<VAR>x : ℝ<VAR>hx : x ≤ -1<GOAL>Real.arccos x = π
<VAR>x : ℝ<GOAL>Real.sin (Real.arccos x) = √(1 - x ^ 2)
<VAR>x : ℝ<GOAL>Real.arccos x ≤ π / 2 ↔ 0 ≤ x
<VAR>x : ℝ<GOAL>Real.arccos x < π / 2 ↔ 0 < x
<VAR>x : ℝ<GOAL>Real.arccos x ≤ π / 4 ↔ √2 / 2 ≤ x
<VAR>x : ℝ<GOAL>Real.tan (Real.arccos x) = √(1 - x ^ 2) / x
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>Real.arccos x = Real.arcsin √(1 - x ^ 2)
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>Real.arcsin x = Real.arccos √(1 - x ^ 2)
<VAR>p : Polynomial ℝ<GOAL>Filter.Tendsto (fun x => Polynomial.eval x p / rexp x) Filter.atTop (𝓝 0)
<VAR>x : ℝ≥0∞<GOAL>x.log.exp = x
<VAR>x : EReal<VAR>y : ℝ<GOAL>(x * ↑y).exp = x.exp ^ y
<VAR>x : ℝ≥0∞<GOAL>ENNReal.logOrderIso x = x.log
<VAR>x : EReal<GOAL>EReal.expOrderIso x = x.exp
<GOAL>ENNReal.logOrderIso.symm = EReal.expOrderIso
<GOAL>EReal.expOrderIso.symm = ENNReal.logOrderIso
<VAR>x : ℝ≥0∞<GOAL>ENNReal.logHomeomorph x = x.log
<VAR>x : EReal<GOAL>EReal.expHomeomorph x = x.exp
<GOAL>ENNReal.logHomeomorph.symm = EReal.expHomeomorph
<GOAL>EReal.expHomeomorph.symm = ENNReal.logHomeomorph
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {f : α → ℝ≥0∞}, Measurable f → Measurable fun x => (f x).log
<VAR>α : Type u_1<GOAL>∀ {x : MeasurableSpace α} {f : α → EReal}, Measurable f → Measurable fun x => (f x).exp
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasStrictDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ Real.arcsin x
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasStrictDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.arcsin x
<VAR>x : ℝ<VAR>h : x ≠ -1<GOAL>HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Ici x) x
<VAR>x : ℝ<VAR>h : x ≠ 1<GOAL>HasDerivWithinAt Real.arcsin (1 / √(1 - x ^ 2)) (Set.Iic x) x
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ Real.arcsin (Set.Ici x) x ↔ x ≠ -1
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ Real.arcsin (Set.Iic x) x ↔ x ≠ 1
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1
<GOAL>deriv Real.arcsin = fun x => 1 / √(1 - x ^ 2)
<GOAL>DifferentiableOn ℝ Real.arcsin {-1, 1}ᶜ
<VAR>n : ℕ∞<GOAL>ContDiffOn ℝ n Real.arcsin {-1, 1}ᶜ
<VAR>x : ℝ<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasStrictDerivAt Real.arccos (-(1 / √(1 - x ^ 2))) x
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<GOAL>HasDerivAt Real.arccos (-(1 / √(1 - x ^ 2))) x
<VAR>x : ℝ<VAR>h₁ : x ≠ -1<VAR>h₂ : x ≠ 1<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.arccos x
<VAR>x : ℝ<VAR>h : x ≠ -1<GOAL>HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Ici x) x
<VAR>x : ℝ<VAR>h : x ≠ 1<GOAL>HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Iic x) x
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ Real.arccos (Set.Ici x) x ↔ x ≠ -1
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ Real.arccos (Set.Iic x) x ↔ x ≠ 1
<VAR>x : ℝ<GOAL>DifferentiableAt ℝ Real.arccos x ↔ x ≠ -1 ∧ x ≠ 1
<GOAL>deriv Real.arccos = fun x => -(1 / √(1 - x ^ 2))
<GOAL>DifferentiableOn ℝ Real.arccos {-1, 1}ᶜ
<VAR>n : ℕ∞<GOAL>ContDiffOn ℝ n Real.arccos {-1, 1}ᶜ
<VAR>x : ℝ<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n Real.arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
<VAR>δ ε : ℝ<GOAL>gronwallBound δ 0 ε = fun x => δ + ε * x
<VAR>δ K ε : ℝ<VAR>hK : K ≠ 0<GOAL>gronwallBound δ K ε = fun x => δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)
<VAR>δ K ε x : ℝ<GOAL>HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
<VAR>δ K ε x a : ℝ<GOAL>HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
<VAR>δ K ε : ℝ<GOAL>gronwallBound δ K ε 0 = δ
<VAR>δ K x : ℝ<GOAL>gronwallBound δ K 0 x = δ * rexp (K * x)
<VAR>K x : ℝ<GOAL>gronwallBound 0 K 0 x = 0
<VAR>δ K x : ℝ<GOAL>Continuous fun ε => gronwallBound δ K ε x
<VAR>f f' : ℝ → ℝ<VAR>δ K ε a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r<VAR>ha : f a ≤ δ<VAR>bound : ∀ x ∈ Set.Ico a b, f' x ≤ K * f x + ε<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → f x ≤ gronwallBound δ K ε (x - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f f' : ℝ → E<VAR>δ K ε a b : ℝ<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x<VAR>ha : ‖f a‖ ≤ δ<VAR>bound : ∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε<VAR>x : ℝ<GOAL>x ∈ Set.Icc a b → ‖f x‖ ≤ gronwallBound δ K ε (x - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t<VAR>f_bound : ∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t<VAR>g_bound : ∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>t : ℝ<GOAL>t ∈ Set.Icc a b → dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzWith K (v t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t<VAR>f_bound : ∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t<VAR>g_bound : ∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg<VAR>ha : dist (f a) (g a) ≤ δ<VAR>t : ℝ<GOAL>t ∈ Set.Icc a b → dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t<VAR>hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t<VAR>hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>t : ℝ<GOAL>t ∈ Set.Icc a b → dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzWith K (v t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t<VAR>ha : dist (f a) (g a) ≤ δ<VAR>t : ℝ<GOAL>t ∈ Set.Icc a b → dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t<VAR>hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t<VAR>hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t<VAR>ha : f a = g a<GOAL>Set.EqOn f g (Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t<VAR>hfs : ∀ t ∈ Set.Ioc a b, f t ∈ s t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t<VAR>hgs : ∀ t ∈ Set.Ioc a b, g t ∈ s t<VAR>hb : f b = g b<GOAL>Set.EqOn f g (Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b t₀ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>ht : t₀ ∈ Set.Ioo a b<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t<VAR>hfs : ∀ t ∈ Set.Ioo a b, f t ∈ s t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t<VAR>hgs : ∀ t ∈ Set.Ioo a b, g t ∈ s t<VAR>heq : f t₀ = g t₀<GOAL>Set.EqOn f g (Set.Icc a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b t₀ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>ht : t₀ ∈ Set.Ioo a b<VAR>hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<GOAL>Set.EqOn f g (Set.Ioo a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>t₀ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<GOAL>f =ᶠ[𝓝 t₀] g
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>v : ℝ → E → E<VAR>K : ℝ≥0<VAR>f g : ℝ → E<VAR>a b : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzWith K (v t)<VAR>hf : ContinuousOn f (Set.Icc a b)<VAR>hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t<VAR>hg : ContinuousOn g (Set.Icc a b)<VAR>hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t<VAR>ha : f a = g a<GOAL>Set.EqOn f g (Set.Icc a b)
<VAR>θ : ℂ<GOAL>Complex.cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑Real.pi / 2
<VAR>θ : ℂ<GOAL>Complex.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * ↑Real.pi / 2
<VAR>θ : ℂ<GOAL>Complex.sin θ = 0 ↔ ∃ k, θ = ↑k * ↑Real.pi
<VAR>θ : ℂ<GOAL>Complex.sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑Real.pi
<VAR>θ : ℂ<GOAL>Complex.tan θ = 0 ↔ ∃ k, ↑k * ↑Real.pi / 2 = θ
<VAR>θ : ℂ<GOAL>Complex.tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * ↑Real.pi / 2 ≠ θ
<VAR>n : ℤ<GOAL>Complex.tan (↑n * ↑Real.pi / 2) = 0
<VAR>θ : ℂ<VAR>hθ : Complex.cos θ ≠ 0<GOAL>Complex.tan θ = 0 ↔ ∃ k, ↑k * ↑Real.pi = θ
<VAR>x y : ℂ<GOAL>Complex.cos x = Complex.cos y ↔ ∃ k, y = 2 * ↑k * ↑Real.pi + x ∨ y = 2 * ↑k * ↑Real.pi - x
<VAR>x y : ℂ<GOAL>Complex.sin x = Complex.sin y ↔ ∃ k, y = 2 * ↑k * ↑Real.pi + x ∨ y = (2 * ↑k + 1) * ↑Real.pi - x
<VAR>x : ℂ<GOAL>Complex.cos x = 1 ↔ ∃ k, ↑k * (2 * ↑Real.pi) = x
<VAR>x : ℂ<GOAL>Complex.cos x = -1 ↔ ∃ k, ↑Real.pi + ↑k * (2 * ↑Real.pi) = x
<VAR>x : ℂ<GOAL>Complex.sin x = 1 ↔ ∃ k, ↑Real.pi / 2 + ↑k * (2 * ↑Real.pi) = x
<VAR>x : ℂ<GOAL>Complex.sin x = -1 ↔ ∃ k, -(↑Real.pi / 2) + ↑k * (2 * ↑Real.pi) = x
<VAR>x y : ℂ<VAR>h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨ (∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * ↑Real.pi / 2<GOAL>Complex.tan (x + y) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)
<VAR>x y : ℂ<VAR>h : (∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2<GOAL>Complex.tan (x + y) = (Complex.tan x + Complex.tan y) / (1 - Complex.tan x * Complex.tan y)
<VAR>z : ℂ<GOAL>Complex.tan (2 * z) = 2 * Complex.tan z / (1 - Complex.tan z ^ 2)
<VAR>x y : ℂ<VAR>h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y * Complex.I ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨ (∃ k, x = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, y * Complex.I = (2 * ↑l + 1) * ↑Real.pi / 2<GOAL>Complex.tan (x + y * Complex.I) = (Complex.tan x + Complex.tanh y * Complex.I) / (1 - Complex.tan x * Complex.tanh y * Complex.I)
<VAR>z : ℂ<VAR>h : ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), ↑z.im * Complex.I ≠ (2 * ↑l + 1) * ↑Real.pi / 2) ∨ (∃ k, ↑z.re = (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∃ l, ↑z.im * Complex.I = (2 * ↑l + 1) * ↑Real.pi / 2<GOAL>Complex.tan z = (Complex.tan ↑z.re + Complex.tanh ↑z.im * Complex.I) / (1 - Complex.tan ↑z.re * Complex.tanh ↑z.im * Complex.I)
<GOAL>ContinuousOn Complex.tan {x | Complex.cos x ≠ 0}
<VAR>z w : ℂ<GOAL>Complex.cos z = w ↔ Complex.exp (z * Complex.I) ^ 2 - 2 * w * Complex.exp (z * Complex.I) + 1 = 0
<VAR>θ : ℝ<GOAL>Real.cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * Real.pi / 2
<VAR>θ : ℝ<GOAL>Real.cos θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ (2 * ↑k + 1) * Real.pi / 2
<VAR>x y : ℝ<GOAL>Real.cos x = Real.cos y ↔ ∃ k, y = 2 * ↑k * Real.pi + x ∨ y = 2 * ↑k * Real.pi - x
<VAR>x y : ℝ<GOAL>Real.sin x = Real.sin y ↔ ∃ k, y = 2 * ↑k * Real.pi + x ∨ y = (2 * ↑k + 1) * Real.pi - x
<VAR>x : ℝ<GOAL>Real.cos x = -1 ↔ ∃ k, Real.pi + ↑k * (2 * Real.pi) = x
<VAR>x : ℝ<GOAL>Real.sin x = 1 ↔ ∃ k, Real.pi / 2 + ↑k * (2 * Real.pi) = x
<VAR>x : ℝ<GOAL>Real.sin x = -1 ↔ ∃ k, -(Real.pi / 2) + ↑k * (2 * Real.pi) = x
<VAR>θ : ℝ<GOAL>Real.tan θ = 0 ↔ ∃ k, ↑k * Real.pi / 2 = θ
<VAR>θ : ℝ<VAR>hθ : Real.cos θ ≠ 0<GOAL>Real.tan θ = 0 ↔ ∃ k, ↑k * Real.pi = θ
<VAR>θ : ℝ<GOAL>Real.tan θ ≠ 0 ↔ ∀ (k : ℤ), ↑k * Real.pi / 2 ≠ θ
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < 1<GOAL>x < Real.sin (Real.pi / 2 * x)
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>hx' : x ≤ 1<GOAL>x ≤ Real.sin (Real.pi / 2 * x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>hx' : x < Real.pi / 2<GOAL>2 / Real.pi * x < Real.sin x
<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>hx' : x ≤ Real.pi / 2<GOAL>2 / Real.pi * x ≤ Real.sin x
<VAR>z : ℂ<GOAL>z.cot = (cexp (2 * Complex.I * z) + 1) / (Complex.I * (1 - cexp (2 * Complex.I * z)))
<VAR>z : ℂ<GOAL>(↑π * z).cot = (cexp (2 * ↑π * Complex.I * z) + 1) / (Complex.I * (1 - cexp (2 * ↑π * Complex.I * z)))
<VAR>z : ℍ<GOAL>↑π * (↑π * ↑z).cot = ↑π * Complex.I - 2 * ↑π * Complex.I * ∑' (n : ℕ), cexp (2 * ↑π * Complex.I * ↑z) ^ n
<VAR>x : ℝ<GOAL>(↑x).exp = ENNReal.ofReal (Real.exp x)
<VAR>x : EReal<GOAL>x.exp = ⊤ ↔ x = ⊤
<VAR>a b : EReal<GOAL>a.exp < b.exp ↔ a < b
<VAR>a : EReal<GOAL>0 < a.exp ↔ ⊥ < a
<VAR>a : EReal<GOAL>a.exp < ⊤ ↔ a < ⊤
<VAR>a : EReal<GOAL>a.exp < 1 ↔ a < 0
<VAR>a : EReal<GOAL>1 < a.exp ↔ 0 < a
<VAR>a b : EReal<GOAL>a.exp ≤ b.exp ↔ a ≤ b
<VAR>a : EReal<GOAL>a.exp ≤ 1 ↔ a ≤ 0
<VAR>a : EReal<GOAL>1 ≤ a.exp ↔ 0 ≤ a
<VAR>x : EReal<GOAL>(-x).exp = x.exp⁻¹
<VAR>x y : EReal<GOAL>(x + y).exp = x.exp * y.exp
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>x y : V<GOAL>affineSegment R x y = segment R x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>affineSegment R x y = affineSegment R y x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>P : Type u_4<VAR>OrderedRing R<VAR>AddCommGroup V<VAR>Module R V<VAR>AddTorsor V P<VAR>x y : P<GOAL>x ∈ affineSegment R x y