-- Mathlib/Analysis/Convolution.lean
theorem posConvolution_eq_convolution_indicator (f : ℝ → E) (g : ℝ → E') (L : E →L[ℝ] E' →L[ℝ] F)
    (ν : Measure ℝ

Proof state:
case neg
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
⊢ 0 = ∫ (t : ℝ), (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) ∂ν

Tactic:
convert (integral_zero ℝ F).symm with t

Result:
case h.e'_3.h.e'_7.h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
⊢ (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) = 0

Proof state:
case pos.e_f.h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
⊢ (Ioo 0 x).indicator (fun t => (L (f t)) (g (x - t))) t =
    (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0)

Tactic:
rcases this with (ht | ht | ht)

Result:
case pos.e_f.h.inl
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : t ≤ 0
⊢ (Ioo 0 x).indicator (fun t => (L (f t)) (g (x - t))) t =
    (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0)

case pos.e_f.h.inr.inl
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : t ∈ Ioo 0 x
⊢ (Ioo 0 x).indicator (fun t => (L (f t)) (g (x - t))) t =
    (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0)

case pos.e_f.h.inr.inr
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : x ≤ t
⊢ (Ioo 0 x).indicator (fun t => (L (f t)) (g (x - t))) t =
    (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0)

Proof state:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ≤ 0
t : ℝ
ht : 0 < t
⊢ x - t ≤ 0

Tactic:
exact sub_nonpos.mpr (h.trans ht.le)

Result:
no goals

Proof state:
case pos
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) = 0

Tactic:
rw [if_neg (_ : x - t ∉ Ioi 0), ContinuousLinearMap.map_zero]

Result:
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ x - t ∉ Ioi 0

Proof state:
case h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
⊢ (if x ∈ Ioi 0 then (fun x => ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν) x else 0) =
    ∫ (t : ℝ), (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) ∂ν

Tactic:
simp only

Result:
case h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
⊢ (if x ∈ Ioi 0 then ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν else 0) =
    ∫ (t : ℝ), (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) ∂ν

Proof state:
case h.e'_3.h.e'_7.h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
⊢ (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) = 0

Tactic:
by_cases ht : 0 < t

Result:
case pos
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) = 0

case neg
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
⊢ (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) = 0

Proof state:
case h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
⊢ posConvolution f g L ν x = ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) x

Tactic:
unfold convolution posConvolution indicator

Result:
case h
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : autoParam (Measure ℝ) _auto✝
inst✝ : NoAtoms ν
x : ℝ
⊢ (if x ∈ Ioi 0 then (fun x => ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν) x else 0) =
    ∫ (t : ℝ), (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) ∂ν