awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos : ∀ (ht : t ≤ 0),
  Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
Tactic: rcases this with (ht | ht | ht)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
pos :
  ∀ (ht : t ≤ 0),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₁ : ∀ (ht : t ∈ Ioo 0 x),
  Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
Tactic: rcases this with (ht | ht | ht)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
pos :
  ∀ (ht : t ≤ 0),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
pos₁ :
  ∀ (ht : t ∈ Ioo 0 x),
    Eq.{uF + 1} (α := F)
      ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
          t :
        F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₂ : ∀ (ht : x ≤ t),
  Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
Tactic: rcases this with (ht | ht | ht)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ≤ 0
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos : Eq.{uF + 1} (α := F) (0 : F)
  ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
        map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ≤ 0
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₁ : Eq.{uF + 1} (α := F) (0 : F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
        map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ≤ 0
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ : Eq.{uF + 1} (α := F) (0 : F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₂ : Eq.{uF + 1} (α := F) (0 : F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
        map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ≤ 0
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ : Eq.{uF + 1} (α := F) (0 : F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
pos₂ : Eq.{uF + 1} (α := F) (0 : F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₃ : Eq.{uF + 1} (α := F) 0 0
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
        map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ∈ Ioo 0 x
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
  ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
          indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ∈ Ioo 0 x
pos :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₁ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
  ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
          indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : t ∈ Ioo 0 x
pos :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ :
  Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
    ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₂ : Eq.{uF + 1} (α := F) ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
  ((((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) : F)
Tactic: rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
          indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : x ≤ t
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos : Eq.{uF + 1} (α := F) (0 : F)
  ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F)
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_ge ht),
          indicator_of_notMem (notMem_Ioi.mpr (sub_nonpos_of_le ht)), map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : x ≤ t
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₁ : Eq.{uF + 1} (α := F) (0 : F) ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) 0 : F)
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_ge ht),
          indicator_of_notMem (notMem_Ioi.mpr (sub_nonpos_of_le ht)), map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
ht : x ≤ t
pos :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
pos₁ :
  Eq.{uF + 1} (α := F) (0 : F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) 0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        t :
      F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
have pos₂ : Eq.{uF + 1} (α := F) 0 0
Tactic: rw [indicator_of_notMem (notMem_Ioo_of_ge ht),
          indicator_of_notMem (notMem_Ioi.mpr (sub_nonpos_of_le ht)), map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
⊢ Eq.{uF + 1} (α := F) 0
    (∫ (t : ℝ),
      (((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
        (indicator (Ioi 0) g (x - t)) ∂ν)
have h₁ : ∀ (t : ℝ),
  Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
Tactic: convert! (integral_zero ℝ F).symm with t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have pos : ∀ (ht : 0 < t),
  Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
Tactic: by_cases ht : 0 < t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
pos :
  ∀ (ht : 0 < t),
    Eq.{uF + 1} (α := F)
      ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) :
        F)
      (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have neg : ∀ (ht : ¬0 < t),
  Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
Tactic: by_cases ht : 0 < t
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have rw : x - t ∉ Ioi 0
Tactic: rw [indicator_of_notMem (_ : x - t ∉ Ioi 0), map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ x - t ∉ Ioi 0
have rw : ∀ (h : x ≤ 0) (t : ℝ) (ht : 0 < t), x - t ≤ 0
Tactic: rw [notMem_Ioi] at h ⊢
Cleared hypotheses: h, t, ht
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have neg : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
Tactic: rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
neg : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have neg₁ : Eq.{uF + 1} (α := F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
Tactic: rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst_6 : NoAtoms ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
neg : Eq.{uF + 1} (α := F) (((L : (a : E) → E' →L[ℝ] F) 0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
neg₁ : Eq.{uF + 1} (α := F) ((0 : (a : E') → F) (indicator (Ioi 0) g (x - t)) : F) (0 : F)
⊢ Eq.{uF + 1} (α := F)
    ((((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) :
      F)
    (0 : F)
have neg₂ : Eq.{uF + 1} (α := F) 0 0
Tactic: rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, ContinuousLinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : IntegrableOn f (Ioi 0) ν
hg : IntegrableOn g (Ioi 0) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (posConvolution f g L ν) μ
have rw : ∀ (hf : Integrable (indicator (Ioi 0) f) ν) (hg : Integrable (indicator (Ioi 0) g) μ) (L : E →L[ℝ] E' →L[ℝ] F),
  Integrable (posConvolution f g L ν) μ
Tactic: rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet (Ioi (0 : ℝ)))] at hf hg
Cleared hypotheses: hf, hg, L
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ E'
inst_5 : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
μ ν : Measure ℝ
inst_6 : SFinite μ
inst_7 : SFinite ν
inst_8 : μ.IsAddRightInvariant
inst_9 : NoAtoms ν
hf : Integrable (indicator (Ioi 0) f) ν
hg : Integrable (indicator (Ioi 0) g) μ
L : E →L[ℝ] E' →L[ℝ] F
⊢ Integrable (posConvolution f g L ν) μ
have rw : Integrable (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) μ
Tactic: rw [posConvolution_eq_convolution_indicator f g L ν]