-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeffOn_eq_integral {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b) :
    fourierCoeffOn hab f n =
      (1 / (b - a)) • ∫ x in a..b, fourier (-n) (x : AddCircle (b - a)) • f x

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
rw [fourierCoeffOn, fourierCoeff_eq_intervalIntegral _ _ a, add_sub, add_sub_cancel_left]

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Proof state:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
simp_rw [intervalIntegral.integral_of_le hab.le]

Result:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x ∂volume =
    ∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • f x ∂volume

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ 0 < b - a

Tactic:
linarith

Result:
no goals

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
⊢ fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
haveI := Fact.mk (by linarith : 0 < b - a)

Result:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Proof state:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))

Tactic:
rwa [add_sub, add_sub_cancel_left]

Result:
no goals

Proof state:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = (fourier (-n)) ↑x • f x

Tactic:
rw [liftIoc_coe_apply]

Result:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ x ∈ Ioc a (a + (b - a))

Proof state:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Result:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x

Proof state:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
⊢ ∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x ∂volume =
    ∫ (x : ℝ) in Ioc a b, (fourier (-n)) ↑x • f x ∂volume

Tactic:
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_

Result:
case e_a
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
n : ℤ
hab : a < b
this : Fact (0 < b - a)
x : ℝ
hx : x ∈ Ioc a b
⊢ (fourier (-n)) ↑x • liftIoc (b - a) a f ↑x = (fourier (-n)) ↑x • f x