-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos_mul_complex {z : ℂ} (hz : z ≠ 0) (a b : ℝ) :
    (∫ x in a..b, Complex.cos (z * x)) = Complex.sin (z * b) / z - Complex.sin (z * a) / z

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
intro x _

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a b x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
have a := Complex.hasDerivAt_sin (↑x * z)

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b x : ℝ
a✝ : x ∈ [[a✝¹, b]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
have d := HasDerivAt.comp_ofReal (c.div_const z)

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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:
simp only [mul_comm] at d

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

case hint
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b

Tactic:
swap

Result:
case hint
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b

case hderiv
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
convert d using 1

Result:
case h.e'_9
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = z * Complex.cos (z * ↑x) / z

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b x : ℝ
a✝ : x ∈ [[a✝¹, b]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
have b : HasDerivAt (fun y => y * z : ℂ → ℂ) z ↑x := hasDerivAt_mul_const _

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case hint
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b

Tactic:
apply Continuous.intervalIntegrable

Result:
case hint.hu
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y => Complex.cos (z * ↑y)

Proof state:
case hint.hu
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y => Complex.cos (z * ↑y)

Tactic:
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)

Result:
no goals

Proof state:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
a : HasDerivAt Complex.sin (Complex.cos (↑x * z)) (↑x * z)
b : HasDerivAt (fun y => y * z) z ↑x
⊢ HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Tactic:
have c : HasDerivAt (Complex.sin ∘ fun y : ℂ => (y * z)) _ ↑x := HasDerivAt.comp (𝕜 := ℂ) x a b

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

Proof state:
case h.e'_9
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = z * Complex.cos (z * ↑x) / z

Tactic:
conv_rhs => arg 1; rw [mul_comm]

Result:
case h.e'_9
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = Complex.cos (z * ↑x) * z / z

Proof state:
case h.e'_9
z : ℂ
hz : z ≠ 0
a✝¹ b✝ x : ℝ
a✝ : x ∈ [[a✝¹, b✝]]
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 => z * y) ↑y / z) (z * Complex.cos (z * ↑x) / z) x
⊢ Complex.cos (z * ↑x) = Complex.cos (z * ↑x) * z / z

Tactic:
rw [mul_div_cancel_right₀ _ hz]

Result:
no goals

Proof state:
z : ℂ
hz : z ≠ 0
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

Result:
case hderiv
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∀ x ∈ [[a, b]], HasDerivAt (fun b => Complex.sin (z * ↑b) / z) (Complex.cos (z * ↑x)) x

case hint
z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ IntervalIntegrable (fun y => Complex.cos (z * ↑y)) MeasureTheory.volume a b