awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
rw :
  (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * (↑(-r) : ℂ))) / Complex.I =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I
rw₁ : Complex.I ≠ 0
⊢ ∫ (t : ℝ) in -r..r, Complex.exp (Complex.I * (↑t : ℂ)) =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I

Tactic:
rw [integral_exp_mul_complex]

Premises used: integral_exp_mul_complex
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
⊢ (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * (↑(-r) : ℂ))) / Complex.I =
    (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
⊢ Complex.I ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
simp : -((Complex.sin (↑r : ℂ) * Complex.I - -Complex.sin (↑r : ℂ) * Complex.I) * Complex.I) = 2 * Complex.sin (↑r : ℂ)
⊢ (Complex.exp (Complex.I * (↑r : ℂ)) - Complex.exp (Complex.I * -(↑r : ℂ))) / Complex.I = 2 * (↑(sin r) : ℂ)

Tactic:
simp only [mul_comm Complex.I, Complex.exp_mul_I, Complex.cos_neg, Complex.sin_neg,
      add_sub_add_left_eq_sub, Complex.div_I, Complex.ofReal_sin]

Premises used: add_sub_add_left_eq_sub, Complex.cos_neg, Complex.div_I, mul_comm, Complex.ofReal_sin, Complex.sin_neg, Complex.exp_mul_I, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
rw :
  -(Complex.sin (↑r : ℂ) * (Complex.I * Complex.I) - -Complex.sin (↑r : ℂ) * (Complex.I * Complex.I)) =
    Complex.sin (↑r : ℂ) + Complex.sin (↑r : ℂ)
⊢ -((Complex.sin (↑r : ℂ) * Complex.I - -Complex.sin (↑r : ℂ) * Complex.I) * Complex.I) = 2 * Complex.sin (↑r : ℂ)

Tactic:
rw [sub_mul, mul_assoc, mul_assoc, two_mul]

Premises used: mul_assoc, two_mul, sub_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
⊢ -(Complex.sin (↑r : ℂ) * (Complex.I * Complex.I) - -Complex.sin (↑r : ℂ) * (Complex.I * Complex.I)) =
    Complex.sin (↑r : ℂ) + Complex.sin (↑r : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
rw : 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
⊢ ∫ (t : ℝ) in -r..r, Complex.exp ((↑t : ℂ) * Complex.I) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)

Tactic:
rw [integral_exp_mul_I_eq_sin]

Premises used: integral_exp_mul_I_eq_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
pos : ∀ (hr : r = 0), 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
neg : ∀ (hr : ¬r = 0), 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
hr : r = 0
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
hr : ¬r = 0
neg : 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sin r / r) : ℂ)
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sinc r) : ℂ)

Tactic:
rw [sinc_of_ne_zero hr]

Premises used: Real.sinc_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
hr : ¬r = 0
neg : 2 * sin r = 2 * r * (sin r / r)
⊢ 2 * (↑(sin r) : ℂ) = 2 * (↑r : ℂ) * (↑(sin r / r) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
r : ℝ
hr : ¬r = 0
⊢ 2 * sin r = 2 * r * (sin r / r)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
rw : b * log b - b - 0 = b * log b - b
hab : 0 < b
hderiv : ∀ x ∈ Set.Ioo 0 b, HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log x) x
ha : Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
hb : Filter.Tendsto (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x)
    (fa := 0) (fb := b * log b - b) (hint := intervalIntegrable_log')]

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto, intervalIntegral.intervalIntegrable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
⊢ b * log b - b - 0 = b * log b - b

Tactic:
abel
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
⊢ 0 < b

Tactic:
ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
⊢ 0 < b

Tactic:
exact ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
s : ℝ
hderiv : ∀ (hs : 0 < s), s < b → HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log s) s
⊢ s ∈ Set.Ioo 0 b → HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log s) s

Tactic:
⟨hs, _ ⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
s : ℝ
hs : 0 < s
right : s < b
⊢ HasDerivAt (fun (x : ℝ) ↦ x * log x - x) (log s) s

Tactic:
simpa using (hasDerivAt_mul_log hs.ne.symm).sub (hasDerivAt_id s)

Premises used: Real.hasDerivAt_mul_log, HasDerivAt.sub, Ne.symm, hasDerivAt_id, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Tactic:
simpa [mul_comm] using ((tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one).sub
      (tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id))

Premises used: Filter.tendsto_id, zero_lt_one, tendsto_nhdsWithin_of_tendsto_nhds, mul_comm, Filter.Tendsto.sub, tendsto_log_mul_rpow_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
funProp : b ≠ 0
funProp₁ : ∀ (x : ℝ), x ≠ 0
funProp₂ : b ≠ 0
funProp₃ funProp₄ : ∀ (x : ℝ), x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x * log x - x) b

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
ht : 0 < b
⊢ Filter.Tendsto (fun (x : ℝ) ↦ x * log x - x) (nhdsWithin b (Set.Iio b)) (nhds (b * log b - b))

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
inl : ∀ (h : b < 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
inr : ∀ (h : b = 0), ∫ (s : ℝ) in 0..b, log s = b * log b - b
inr₁ : ∀ (h : 0 < b), ∫ (s : ℝ) in 0..b, log s = b * log b - b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
rcases lt_trichotomy b 0 with h | h | h

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
arg : ∫ (s : ℝ) in 0..b, log s
| ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
arg 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
arg : fun (s : ℝ) ↦ log s
| ∫ (s : ℝ) in 0..b, log s

Tactic:
arg 1
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
t : ℝ
h₁ : log (-t)
| log t

Tactic:
rw [← log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
h₁ : ∀ (t : ℝ), log (-t)
| ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
arg 1; arg 1; intro t; rw [← log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
inl : ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
inl : -(-b * log b - -b) = b * log b - b
⊢ ∫ (t : ℝ) in 0..b, log (-t) = b * log b - b

Tactic:
rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
      integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]

Premises used: Iff.mpr, Real.log_neg_eq_log, intervalIntegral.integral_symm, integral_log_from_zero_of_pos, Left.neg_pos_iff, neg_zero, intervalIntegral.integral_comp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b < 0
⊢ -(-b * log b - -b) = b * log b - b

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : b = 0
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
integral_log_from_zero_of_pos h

Premises used: integral_log_from_zero_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
b : ℝ
h : 0 < b
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
exact integral_log_from_zero_of_pos h

Premises used: integral_log_from_zero_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a
hab : IntervalIntegrable log MeasureTheory.volume a 0
hbc : IntervalIntegrable log MeasureTheory.volume 0 b
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]

Premises used: intervalIntegral.integral_add_adjacent_intervals
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
rw : -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in a..0, log x) (∫ (x : ℝ) in 0..b, log x) = b * log b - a * log a - b + a

Tactic:
rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]

Premises used: intervalIntegral.integral_symm, integral_log_from_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ -(a * log a - a) + (b * log b - b) = b * log b - a * log a - b + a

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

Tactic:
intervalIntegrable_log'

Premises used: intervalIntegral.intervalIntegrable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume a 0

Tactic:
exact intervalIntegrable_log'

Premises used: intervalIntegral.intervalIntegrable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
intervalIntegrable_log'

Premises used: intervalIntegral.intervalIntegrable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ IntervalIntegrable log MeasureTheory.volume 0 b

Tactic:
exact intervalIntegrable_log'

Premises used: intervalIntegral.intervalIntegrable_log'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
rw : -cos b - -cos a = cos a - cos b
hderiv : (deriv fun (x : ℝ) ↦ -cos x) = sin
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -cos x) x
hcont : ContinuousOn sin [[a, b]]
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b

Tactic:
rw [integral_deriv_eq_sub' fun x => -cos x]

Premises used: Real.cos, intervalIntegral.integral_deriv_eq_sub', Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ -cos b - -cos a = cos a - cos b

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ (deriv fun (x : ℝ) ↦ -cos x) = sin

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ -cos x) x

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn sin [[a, b]]

Tactic:
continuousOn_sin

Premises used: Real.continuousOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn sin [[a, b]]

Tactic:
exact continuousOn_sin

Premises used: Real.continuousOn_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
hderiv : deriv sin = cos
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x
hcont : ContinuousOn cos [[a, b]]
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a

Tactic:
rw [integral_deriv_eq_sub']

Premises used: intervalIntegral.integral_deriv_eq_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ deriv sin = cos

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x

Tactic:
simp only [differentiableAt_sin, implies_true]

Premises used: implies_true, Real.differentiableAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Tactic:
continuousOn_cos

Premises used: Real.continuousOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ContinuousOn cos [[a, b]]

Tactic:
exact continuousOn_cos

Premises used: Real.continuousOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a b : ℝ
hderiv : ∀ x ∈ [[a, b]], HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
hint : IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ Complex.cos (z * (↑y : ℂ))) MeasureTheory.volume a b
⊢ ∫ (x : ℝ) in a..b, Complex.cos (z * (↑x : ℂ)) = Complex.sin (z * (↑b : ℂ)) / z - Complex.sin (z * (↑a : ℂ)) / z

Tactic:
apply integral_eq_sub_of_hasDerivAt

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous (Y := ℂ) fun (y : ℝ) ↦ Complex.cos (z * (↑y : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ Complex.cos (z * (↑y : ℂ))) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable <| by fun_prop

Premises used: Continuous.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a b x : ℝ
hderiv : x ∈ [[a, b]] → HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x
⊢ x ∈ [[a, b]] → HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a b x : ℝ
h : x ∈ [[a, b]]
⊢ HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)

Tactic:
have a := Complex.hasDerivAt_sin (↑x * z)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a_1 b x : ℝ
h : x ∈ [[a_1, b]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
⊢ HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)

Tactic:
have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a_1 b_1 x : ℝ
h : x ∈ [[a_1, b_1]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
b : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
⊢ HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (Complex.cos ((↑x : ℂ) * z) * z) (↑x : ℂ)

Tactic:
have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a_1 b_1 x : ℝ
h : x ∈ [[a_1, b_1]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
b : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
c : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (Complex.cos ((↑x : ℂ) * z) * z) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (↑y : ℂ) / z) (Complex.cos ((↑x : ℂ) * z) * z / z) x

Tactic:
have d := HasDerivAt.comp_ofReal (c.div_const z)
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
z : ℂ
hz : z ≠ 0
a_1 b_1 x : ℝ
h : x ∈ [[a_1, b_1]]
a : HasDerivAt Complex.sin (Complex.cos ((↑x : ℂ) * z)) ((↑x : ℂ) * z)
b : HasDerivAt (fun (y : ℂ) ↦ y * z) z (↑x : ℂ)
c : HasDerivAt (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (Complex.cos ((↑x : ℂ) * z) * z) (↑x : ℂ)
d : HasDerivAt (fun (y : ℝ) ↦ (Complex.sin ∘ fun (y : ℂ) ↦ y * z) (↑y : ℂ) / z) (Complex.cos ((↑x : ℂ) * z) * z / z) x
⊢ HasDerivAt (fun (b : ℝ) ↦ Complex.sin (z * (↑b : ℂ)) / z) (Complex.cos (z * (↑x : ℂ))) x

Tactic:
simpa [hz, mul_comm] using d

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 = sin b * cos b - sin a * cos a

Tactic:
simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
    integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
      continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable

Premises used: ContinuousOn.neg, Real.hasDerivAt_sin, sub_eq_add_neg, Real.continuousOn_cos, sq, Real.hasDerivAt_cos, intervalIntegral.integral_deriv_mul_eq_sub, Real.continuousOn_sin, neg_mul_eq_mul_neg, ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + HPow.hPow (β := ℕ) x 2) = arctan b - arctan a

Tactic:
integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
    (continuous_const.div ?_ fun x => ?_).continuousOn

Premises used: Continuous.continuousOn, continuous_const, Real.deriv_arctan, Real.differentiableAt_arctan, Continuous.div, intervalIntegral.integral_deriv_eq_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
refine_1 : Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 + HPow.hPow (β := ℕ) x 2
refine_2 : ∀ (x : ℝ), 1 + HPow.hPow (β := ℕ) x 2 ≠ 0
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + HPow.hPow (β := ℕ) x 2) = arctan b - arctan a

Tactic:
refine integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
    (continuous_const.div ?_ fun x => ?_).continuousOn

Premises used: Continuous.continuousOn, continuous_const, Real.deriv_arctan, Real.differentiableAt_arctan, Continuous.div, intervalIntegral.integral_deriv_eq_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ 1 + HPow.hPow (β := ℕ) x 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b x : ℝ
nlinarith : 1 + HPow.hPow (β := ℕ) x 2 = 0 → -1 + (0 - HPow.hPow (β := ℕ) x 2) + (1 + HPow.hPow (β := ℕ) x 2 - 0) = 0
⊢ 1 + HPow.hPow (β := ℕ) x 2 ≠ 0

Tactic:
nlinarith
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, (1 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan b - arctan a

Tactic:
simp only [← one_div, integral_one_div_one_add_sq]

Premises used: one_div, integral_one_div_one_add_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : c ≠ 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in a..b, (HPow.hPow (β := ℕ) c 2)⁻¹ * (1 + HPow.hPow (β := ℕ) (x / c) 2)⁻¹)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : c ≠ 0
simp : c * ((HPow.hPow (β := ℕ) c 2)⁻¹ * (arctan (b / c) - arctan (a / c))) = c⁻¹ * (arctan (b / c) - arctan (a / c))
⊢ ∫ (x : ℝ) in a..b, (HPow.hPow (β := ℕ) c 2)⁻¹ * (1 + HPow.hPow (β := ℕ) (x / c) 2)⁻¹ =
    c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
simp [integral_comp_div (fun x => (c ^ 2)⁻¹ * (1 + x ^ 2)⁻¹) hc]

Premises used: HMul.hMul, intervalIntegral.integral_comp_div, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : c ≠ 0
⊢ c * ((HPow.hPow (β := ℕ) c 2)⁻¹ * (arctan (b / c) - arctan (a / c))) = c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in a..b, c / (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2))
    (∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
pos :
  ∀ (hc : c = 0),
    ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
neg :
  ∀ (hc : ¬c = 0),
    ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : c = 0
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
simp [hc]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : ¬c = 0
neg : c * (c⁻¹ * (arctan (b / c) - arctan (a / c))) = arctan (b / c) - arctan (a / c)
⊢ ∫ (x : ℝ) in a..b, c * (HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) x 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
rw [integral_const_mul, integral_inv_sq_add_sq hc]

Premises used: integral_inv_sq_add_sq, intervalIntegral.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b c : ℝ
hc : ¬c = 0
⊢ c * (c⁻¹ * (arctan (b / c) - arctan (a / c))) = arctan (b / c) - arctan (a / c)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
contrapose : ∀ (ht : t + 1 = 0), t = -1
⊢ t + 1 ≠ 0

Tactic:
contrapose ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t + 1 = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (ht : t = -1), t = -1
⊢ t = -1

Tactic:
rwa [add_eq_zero_iff_eq_neg] at ht

Premises used: add_eq_zero_iff_eq_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0

Tactic:
have : t + 1 ≠ 0 := by contrapose ht; rwa [add_eq_zero_iff_eq_neg] at ht
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
hderiv :
  ∀ x ∈ [[a, b]],
    HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
      ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
hint :
  IntervalIntegrable (ε := ℂ) (fun (y : ℝ) ↦ (↑y : ℂ) * (1 + HPow.hPow (β := ℕ) (↑y : ℂ) 2) ^ t) MeasureTheory.volume a
    b
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t =
    (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)) -
      (1 + HPow.hPow (β := ℕ) (↑a : ℂ) 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
apply integral_eq_sub_of_hasDerivAt

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
hderiv :
  x ∈ [[a, b]] →
    HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
      ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x
⊢ x ∈ [[a, b]] →
    HasDerivAt (fun {b : ℝ} ↦ (1 + HPow.hPow (β := ℕ) (↑b : ℂ) 2) ^ (t + 1) / (2 * (t + 1)))
      ((↑x : ℂ) * (1 + HPow.hPow (β := ℕ) (↑x : ℂ) 2) ^ t) x

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
⊢ HasDerivAt (fun (x : ℂ) ↦ 1 + HPow.hPow (β := ℕ) x 2) ((↑2 : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℕ) 2 1) (↑x : ℂ)

Tactic:
(hasDerivAt_pow 2 (x : ℂ)).const_add 1

Premises used: Complex.ofReal, HasDerivAt.const_add, hasDerivAt_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h_1 : x ∈ [[a, b]]
h : (↑x : ℂ) = (↑x : ℂ) ^ HSub.hSub (α := ℕ) 2 1
⊢ HasDerivAt (fun (y : ℂ) ↦ 1 + HPow.hPow (β := ℕ) y 2) (2 * (↑x : ℂ)) (↑x : ℂ)

Tactic:
convert! (hasDerivAt_pow 2 (x : ℂ)).const_add 1

Premises used: Complex.ofReal, HasDerivAt.const_add, hasDerivAt_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic
Goal:
a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
h : x ∈ [[a, b]]
⊢ (↑x : ℂ) = (↑x : ℂ) ^ HSub.hSub (α := ℕ) 2 1

Tactic:
simp