-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem tendsto_integral_comp_smul_smul_of_integrable'
    {φ : F → ℝ} (hφ : ∀ x, 0 ≤ φ x) (h'φ : ∫ x, φ x ∂μ = 1)
    (h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0))
    {g : F → E} {x₀ : F} (hg : Integrable g μ) (h'g : ContinuousAt g x₀) :
    Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • (x₀ - x))) • g x ∂μ)
      atTop (𝓝 (g x₀))

Proof state:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))

Tactic:
apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If

Result:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
⊢ ContinuousAt f 0

Proof state:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • f x ∂μ)
    atTop (𝓝 (f 0)) := by
  apply tendsto_integral_comp_smul_smul_of_integrable hφ h'φ h If
  have A : ContinuousAt g (x₀ - 0) := by simpa using h'g
  exact A.comp <| by fun_prop

Result:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Proof state:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
A : ContinuousAt g (x₀ - 0)
⊢ ContinuousAt (HSub.hSub x₀) 0

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.e'_3.h
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
⊢ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ = ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ

Tactic:
conv_rhs => rw [← integral_add_left_eq_self x₀ (μ := μ)
  (f := fun x ↦ (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x)), ← integral_neg_eq_self]

Result:
case h.e'_3.h
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
c : ℝ
⊢ ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ =
    ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ

Proof state:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
have If : Integrable f μ := by simpa [f, sub_eq_add_neg] using (hg.comp_add_left x₀).comp_neg

Result:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))