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

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 ∫ (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) ∂ν

Tactic:
split_ifs with h

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 : ℝ) in 0 ..x, (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 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) ∂ν

Proof state:
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)

Tactic:
rw [indicator_of_not_mem (not_mem_Ioo_of_ge ht),
  if_neg (not_mem_Ioi.mpr (sub_nonpos_of_le ht)), ContinuousLinearMap.map_zero]

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
⊢ ∫ (x_1 : ℝ), (Ioo 0 x).indicator (fun t => (L (f t)) (g (x - t))) x_1 ∂ν =
    ∫ (t : ℝ), (L (if t ∈ Ioi 0 then f t else 0)) (if x - t ∈ Ioi 0 then g (x - t) else 0) ∂ν

Tactic:
congr 1 with t : 1

Result:
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 : ℝ
⊢ (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:
case 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 : ℝ
h : 0 < t
h' : t < x
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

case 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 : ℝ
h : 0 < t
h' : x ≤ t
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
exacts [Or.inr (Or.inl ⟨h, h'⟩), Or.inr (Or.inr h')]

Result:
no goals

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
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 (mem_Ioi.not.mpr ht), ContinuousLinearMap.map_zero,
  ContinuousLinearMap.zero_apply]

Result:
no goals