-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem fourierIntegral_add (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2)
    {f g : V → E} (hf : Integrable f μ) (hg : Integrable g μ) :
    fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g

Proof state:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ ∫ (v : V), e (-(L v) w) • (f v + g v) ∂μ = ∫ (v : V), e (-(L v) w) • f v ∂μ + ∫ (v : V), e (-(L v) w) • g v ∂μ

Tactic:
simp_rw [smul_add]

Result:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ ∫ (v : V), e (-(L v) w) • f v + e (-(L v) w) • g v ∂μ =
    ∫ (v : V), e (-(L v) w) • f v ∂μ + ∫ (v : V), e (-(L v) w) • g v ∂μ

Proof state:
case h.hg
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable (fun v => e (-(L v) w) • g v) μ

Tactic:
exact (fourierIntegral_convergent_iff he hL w).2 hg

Result:
no goals

Proof state:
case h.hf
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable (fun v => e (-(L v) w) • f v) μ

Tactic:
exact (fourierIntegral_convergent_iff he hL w).2 hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
⊢ fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g

Tactic:
ext1 w

Result:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w

Proof state:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ ∫ (v : V), e (-(L v) w) • f v + e (-(L v) w) • g v ∂μ =
    ∫ (v : V), e (-(L v) w) • f v ∂μ + ∫ (v : V), e (-(L v) w) • g v ∂μ

Tactic:
rw [integral_add]

Result:
case h.hf
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable (fun v => e (-(L v) w) • f v) μ

case h.hg
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ Integrable (fun v => e (-(L v) w) • g v) μ

Proof state:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ fourierIntegral e μ L (f + g) w = (fourierIntegral e μ L f + fourierIntegral e μ L g) w

Tactic:
dsimp only [Pi.add_apply, fourierIntegral]

Result:
case h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ⇑e
hL : Continuous fun p => (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
w : W
⊢ ∫ (v : V), e (-(L v) w) • (f v + g v) ∂μ = ∫ (v : V), e (-(L v) w) • f v ∂μ + ∫ (v : V), e (-(L v) w) • g v ∂μ