mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ∞
⊢ Memℓp (c • f) ∞

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove
    refine memℓp_infty ⟨‖c‖ * A, ?_⟩
    rintro a ⟨i, rfl⟩
    dsimp only [Pi.smul_apply]
    refine (norm_smul_le _ _).trans ?_
    gcongr
    exact hA ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl.inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
_i : Nonempty α
inhabited_h : Inhabited α
⊢ 0 ≤ ‖f‖

Tactic:
exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ≤ ‖f‖

Tactic:
rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']

Goal state after:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ ‖↑f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
Module: Mathlib.Analysis.SpecialFunctions.PolynomialExp

Goal state before:
pp: case monomial
n : ℕ
c : ℝ
⊢ Tendsto (fun x ↦ eval x ((monomial n) c) / rexp x) atTop (𝓝 0)

Tactic:
simpa [exp_neg, div_eq_mul_inv, mul_assoc]
    using tendsto_const_nhds.mul (tendsto_pow_mul_exp_neg_atTop_nhds_zero n)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case pos
α : 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
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
have h_ball : ball x₀ ε ∈ 𝓝 x₀ := ball_mem_nhds x₀ ε_pos

Goal state after:
case pos
α : 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₀
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
Module: Mathlib.Analysis.InnerProductSpace.Calculus

Goal state before:
pp: n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ ContDiffAt ℝ (↑n) (fun y ↦ (√(1 - ‖y‖ ^ 2))⁻¹) y

Tactic:
have h : (0 : ℝ) < (1 : ℝ) - ‖(y : E)‖ ^ 2 := by
    rwa [mem_ball_zero_iff, ← _root_.abs_one, ← abs_norm, ← sq_lt_sq, one_pow, ← sub_pos] at hy

Goal state after:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
y : E
hy : y ∈ ball 0 1
h : 0 < 1 - ‖y‖ ^ 2
⊢ ContDiffAt ℝ (↑n) (fun y ↦ (√(1 - ‖y‖ ^ 2))⁻¹) y
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
𝕜 : 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
g : P → G → E'
s : Set P
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)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
p : P
x : G
hp : (p, x).1 ∈ s
⊢ (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (p, x) = (fun x ↦ 0) (p, x)

Tactic:
apply integral_eq_zero_of_ae (Eventually.of_forall (fun y ↦ ?_))

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
g : P → G → E'
s : Set P
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)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
p : P
x : G
hp : (p, x).1 ∈ s
y : G
⊢ (L (f y)) (g (p, x).1 ((p, x).2 - y)) = 0 y
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case inr
𝕜 : 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✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
⊢ HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) x₀

Tactic:
let K' := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1

Goal state after:
case inr
𝕜 : 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✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
⊢ HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) x₀
Module: Mathlib.Analysis.Calculus.ContDiff.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✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := ⋯
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := ⋯
hK' : IsCompact K'
⊢ Integrable (fun t ↦ (L (f t)) (g (x₀ - t))) μ

Tactic:
· exact hcg.convolutionExists_right L hf hg.continuous x₀

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

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
hF_int : IntervalIntegrable (F x₀) μ a b
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))
h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x ↦ F x t) (F' t) x₀
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
by
  simp_rw [AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff, eventually_and] at hF_meas hF'_meas
  rw [ae_restrict_uIoc_iff] at h_lip h_diff
  have H₁ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.1 hF_int.1 hF'_meas.1 h_lip.1
      bound_integrable.1 h_diff.1
  have H₂ :=
    hasFDerivAt_integral_of_dominated_loc_of_lip hs hF_meas.2 hF_int.2 hF'_meas.2 h_lip.2
      bound_integrable.2 h_diff.2
  exact ⟨⟨H₁.1, H₂.1⟩, H₁.2.sub H₂.2⟩

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

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : UniformCauchySeqOnFilter f' l l'
u : Set ((𝕜 →L[𝕜] G) × (𝕜 →L[𝕜] G))
⊢ u ∈ uniformity (𝕜 →L[𝕜] G) →
    ∀ᶠ (m : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l',
      ((fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)) m.1.1 m.2,
          (fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)) m.1.2 m.2) ∈
        u

Tactic:
hu

Goal state after:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f' : ι → 𝕜 → G
l' : Filter 𝕜
hf' : UniformCauchySeqOnFilter f' l l'
u : Set ((𝕜 →L[𝕜] G) × (𝕜 →L[𝕜] G))
hu : u ∈ uniformity (𝕜 →L[𝕜] G)
⊢ ∀ᶠ (m : (ι × ι) × 𝕜) in (l ×ˢ l) ×ˢ l',
    ((fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)) m.1.1 m.2,
        (fun n z ↦ ContinuousLinearMap.smulRight 1 (f' n z)) m.1.2 m.2) ∈
      u
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_1
𝕜 : 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₀ ≤ ε
⊢ BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ x₀ - t) ⁻¹' ball 0 R)

Tactic:
rw [bddAbove_def]

Goal state after:
case refine_1
𝕜 : 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₀ ≤ ε
⊢ ∃ x, ∀ y ∈ (fun i ↦ ‖g i‖) '' (fun t ↦ x₀ - t) ⁻¹' ball 0 R, y ≤ x
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst✝²] u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (μ.everywherePosSubset s)

Tactic:
hu

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : OpensMeasurableSpace α
hs : MeasurableSet s
u : Set α
u_open : IsOpen[inst✝²] u
hu : μ.everywherePosSubset s = s \ u
⊢ MeasurableSet (s \ u)
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst✝¹] s
u : Set α
u_open : IsOpen[inst✝¹] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed[inst✝¹] (μ.everywherePosSubset s)

Tactic:
hu

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsClosed[inst✝¹] s
u : Set α
u_open : IsOpen[inst✝¹] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsClosed[inst✝¹] (s \ u)
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst✝¹] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (μ.everywherePosSubset s)

Tactic:
hu

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen[inst✝¹] u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (s \ u)
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos.e_f.inr.inl
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : t ∈ Ioo 0 x
⊢ (Ioo 0 x).indicator (fun t ↦ (L (f t)) (g (x - t))) t = (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t))

pp: case pos.e_f.inr.inr
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : x ≤ t
⊢ (Ioo 0 x).indicator (fun t ↦ (L (f t)) (g (x - t))) t = (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t))

Tactic:
· rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
          indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]

Goal state after:
case pos.e_f.inr.inr
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : x ≤ t
⊢ (Ioo 0 x).indicator (fun t ↦ (L (f t)) (g (x - t))) t = (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t))
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e'_7
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0

Tactic:
by_cases ht : 0 < t

Goal state after:
case pos
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : 0 < t
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0

case neg
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
t : ℝ
ht : ¬0 < t
⊢ (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) = 0
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ Continuous[instTopologicalSpaceProd, _] (uncurry fun x y ↦ f (y * x) * (D (y * x))⁻¹ * g x)

pp: G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ HasCompactSupport (uncurry fun x y ↦ f (y * x) * (D (y * x))⁻¹ * g x)

Tactic:
· apply Continuous.mul ?_ (hg.comp continuous_fst)
        exact (hf.comp (continuous_snd.mul continuous_fst)).mul
          ((D_cont.comp (continuous_snd.mul continuous_fst)).inv₀ (fun x ↦ (D_pos _).ne'))

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ HasCompactSupport (uncurry fun x y ↦ f (y * x) * (D (y * x))⁻¹ * g x)
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case succ
𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg : ContDiffOn 𝕜 (↑↑n.succ) (↿g) (s ×ˢ univ)
⊢ ContDiffOn 𝕜 (↑↑n.succ) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
| succ n ih =>

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
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B'

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
hx : x ∈ closedBall 0 (1 - D)
⊢ y D x = 1

Tactic:
by
  change (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1
  have B : ∀ y : E, y ∈ ball x D → φ y = 1 := by
    have C : ball x D ⊆ ball 0 1 := by
      apply ball_subset_ball'
      simp only [mem_closedBall] at hx
      linarith only [hx]
    intro y hy
    simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]
    intro h'y
    linarith only [mem_ball.1 (C hy), h'y]
  have Bx : φ x = 1 := B _ (mem_ball_self Dpos)
  have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B
  rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']
  simp only [lsmul_apply, smul_eq_mul, integral_mul_const, w_integral E Dpos, Bx,
    one_mul]

Goal state after: