mathlib-initiative/mathlib-tactics huggingface dataset:
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'
x : G
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd G
inst✝ : μ.IsNegInvariant
h : ConvolutionExistsAt f g x L μ
⊢ Integrable (fun t ↦ (L (f (x - t))) (g t)) μ

Tactic:
by
  convert! h.comp_sub_left x
  simp_rw [sub_sub_self]

Goal state after:
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
⊢ Tendsto (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) (l.curry (𝓝 x)) (𝓝 0)

Tactic:
have := difference_quotients_converge_uniformly hf' hf hfg

Goal state after:
case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this : TendstoUniformlyOnFilter (fun n y ↦ (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y ↦ (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
⊢ Tendsto (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) (l.curry (𝓝 x)) (𝓝 0)
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
a : α
ha : HasFDerivAt (fun x ↦ F x a) (F' a) x₀
x : H
⊢ ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a - (F' a) (x - x₀)‖ = ‖‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀))‖

Tactic:
norm_smul_of_nonneg (nneg _)

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
a : α
ha : HasFDerivAt (fun x ↦ F x a) (F' a) x₀
x : H
⊢ ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a - (F' a) (x - x₀)‖ = ‖x - x₀‖⁻¹ * ‖F x a - F x₀ a - (F' a) (x - x₀)‖
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : 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✝¹⁰ : 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✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
⊢ MapsTo (fun x ↦ (id x, v x)) s (s ×ˢ univ)

Tactic:
intro x hx

Goal state after:
𝕜 : 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✝¹⁰ : 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✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case hnhds
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, μ t = 0

Tactic:
intro x hx

Goal state after:
case hnhds
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
x : α
hx : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, μ t = 0
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u

Tactic:
intro x hx

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
H : ν.IsEverywherePos s
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ u = ν u
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
⊢ ⋂ n, V n * k ⊆ k

Tactic:
intro x hx

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
x : G
hx : x ∈ ⋂ n, V n * k
⊢ x ∈ 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), (L (f y)) (∫ (x : G), g x ∂μ) ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)

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

Goal state after:
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 }
⊢ s ⊆ ⋃ f, support ↑f

Tactic:
intro x hx

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 }
x : E
hx : x ∈ s
⊢ x ∈ ⋃ f, support ↑f
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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : x ∈ s
⊢ ∃ n, x ∈ support (g n)

Tactic:
rw [← hT] at hx

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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : x ∈ ⋃ f ∈ T, support ↑f
⊢ ∃ n, x ∈ support (g n)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : last N ≤ i
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
· have I : i = last N := top_le_iff.1 H
    have := (a.rpos (last N)).le
    simp only [I, add_nonneg this this, dist_self]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case inr.refine_1.h₁
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) := ⋯
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := ⋯
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
⊢ (support fun x ↦ ∑' (n : ℕ), (r n • g n) x) ⊆ s

Tactic:
intro x hx

Goal state after:
case inr.refine_1.h₁
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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
x : E
hx : x ∈ support fun x ↦ ∑' (n : ℕ), (r n • g n) x
⊢ x ∈ s
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case inr.refine_1.h₂
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) := ⋯
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := ⋯
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
⊢ s ⊆ support fun x ↦ ∑' (n : ℕ), (r n • g n) x

Tactic:
intro x hx

Goal state after:
case inr.refine_1.h₂
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 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
x : E
hx : x ∈ s
⊢ x ∈ support fun x ↦ ∑' (n : ℕ), (r n • g n) x
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_3.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ∀ x ∈ Ioo 0 1 ×ˢ univ, x.1 ≠ 0

Tactic:
intro x hx

Goal state after:
case refine_3.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
x : ℝ × E
hx : x ∈ Ioo 0 1 ×ˢ univ
⊢ x.1 ≠ 0
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : 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
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
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
s : Set P
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
⊢ MapsTo (fun x ↦ (id x, v x)) s (s ×ˢ univ)

Tactic:
intro x hx

Goal state after:
𝕜 : 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
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
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
s : Set P
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : 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
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
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
f : G → E
n : ℕ∞
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
⊢ ContDiffOn 𝕜 (↑n) (fun q ↦ (g q.1 ⋆[L, μ] f) q.2) (s ×ˢ univ)

Tactic:
by
  simpa only [convolution_flip] using contDiffOn_convolution_right_with_param L.flip hs hk hgs hf hg

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : 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
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
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
s : Set P
n : ℕ∞
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
⊢ MapsTo (fun x ↦ (id x, v x)) s (s ×ˢ univ)

Tactic:
intro x hx

Goal state after:
𝕜 : 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
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
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
s : Set P
n : ℕ∞
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
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 𝕜 (↑n) (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ
Module: Mathlib.Analysis.Calculus.BumpFunction.Convolution

Goal state before:
pp: case g_supp
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
i : ι
⊢ (fun y ↦ x₀ - y) ⁻¹' ball 0 (φ i).rOut ⊆ closedBall x₀ (φ i).rOut

Tactic:
intro x hx

Goal state after:
case g_supp
G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : NormedSpace ℝ E'
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : CompleteSpace E'
inst✝² : BorelSpace G
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddHaarMeasure
ι : Type u_1
φ : ι → ContDiffBump 0
l : Filter ι
K : ℝ
hφ : Tendsto (fun i ↦ (φ i).rOut) l (𝓝 0)
h'φ : ∀ᶠ (i : ι) in l, (φ i).rOut ≤ K * (φ i).rIn
hg : LocallyIntegrable g μ
x₀ : G
h₀ : Tendsto (fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ((Besicovitch.vitaliFamily μ).filterAt x₀) (𝓝 0)
hφ' : Tendsto (fun i ↦ (φ i).rOut) l (𝓝[>] 0)
this : Tendsto (((fun a ↦ ⨍ (y : G) in a, ‖g y - g x₀‖ ∂μ) ∘ fun r ↦ closedBall x₀ r) ∘ fun i ↦ (φ i).rOut) l (𝓝 0)
i : ι
x : G
hx : x ∈ (fun y ↦ x₀ - y) ⁻¹' ball 0 (φ i).rOut
⊢ x ∈ closedBall x₀ (φ i).rOut