-- Mathlib/Analysis/Convolution.lean
theorem convolution_mono_right_of_nonneg {f g g' : G → ℝ}
    (hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, g x ≤ g' x)
    (hg' : ∀ x, 0 ≤ g' x) : (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Proof state:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
have : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0 := integral_undef H

Result:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Proof state:
case pos
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
exact convolution_mono_right H hfg' hf hg

Result:
no goals

Proof state:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
rw [this]

Result:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Proof state:
case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
this : (f ⋆[lsmul ℝ ℝ, μ] g) x = 0
⊢ 0 ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
exact integral_nonneg fun y => mul_nonneg (hf y) (hg' (x - y))

Result:
no goals

Proof state:
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

Tactic:
by_cases H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ

Result:
case pos
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x

case neg
G : Type uG
x : G
inst✝¹ : MeasurableSpace G
μ : Measure G
inst✝ : AddGroup G
f g g' : G → ℝ
hfg' : ConvolutionExistsAt f g' x (lsmul ℝ ℝ) μ
hf : ∀ (x : G), 0 ≤ f x
hg : ∀ (x : G), g x ≤ g' x
hg' : ∀ (x : G), 0 ≤ g' x
H : ¬ConvolutionExistsAt f g x (lsmul ℝ ℝ) μ
⊢ (f ⋆[lsmul ℝ ℝ, μ] g) x ≤ (f ⋆[lsmul ℝ ℝ, μ] g') x