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

Proof state:
case 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
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
rcases lt_or_le t x with (h' | h')

Result:
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

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 ν
⊢ posConvolution f g L ν = (Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g

Tactic:
ext1 x

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 : ℝ
⊢ posConvolution f g L ν x = ((Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g) x

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 ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ x - t ∉ Ioi 0

Tactic:
rw [not_mem_Ioi] at h ⊢

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 ≤ 0
t : ℝ
ht : 0 < t
⊢ x - t ≤ 0

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

Tactic:
rw [indicator_of_mem ht, if_pos (mem_Ioi.mpr ht.1),
  if_pos (mem_Ioi.mpr <| sub_pos.mpr ht.2)]

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 : ℝ) 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) ∂ν

Tactic:
rw [intervalIntegral.integral_of_le (le_of_lt h), integral_Ioc_eq_integral_Ioo, ←
  integral_indicator (measurableSet_Ioo : MeasurableSet (Ioo 0 x))]

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

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

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

Result:
no goals

Proof state:
case 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 : t ≤ 0
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t

Tactic:
exact Or.inl h

Result:
no goals

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

Tactic:
rcases le_or_lt t 0 with (h | h)

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

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