awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
refine :
  AEStronglyMeasurable.{uG, uF''} (β := F'')
    (fun (x : G × G) ↦
      (((L₄ : (a : E') → E'' →L[𝕜] F'') (g x.1) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x.2 - x.1)))
    (μ.prod ν)
⊢ 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:
refine L₃.aestronglyMeasurable_comp₂ hf.comp_snd ?_

Premises used: ContinuousLinearMap.aestronglyMeasurable_comp₂, MeasureTheory.AEStronglyMeasurable.comp_snd
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
⊢ AEStronglyMeasurable.{uG, uF''} (β := F'')
    (fun (x : G × G) ↦
      (((L₄ : (a : E') → E'' →L[𝕜] F'') (g x.1) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x.2 - x.1)))
    (μ.prod ν)

Tactic:
L₄.aestronglyMeasurable_comp₂ hg.comp_fst ?_

Premises used: ContinuousLinearMap.aestronglyMeasurable_comp₂, MeasureTheory.AEStronglyMeasurable.comp_fst
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
refine : AEStronglyMeasurable.{uG, uE''} (β := E'') (fun (x : G × G) ↦ k (x₀ - x.2 - x.1)) (μ.prod ν)
⊢ AEStronglyMeasurable.{uG, uF''} (β := F'')
    (fun (x : G × G) ↦
      (((L₄ : (a : E') → E'' →L[𝕜] F'') (g x.1) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - x.2 - x.1)))
    (μ.prod ν)

Tactic:
refine L₄.aestronglyMeasurable_comp₂ hg.comp_fst ?_

Premises used: ContinuousLinearMap.aestronglyMeasurable_comp₂, MeasureTheory.AEStronglyMeasurable.comp_fst
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
⊢ Measurable (β := G) fun (x : G × G) ↦ x₀ - x.2 - x.1

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
refine : Measure.map (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) ≪ μ
⊢ AEStronglyMeasurable.{uG, uE''} (β := E'') (fun (x : G × G) ↦ k (x₀ - x.2 - x.1)) (μ.prod ν)

Tactic:
refine (hk.mono_ac ?_).comp_measurable (by fun_prop)

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.mono_ac
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
⊢ Measure.map (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) ≪ μ

Tactic:
QuasiMeasurePreserving.absolutelyContinuous ?_

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
refine : QuasiMeasurePreserving (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) μ
⊢ Measure.map (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) ≪ μ

Tactic:
refine QuasiMeasurePreserving.absolutelyContinuous ?_

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.Analysis.Convolution
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 ℝ ℝ) ν
refine : ∀ (y : G), QuasiMeasurePreserving (fun (x : G) ↦ x₀ - (x, y).2 - (x, y).1) μ μ
⊢ QuasiMeasurePreserving (fun (x : G × G) ↦ x₀ - x.2 - x.1) (μ.prod ν) μ

Tactic:
refine QuasiMeasurePreserving.prod_of_left (by fun_prop) (Eventually.of_forall fun y => ?_)

Premises used: MeasureTheory.QuasiMeasurePreserving.prod_of_left, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Convolution
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
dsimp : QuasiMeasurePreserving (fun (x : G) ↦ x₀ - y - x) μ μ
⊢ QuasiMeasurePreserving (fun (x : G) ↦ x₀ - (x, y).2 - (x, y).1) μ μ

Tactic:
dsimp only
-- Module: Mathlib.Analysis.Convolution
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₀ - y - x) μ μ

Tactic:
quasiMeasurePreserving_sub_left_of_right_invariant μ _

Premises used: MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant
-- Module: Mathlib.Analysis.Convolution
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₀ - y - x) μ μ

Tactic:
exact quasiMeasurePreserving_sub_left_of_right_invariant μ _

Premises used: MeasureTheory.quasiMeasurePreserving_sub_left_of_right_invariant