-- Mathlib/Analysis/Convolution.lean
theorem support_convolution_subset_swap : support (f ⋆[L, μ] g) ⊆ support g + support f

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
⊢ ∫ (t : G), (L (f t)) (g (x - t)) ∂μ = 0

Tactic:
convert integral_zero G F using 2

Result:
case h.e'_2.h.e'_7
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
⊢ (fun t => (L (f t)) (g (x - t))) = fun x => 0

Proof state:
case h.e'_2.h.e'_7.h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
⊢ (L (f t)) (g (x - t)) = 0

Tactic:
rcases hx (x - t) t with (h | h | h)

Result:
case h.e'_2.h.e'_7.h.inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : g (x - t) = 0
⊢ (L (f t)) (g (x - t)) = 0

case h.e'_2.h.e'_7.h.inr.inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : f t = 0
⊢ (L (f t)) (g (x - t)) = 0

case h.e'_2.h.e'_7.h.inr.inr
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : ¬x - t + t = x
⊢ (L (f t)) (g (x - t)) = 0

Proof state:
case h.e'_2.h.e'_7.h.inr.inl
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
x : G
h2x : x ∈ support (f ⋆[L, μ] g)
hx : ∀ (x_1 x_2 : G), g x_1 = 0 ∨ f x_2 = 0 ∨ ¬x_1 + x_2 = x
t : G
h : f t = 0
⊢ (L (f t)) (g (x - t)) = 0

Tactic:
rw [h, L.map_zero₂]

Result:
no goals