mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : f t = 0
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε

Tactic:
[

Goal state after:
case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
t : G
ht : f t = 0
⊢ dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
[

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist (∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
[

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), dist ((L (f t)) (g (x₀ - t))) ((L (f t)) z₀) ≤ ‖L (f t)‖ * ε
⊢ dist (∫ (t : G), (L (f t)) (g (x₀ - t)) ∂μ) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
ε : ℝ
εpos : 0 < ε
hε : thickening ε ({q₀.1} ×ˢ k) ⊆ t
h'ε : ball q₀.1 ε ⊆ s
C : ℝ
Cpos : 0 < C
hC : g' '' t ⊆ closedBall 0 C
p : P
x : G
hp : ‖p - q₀.1‖ < ε
hps : p ∈ s
hx : x ∉ k
this : g' (p, x) = 0
⊢ ‖g' (p, x)‖ ≤ C

Tactic:
this

Goal state after:
case neg
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
ε : ℝ
εpos : 0 < ε
hε : thickening ε ({q₀.1} ×ˢ k) ⊆ t
h'ε : ball q₀.1 ε ⊆ s
C : ℝ
Cpos : 0 < C
hC : g' '' t ⊆ closedBall 0 C
p : P
x : G
hp : ‖p - q₀.1‖ < ε
hps : p ∈ s
hx : x ∉ k
this : g' (p, x) = 0
⊢ ‖0‖ ≤ C
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e'_3
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : ∫ (x : G), f x ∂μ = 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ z₀ = ∫ (t : G), ((lsmul ℝ ℝ) (f t)) z₀ ∂μ

Tactic:
[

Goal state after:
case e'_3
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : ∫ (x : G), f x ∂μ = 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ z₀ = ∫ (t : G), ((lsmul ℝ ℝ) (f t)) z₀ ∂μ
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case convert_2
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : ∫ (x : G), f x ∂μ = 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ (‖lsmul ℝ ℝ‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε

Tactic:
[

Goal state after:
case convert_2
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : ∫ (x : G), f x ∂μ = 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ (‖lsmul ℝ ℝ‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : 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, ∫ (x : G), φ i x ∂μ = 1
hφ : Tendsto (fun n ↦ support (φ n)) l (𝓝 0).smallSets
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)
hk : Tendsto k l (𝓝 x₀)
⊢ Tendsto (fun i ↦ (φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)

Tactic:
[

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : 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, ∫ (x : G), φ i x ∂μ = 1
hφ : Tendsto (fun n ↦ support (φ n)) l (𝓝 0).smallSets
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)
hk : Tendsto k l (𝓝 x₀)
⊢ Tendsto (fun i ↦ (φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : 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, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : ∀ ε > 0, ∀ᶠ (x : ι × G) in l ×ˢ 𝓝 x₀, dist (uncurry g x) z₀ < ε
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε

Tactic:
[

Goal state after:
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : 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, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : ∀ ε > 0, ∀ᶠ (x : ι × G) in l ×ˢ 𝓝 x₀, dist (uncurry g x) z₀ < ε
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ n, V n * k
⊢ IsGδ k

Tactic:
this

Goal state after:
G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
this : k = ⋂ n, V n * k
⊢ IsGδ (⋂ n, V n * k)
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁰ : CompleteSpace F
inst✝⁹ : AddGroup G
inst✝⁸ : SFinite μ
inst✝⁷ : SFinite ν
inst✝⁶ : μ.IsAddRightInvariant
inst✝⁵ : MeasurableAdd₂ G
inst✝⁴ : MeasurableNeg G
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ ∫ (y : G), ∫ (x : G), (L (f y)) (g (x - y)) ∂μ ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)

Tactic:
[

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁰ : CompleteSpace F
inst✝⁹ : AddGroup G
inst✝⁸ : SFinite μ
inst✝⁷ : SFinite ν
inst✝⁶ : μ.IsAddRightInvariant
inst✝⁵ : MeasurableAdd₂ G
inst✝⁴ : MeasurableNeg G
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ ∫ (y : G), ∫ (x : G), (L (f y)) (g (x - y)) ∂μ ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : 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✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
⊢ ∫ (t : G), ∫ (s : G), (L₂ ((L (f s)) (g (t - s)))) (k (x₀ - t)) ∂ν ∂μ =
    ∫ (t : G), ∫ (s : G), (L₃ (f s)) ((L₄ (g (t - s))) (k (x₀ - t))) ∂ν ∂μ

Tactic:
[

Goal state after:
𝕜 : 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✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
⊢ ∫ (t : G), ∫ (s : G), (L₂ ((L (f s)) (g (t - s)))) (k (x₀ - t)) ∂ν ∂μ =
    ∫ (t : G), ∫ (s : G), (L₃ (f s)) ((L₄ (g (t - s))) (k (x₀ - t))) ∂ν ∂μ
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e_f
𝕜 : 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✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
t : G
⊢ ∫ (x : G), (L₃ (f t)) ((L₄ (g (x - t))) (k (x₀ - t - (x - t)))) ∂μ =
    ∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ

Tactic:
[

Goal state after:
case e_f
𝕜 : 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✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
t : G
⊢ ∫ (x : G), (L₃ (f t)) ((L₄ (g (x - t))) (k (x₀ - t - (x - t)))) ∂μ =
    ∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
this : ⋃ f, support ↑f = s
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = s

Tactic:
[

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
this : ⋃ f, support ↑f = s
⊢ ∃ T, T.Countable ∧ ⋃ f ∈ T, support ↑f = s