-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeffOn_of_hasDeriv_right {a b : ℝ} (hab : a < b) {f f' : ℝ → ℂ}
    {n : ℤ} (hn : n ≠ 0)
    (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x, x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x)
    (hf' : IntervalIntegrable f' volume a b) :
    fourierCoeffOn hab f n = 1 / (-2 * π * I * n) *
      (fourier (-n) (a : AddCircle (b - a)) * (f b - f a) - (b - a) * fourierCoeffOn hab f' n)

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑(b - a) / (-2 * ↑π * I * ↑n) = ↑(b - a) * (1 / (-2 * ↑π * I * ↑n))

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - (↑b - ↑a) * fourierCoeffOn hab f' n)

Tactic:
rw [← ofReal_sub]

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, f' x * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Tactic:
conv in intervalIntegral _ _ _ _ => congr; ext; rw [this]

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑b) -
          f a * (↑(b - a) / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) / (-2 * ↑π * I * ↑n) * (f' x * (fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑b) -
          f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * (fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Tactic:
have s2 : (b : AddCircle (b - a)) = (a : AddCircle (b - a)) := by
  simpa using coe_add_period (b - a) a

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) *
      (f b * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑b) -
          f a * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a) -
        ∫ (x : ℝ) in a..b, ↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (f' x * (fourier (-n)) ↑x)) =
    1 / (-2 * ↑π * I * ↑n) *
      ((f b - f a) * (fourier (-n)) ↑a - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)

Tactic:
intros

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
u✝ v✝ w✝ : ℂ
⊢ u✝ * (↑(b - a) / v✝ * w✝) = ↑(b - a) / v✝ * (u✝ * w✝)

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
u✝ v✝ w✝ : ℂ
⊢ u✝ * (↑(b - a) / v✝ * w✝) = ↑(b - a) / v✝ * (u✝ * w✝)

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)

Tactic:
simp_rw [fourierCoeffOn_eq_integral, smul_eq_mul, real_smul, ofReal_div, ofReal_one]

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f' x))

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ 0 < b - a

Tactic:
linarith

Result:
no goals

Proof state:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)

Tactic:
have hT : Fact (0 < b - a) := ⟨by linarith⟩

Result:
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n =
    1 / (-2 * ↑π * I * ↑n) * ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * fourierCoeffOn hab f' n)