Theorem: F_sub (PrimeNumberTheoremAnd/Fourier.lean)

State before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x - g x) x = 𝓕 f x - 𝓕 g x
Tactic:
simp_rw [sub_eq_add_neg]
State after:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x + -g x) x = 𝓕 f x + -𝓕 g x

State before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x + -g x) x = 𝓕 f x + -𝓕 g x
Tactic:
rw [F_add]
State after:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x) x + 𝓕 (fun x => -g x) x = 𝓕 f x + -𝓕 g x

case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume

State before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ 𝓕 (fun x => f x) x + 𝓕 (fun x => -g x) x = 𝓕 f x + -𝓕 g x

case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
simp
State after:
case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume

State before:
case hf
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => f x) volume

case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
exact hf
State after:
case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume

State before:
case hg
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Integrable (fun x => -g x) volume
Tactic:
exact hg.neg
State after:
no goals