awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : CompleteSpace F
inst_12 : NormedAddCommGroup F'
inst_13 : NormedSpace ℝ F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : CompleteSpace F'
inst_16 : NormedAddCommGroup F''
inst_17 : NormedSpace ℝ F''
inst_18 : NormedSpace 𝕜 F''
inst_19 : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst_20 : AddGroup G
inst_21 : SFinite μ
inst_22 : SFinite ν
inst_23 : μ.IsAddRightInvariant
inst_24 : MeasurableAdd₂ G
inst_25 : ν.IsAddRightInvariant
inst_26 : MeasurableNeg G
hL :
  ∀ (x : E) (y : E') (z : E''),
    Eq.{uF' + 1} (α := F')
      ((((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) x : E' →L[𝕜] F) : (a : E') → F) y) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          z :
        F')
      ((((L₃ : (a : E) → F'' →L[𝕜] F') x : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') y : E'' →L[𝕜] F'') : (a : E'') → F'') z : F'') :
        F')
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) ↦ ‖g x‖) (fun (x : G) ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk :
  ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) ((fun (x : G) ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun (x : G) ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
⊢ QuasiMeasurePreserving (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) μ
have refine : ∀ (y : G), QuasiMeasurePreserving (fun (x : G) ↦ x₀ - (x, y).2 - (x, y).1) μ μ
Tactic: refine QuasiMeasurePreserving.prod_of_left (by fun_prop) (Eventually.of_forall fun y => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : CompleteSpace F
inst_12 : NormedAddCommGroup F'
inst_13 : NormedSpace ℝ F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : CompleteSpace F'
inst_16 : NormedAddCommGroup F''
inst_17 : NormedSpace ℝ F''
inst_18 : NormedSpace 𝕜 F''
inst_19 : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst_20 : AddGroup G
inst_21 : SFinite μ
inst_22 : SFinite ν
inst_23 : μ.IsAddRightInvariant
inst_24 : MeasurableAdd₂ G
inst_25 : ν.IsAddRightInvariant
inst_26 : MeasurableNeg G
hL :
  ∀ (x : E) (y : E') (z : E''),
    Eq.{uF' + 1} (α := F')
      ((((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) x : E' →L[𝕜] F) : (a : E') → F) y) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          z :
        F')
      ((((L₃ : (a : E) → F'' →L[𝕜] F') x : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') y : E'' →L[𝕜] F'') : (a : E'') → F'') z : F'') :
        F')
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) ↦ ‖g x‖) (fun (x : G) ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk :
  ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) ((fun (x : G) ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun (x : G) ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
y : G
⊢ QuasiMeasurePreserving (fun (x : G) ↦ x₀ - (x, y).2 - (x, y).1) μ μ
have dsimp : QuasiMeasurePreserving (fun (x : G) ↦ x₀ - y - x) μ μ
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : CompleteSpace F
inst_12 : NormedAddCommGroup F'
inst_13 : NormedSpace ℝ F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : CompleteSpace F'
inst_16 : NormedAddCommGroup F''
inst_17 : NormedSpace ℝ F''
inst_18 : NormedSpace 𝕜 F''
inst_19 : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst_20 : AddGroup G
inst_21 : SFinite μ
inst_22 : SFinite ν
inst_23 : μ.IsAddRightInvariant
inst_24 : MeasurableAdd₂ G
inst_25 : ν.IsAddRightInvariant
inst_26 : MeasurableNeg G
hL :
  ∀ (x : E) (y : E') (z : E''),
    Eq.{uF' + 1} (α := F')
      ((((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) x : E' →L[𝕜] F) : (a : E') → F) y) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          z :
        F')
      ((((L₃ : (a : E) → F'' →L[𝕜] F') x : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') y : E'' →L[𝕜] F'') : (a : E'') → F'') z : F'') :
        F')
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) ↦ ‖g x‖) (fun (x : G) ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk :
  ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) ((fun (x : G) ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun (x : G) ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
⊢ Integrable.{uF', uG} (ε := F')
    (uncurry fun (x y : G) ↦
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (x - y)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x)) : F''))
    (μ.prod ν)
have h_meas : AEStronglyMeasurable.{uG, uF'} (β := F')
  (uncurry fun (x y : G) ↦
    (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
      ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g x) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - y - x)) : F''))
  (μ.prod ν)
Tactic: have h_meas :
    AEStronglyMeasurable (uncurry fun x y => L₃ (f y) (L₄ (g x) (k (x₀ - y - x))))
      (μ.prod ν) := by
    refine L₃.aestronglyMeasurable_comp₂ hf.comp_snd ?_
    refine L₄.aestronglyMeasurable_comp₂ hg.comp_fst ?_
    refine (hk.mono_ac ?_).comp_measurable (by fun_prop)
    refine QuasiMeasurePreserving.absolutelyContinuous ?_
    refine QuasiMeasurePreserving.prod_of_left (by fun_prop) (Eventually.of_forall fun y => ?_)
    dsimp only
    exact quasiMeasurePreserving_sub_left_of_right_invariant μ _
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : CompleteSpace F
inst_12 : NormedAddCommGroup F'
inst_13 : NormedSpace ℝ F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : CompleteSpace F'
inst_16 : NormedAddCommGroup F''
inst_17 : NormedSpace ℝ F''
inst_18 : NormedSpace 𝕜 F''
inst_19 : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst_20 : AddGroup G
inst_21 : SFinite μ
inst_22 : SFinite ν
inst_23 : μ.IsAddRightInvariant
inst_24 : MeasurableAdd₂ G
inst_25 : ν.IsAddRightInvariant
inst_26 : MeasurableNeg G
hL :
  ∀ (x : E) (y : E') (z : E''),
    Eq.{uF' + 1} (α := F')
      ((((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) x : E' →L[𝕜] F) : (a : E') → F) y) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          z :
        F')
      ((((L₃ : (a : E) → F'' →L[𝕜] F') x : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') y : E'' →L[𝕜] F'') : (a : E'') → F'') z : F'') :
        F')
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) ↦ ‖g x‖) (fun (x : G) ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk :
  ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) ((fun (x : G) ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun (x : G) ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
h_meas :
  AEStronglyMeasurable.{uG, uF'} (β := F')
    (uncurry fun (x y : G) ↦
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g x) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - y - x)) : F''))
    (μ.prod ν)
⊢ Integrable.{uF', uG} (ε := F')
    (uncurry fun (x y : G) ↦
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (x - y)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x)) : F''))
    (μ.prod ν)
have h2_meas : AEStronglyMeasurable (β := ℝ)
  (fun (y : G) ↦
    ∫ (x : G),
      norm.{uF'} (E := F')
        ((((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
            ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g x) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - y - x)) : F'') :
          F') ∂μ)
  ν
Tactic: have h2_meas :
      AEStronglyMeasurable (fun y => ∫ x, ‖L₃ (f y) (L₄ (g x) (k (x₀ - y - x)))‖ ∂μ) ν :=
    h_meas.prod_swap.norm.integral_prod_right'
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : CompleteSpace F
inst_12 : NormedAddCommGroup F'
inst_13 : NormedSpace ℝ F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : CompleteSpace F'
inst_16 : NormedAddCommGroup F''
inst_17 : NormedSpace ℝ F''
inst_18 : NormedSpace 𝕜 F''
inst_19 : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst_20 : AddGroup G
inst_21 : SFinite μ
inst_22 : SFinite ν
inst_23 : μ.IsAddRightInvariant
inst_24 : MeasurableAdd₂ G
inst_25 : ν.IsAddRightInvariant
inst_26 : MeasurableNeg G
hL :
  ∀ (x : E) (y : E') (z : E''),
    Eq.{uF' + 1} (α := F')
      ((((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) x : E' →L[𝕜] F) : (a : E') → F) y) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          z :
        F')
      ((((L₃ : (a : E) → F'' →L[𝕜] F') x : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') y : E'' →L[𝕜] F'') : (a : E'') → F'') z : F'') :
        F')
x₀ : G
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun (x : G) ↦ ‖g x‖) (fun (x : G) ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk :
  ConvolutionExistsAt (fun (x : G) ↦ ‖f x‖) ((fun (x : G) ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun (x : G) ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
h_meas :
  AEStronglyMeasurable.{uG, uF'} (β := F')
    (uncurry fun (x y : G) ↦
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g x) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - y - x)) : F''))
    (μ.prod ν)
h2_meas :
  AEStronglyMeasurable (β := ℝ)
    (fun (y : G) ↦
      ∫ (x : G),
        norm.{uF'} (E := F')
          ((((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
              ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g x) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - y - x)) : F'') :
            F') ∂μ)
    ν
⊢ Integrable.{uF', uG} (ε := F')
    (uncurry fun (x y : G) ↦
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f y) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (x - y)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x)) : F''))
    (μ.prod ν)
have h3 : Measure.map (fun (z : G × G) ↦ (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν
Tactic: have h3 : map (fun z : G × G => (z.1 - z.2, z.2)) (μ.prod ν) = μ.prod ν :=
    (measurePreserving_sub_prod μ ν).map_eq
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : NormedAddCommGroup G
inst_12 : BorelSpace G
g : G → E'' →L[𝕜] E'
hf : LocallyIntegrable f μ
hcg : HasCompactSupport g
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
x₀ : G
x : E''
⊢ Eq.{uF + 1} (α := F) ((convolution (𝕜 := 𝕜) f g (precompR E'' L) μ x₀ : (a : E'') → F) x : F)
    (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f (fun (a : G) ↦ (g a : (a : E'') → E') x) L μ x₀ : F)
have this : ConvolutionExistsAt (𝕜 := 𝕜) (F := E'' →L[𝕜] F) f g x₀ (precompR E'' L) μ
Tactic: have := hcg.convolutionExists_right (L.precompR E'' :) hf hg x₀
-- Lean 4 proof step from Mathlib.Analysis.Convolution (goal)
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup E''
inst_3 : NormedAddCommGroup F
f : G → E
inst_4 : RCLike 𝕜
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedSpace 𝕜 E'
inst_7 : NormedSpace 𝕜 E''
inst_8 : NormedSpace ℝ F
inst_9 : NormedSpace 𝕜 F
inst_10 : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_11 : NormedAddCommGroup G
inst_12 : BorelSpace G
g : G → E'' →L[𝕜] E'
hf : LocallyIntegrable f μ
hcg : HasCompactSupport g
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
x₀ : G
x : E''
this : ConvolutionExistsAt (𝕜 := 𝕜) (F := E'' →L[𝕜] F) f g x₀ (precompR E'' L) μ
⊢ Eq.{uF + 1} (α := F) ((convolution (𝕜 := 𝕜) f g (precompR E'' L) μ x₀ : (a : E'') → F) x : F)
    (convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (E' := E') f (fun (a : G) ↦ (g a : (a : E'') → E') x) L μ x₀ : F)
have simp_rw : Eq.{uF + 1} (α := F)
  (∫ (x_1 : G),
    (((((precompR E'' L : (a : E) → (E'' →L[𝕜] E') →L[𝕜] E'' →L[𝕜] F) (f x_1) : (E'' →L[𝕜] E') →L[𝕜] E'' →L[𝕜] F) :
              (a : E'' →L[𝕜] E') → E'' →L[𝕜] F)
            (g (x₀ - x_1)) :
          E'' →L[𝕜] F) :
        (a : E'') → F)
      x ∂μ)
  (∫ (t : G),
    (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) ((g (x₀ - t) : (a : E'') → E') x : E') ∂μ)
Tactic: simp_rw [convolution_def, ContinuousLinearMap.integral_apply 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 ν
⊢ posConvolution f g L ν = indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g
have h : ∀ (x : ℝ), posConvolution f g L ν x = (indicator (Ioi 0) f ⋆[L, ν] indicator (Ioi 0) g) x
Tactic: ext1 x
-- 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 : ℝ
⊢ Eq.{uF + 1} (α := F)
    (if Membership.mem (γ := Set ℝ) (Ioi 0) x then
      ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν
    else 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 pos : ∀ (h : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  Eq.{uF + 1} (α := F)
    (∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
    (∫ (t : ℝ),
      (((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
        (indicator (Ioi 0) g (x - t)) ∂ν)
Tactic: split_ifs with h
-- 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 : ℝ
pos :
  ∀ (h : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    Eq.{uF + 1} (α := F)
      (∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
      (∫ (t : ℝ),
        (((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F)
          (indicator (Ioi 0) g (x - t)) ∂ν)
⊢ Eq.{uF + 1} (α := F)
    (if Membership.mem (γ := Set ℝ) (Ioi 0) x then
      ∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν
    else 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 neg : ∀ (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)) ∂ν)
Tactic: split_ifs with h
-- 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
⊢ Eq.{uF + 1} (α := F)
    (∫ (t : ℝ) in 0..x, (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)) ∂ν)
    (∫ (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 pos : Eq.{uF + 1} (α := F)
  (∫ (x_1 : ℝ),
    (Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
      x_1 ∂ν)
  (∫ (t : ℝ),
    (((L : (a : E) → E' →L[ℝ] F) (indicator (Ioi 0) f t) : E' →L[ℝ] F) : (a : E') → F) (indicator (Ioi 0) g (x - t)) ∂ν)
Tactic: rw [intervalIntegral.integral_of_le (le_of_lt h), integral_Ioc_eq_integral_Ioo, ←
      integral_indicator (measurableSet_Ioo : MeasurableSet (Ioo 0 x))]
-- 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
⊢ Eq.{uF + 1} (α := F)
    (∫ (x_1 : ℝ),
      (Ioo 0 x).indicator (fun (t : ℝ) ↦ (((L : (a : E) → E' →L[ℝ] F) (f t) : E' →L[ℝ] F) : (a : E') → F) (g (x - t)))
        x_1 ∂ν)
    (∫ (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 pos : ∀ (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: congr 1 with t : 1
-- 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 : ℝ
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
have inl : ∀ (h : t ≤ 0), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
Tactic: rcases le_or_gt t 0 with (h | h)
-- 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 : ℝ
inl : ∀ (h : t ≤ 0), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
have inr : ∀ (h : 0 < t), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
Tactic: rcases le_or_gt t 0 with (h | h)
-- 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_1 : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
h : 0 < t
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
have inr : ∀ (h' : t < x), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
Tactic: rcases lt_or_ge t x with (h' | h')
-- 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_1 : Membership.mem (γ := Set ℝ) (Ioi 0) x
t : ℝ
h : 0 < t
inr : ∀ (h' : t < x), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
⊢ t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
have inr₁ : ∀ (h' : x ≤ t), t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
Tactic: rcases lt_or_ge t x with (h' | h')
-- Lean 4 proof step from Mathlib.Analysis.Convolution (hypothesis)
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 : ℝ
⊢ 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 this : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t
Tactic: have : t ≤ 0 ∨ t ∈ Ioo 0 x ∨ x ≤ t := by
      rcases le_or_gt t 0 with (h | h)
      · exact Or.inl h
      · rcases lt_or_ge t x with (h' | h')
        exacts [Or.inr (Or.inl ⟨h, h'⟩), Or.inr (Or.inr h')]