awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3
this : dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) (g i (k i)) ≤ ε / 3 + ε / 3
h : ε / 3 + ε / 3 + ε / 3 = ε
⊢ dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) z₀ < ε

Tactic:
refine ((dist_triangle _ _ _).trans_lt (add_lt_add_of_le_of_lt this hgi)).trans_eq ?_

Premises used: dist_triangle, add_lt_add_of_le_of_lt, LT.lt.trans_eq, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3
this : dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) (g i (k i)) ≤ ε / 3 + ε / 3
⊢ ε / 3 + ε / 3 + ε / 3 = ε

Tactic:
ring
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : CompleteSpace F
inst_10 : AddGroup G
inst_11 : SFinite μ
inst_12 : SFinite ν
inst_13 : μ.IsAddRightInvariant
inst_14 : MeasurableAdd₂ G
inst_15 : MeasurableNeg G
inst_16 : NormedSpace ℝ E
inst_17 : NormedSpace ℝ E'
inst_18 : CompleteSpace E
inst_19 : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ Integrable.{uF, uG} (ε := F)
    (uncurry fun (x t : G) ↦ (((L : (a : E) → E' →L[𝕜] F) (f t) : E' →L[𝕜] F) : (a : E') → F) (g (x - t))) (μ.prod ν)

Tactic:
apply hf.convolution_integrand L hg

Premises used: MeasureTheory.Integrable.convolution_integrand
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : CompleteSpace F
inst_10 : AddGroup G
inst_11 : SFinite μ
inst_12 : SFinite ν
inst_13 : μ.IsAddRightInvariant
inst_14 : MeasurableAdd₂ G
inst_15 : MeasurableNeg G
inst_16 : NormedSpace ℝ E
inst_17 : NormedSpace ℝ E'
inst_18 : CompleteSpace E
inst_19 : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
refine :
  Eq.{uF + 1} (α := F)
    (∫ (y : G), ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) ∂μ ∂ν : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)
⊢ Eq.{uF + 1} (α := F) (∫ (x : G), convolution.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) f g L ν x ∂μ : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)

Tactic:
refine (integral_integral_swap (by apply hf.convolution_integrand L hg)).trans ?_

Premises used: MeasureTheory.integral_integral_swap, Eq.trans
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : CompleteSpace F
inst_10 : AddGroup G
inst_11 : SFinite μ
inst_12 : SFinite ν
inst_13 : μ.IsAddRightInvariant
inst_14 : MeasurableAdd₂ G
inst_15 : MeasurableNeg G
inst_16 : NormedSpace ℝ E
inst_17 : NormedSpace ℝ E'
inst_18 : CompleteSpace E
inst_19 : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
simp_rw :
  Eq.{uF + 1} (α := F)
    (∫ (y : G), (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (∫ (x : G), g x ∂μ) ∂ν : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)
⊢ Eq.{uF + 1} (α := F)
    (∫ (y : G), ∫ (x : G), (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (g (x - y)) ∂μ ∂ν : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)

Tactic:
simp_rw [integral_comp_comm _ (hg.comp_sub_right _), integral_sub_right_eq_self]

Premises used: ContinuousLinearMap.integral_comp_comm, MeasureTheory.integral_sub_right_eq_self, MeasureTheory.Integrable.comp_sub_right
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : CompleteSpace F
inst_10 : AddGroup G
inst_11 : SFinite μ
inst_12 : SFinite ν
inst_13 : μ.IsAddRightInvariant
inst_14 : MeasurableAdd₂ G
inst_15 : MeasurableNeg G
inst_16 : NormedSpace ℝ E
inst_17 : NormedSpace ℝ E'
inst_18 : CompleteSpace E
inst_19 : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ Eq.{uF + 1} (α := F)
    (∫ (y : G), (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (∫ (x : G), g x ∂μ) ∂ν : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)

Tactic:
(L.flip (∫ x, g x ∂μ)).integral_comp_comm hf

Premises used: MeasureTheory.integral, ContinuousLinearMap.flip, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- Module: Mathlib.Analysis.Convolution
Goal:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup E'
inst_2 : NormedAddCommGroup F
f : G → E
g : G → E'
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedSpace 𝕜 E'
inst_6 : NormedSpace ℝ F
inst_7 : NormedSpace 𝕜 F
inst_8 : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst_9 : CompleteSpace F
inst_10 : AddGroup G
inst_11 : SFinite μ
inst_12 : SFinite ν
inst_13 : μ.IsAddRightInvariant
inst_14 : MeasurableAdd₂ G
inst_15 : MeasurableNeg G
inst_16 : NormedSpace ℝ E
inst_17 : NormedSpace ℝ E'
inst_18 : CompleteSpace E
inst_19 : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ Eq.{uF + 1} (α := F)
    (∫ (y : G), (((L : (a : E) → E' →L[𝕜] F) (f y) : E' →L[𝕜] F) : (a : E') → F) (∫ (x : G), g x ∂μ) ∂ν : F)
    (((L : (a : E) → E' →L[𝕜] F) (∫ (x : G), f x ∂ν) : (a : E') → F) (∫ (x : G), g x ∂μ) : F)

Tactic:
exact (L.flip (∫ x, g x ∂μ)).integral_comp_comm hf

Premises used: MeasureTheory.integral, ContinuousLinearMap.flip, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- 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
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt.{u𝕜, uG, uE', uE'', uF''} (𝕜 := 𝕜) (F := F'') g k x L₄ μ
hi :
  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 ν)
⊢ Eq.{uF' + 1} (α := F')
    (∫ (t : G),
      ∫ (s : G),
        (((L₂ : (a : F) → E'' →L[𝕜] F') ((((L : (a : E) → E' →L[𝕜] F) (f s) : E' →L[𝕜] F) : (a : E') → F) (g (t - s))) :
              E'' →L[𝕜] F') :
            (a : E'') → F')
          (k (x₀ - t)) ∂ν ∂μ)
    (∫ (t : G),
      ∫ (s : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂ν ∂μ)

Tactic:
simp_rw [hL]
-- 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
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt.{u𝕜, uG, uE', uE'', uF''} (𝕜 := 𝕜) (F := F'') g k x L₄ μ
hi :
  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 ν)
rw rw₁ :
  Eq.{uF' + 1} (α := F')
    (∫ (y : G),
      ∫ (x : 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'') ∂μ ∂ν)
    (∫ (s : G),
      ∫ (t : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂μ ∂ν)
⊢ Eq.{uF' + 1} (α := F')
    (∫ (t : G),
      ∫ (s : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂ν ∂μ)
    (∫ (s : G),
      ∫ (t : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂μ ∂ν)

Tactic:
rw [integral_integral_swap hi]

Premises used: MeasureTheory.integral_integral_swap
-- 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
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt.{u𝕜, uG, uE', uE'', uF''} (𝕜 := 𝕜) (F := F'') g k x L₄ μ
hi :
  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 ν)
e_f :
  Eq (α := G → F')
    (fun (s : G) ↦
      ∫ (t : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂μ)
    fun (s : G) ↦
    ∫ (u : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g u) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - s - u)) : F'') ∂μ
⊢ Eq.{uF' + 1} (α := F')
    (∫ (s : G),
      ∫ (t : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂μ ∂ν)
    (∫ (s : G),
      ∫ (u : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g u) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - s - u)) : F'') ∂μ ∂ν)

Tactic:
congr
-- 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
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt.{u𝕜, uG, uE', uE'', uF''} (𝕜 := 𝕜) (F := F'') g k x L₄ μ
hi :
  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 ν)
e_f :
  ∀ (t : G),
    Eq.{uF' + 1} (α := F')
      (∫ (t_1 : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t_1 - t)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t_1)) : F'') ∂μ)
      (∫ (u : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g u) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t - u)) : F'') ∂μ)
⊢ Eq (α := G → F')
    (fun (s : G) ↦
      ∫ (t : G),
        (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
          ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t - s)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t)) : F'') ∂μ)
    fun (s : G) ↦
    ∫ (u : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f s) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g u) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - s - u)) : F'') ∂μ

Tactic:
ext t
-- 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
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt.{u𝕜, uG, uE, uE', uF} (𝕜 := 𝕜) (F := F) f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt.{u𝕜, uG, uE', uE'', uF''} (𝕜 := 𝕜) (F := F'') g k x L₄ μ
hi :
  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 ν)
t : G
e_f :
  Eq.{uF' + 1} (α := F')
    (∫ (x : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (x - t)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t - (x - t))) :
          F'') ∂μ)
    (∫ (t_1 : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t_1 - t)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t_1)) : F'') ∂μ)
⊢ Eq.{uF' + 1} (α := F')
    (∫ (t_1 : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g (t_1 - t)) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t_1)) : F'') ∂μ)
    (∫ (u : G),
      (((L₃ : (a : E) → F'' →L[𝕜] F') (f t) : F'' →L[𝕜] F') : (a : F'') → F')
        ((((L₄ : (a : E') → E'' →L[𝕜] F'') (g u) : E'' →L[𝕜] F'') : (a : E'') → F'') (k (x₀ - t - u)) : F'') ∂μ)

Tactic:
rw [eq_comm, ← integral_sub_right_eq_self _ t]

Premises used: eq_comm, MeasureTheory.integral_sub_right_eq_self