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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ∞

Tactic:
by
  have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
  -- We start by applying the layer cake formula
  have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) := by fun_prop
  have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
  rw [lintegral_eq_lintegral_meas_le μ (Eventually.of_forall h_pos) h_meas.aemeasurable]
  have h_int : ∀ t, 0 < t → μ {a : E | t ≤ (1 + ‖a‖) ^ (-r)} =
      μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) := fun t ht ↦ by
    congr 1
    ext x
    simp only [mem_ofPred_eq, mem_closedBall_zero_iff]
    exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
  rw [setLIntegral_congr_fun measurableSet_Ioi h_int]
  set f := fun t : ℝ ↦ μ (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
  set mB := μ (Metric.ball (0 : E) 1)
  -- the next two inequalities are in fact equalities but we don't need that
  calc
    ∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
    _ ≤ (∫⁻ t in Ioc 0 1, f t) + ∫⁻ t in Ioi 1, f t := lintegral_union_le _ _ _
    _ < ∞ := ENNReal.add_lt_top.2 ⟨?_, ?_⟩
  · -- We use estimates from auxiliary lemmas to deal with integral from `0` to `1`
    have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1,
        f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦ by
      refine μ.addHaar_closedBall (0 : E) ?_
      rw [sub_nonneg]
      exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
    rw [setLIntegral_congr_fun measurableSet_Ioc h_int',
      lintegral_mul_const' _ _ measure_ball_lt_top.ne]
    exact ENNReal.mul_lt_top
      (finite_integral_rpow_sub_one_pow_aux (finrank ℝ E) hnr) measure_ball_lt_top
  · -- The integral from 1 to ∞ is zero:
    have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
      simp only [f, closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
    -- The integral over the constant zero function is finite:
    rw [setLIntegral_congr_fun measurableSet_Ioi h_int'', lintegral_const 0,
      zero_mul]
    exact WithTop.top_pos

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Compact.Basic

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ K ⊆ σ₁₂ c • U

Tactic:
refine hrU (σ₁₂ c) ?_

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁰ : RingHomIsometric σ₁₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module 𝕜₁ M₁
inst✝⁴ : Module 𝕜₂ M₂
inst✝³ : IsTopologicalAddGroup M₁
inst✝² : ContinuousConstSMul 𝕜₁ M₁
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : ContinuousSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
U : Set M₂
hU : U ∈ 𝓝 0
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrU : ∀ (c : 𝕜₂), r ≤ ‖c‖ → K ⊆ c • U
c : 𝕜₁
hc : r < ‖c‖
hcnz : c ≠ 0
⊢ r ≤ ‖σ₁₂ c‖
Module: Mathlib.Analysis.InnerProductSpace.Rayleigh

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMaxOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
⊢ ‖x‖ = ‖x₀‖

Tactic:
simpa using hx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hx₀ : x₀ ≠ 0
hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
hx₀' : 0 < ‖x₀‖
hx₀'' : x₀ ∈ sphere 0 ‖x₀‖
x : E
hx : x ∈ sphere 0 ‖x₀‖
⊢ ‖x‖ = ‖x₀‖

Tactic:
simpa using hx

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
h : (charpoly f).Splits
⊢ ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V)) f).det = (charpoly f).roots.prod

Tactic:
Matrix.det_eq_prod_roots_charpoly_of_splits (by simpa using h),

Goal state after:
K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
f : End K V
h : (charpoly f).Splits
⊢ ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V)) f).charpoly.roots.prod = (charpoly f).roots.prod
Module: Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative

Goal state before:
pp: 𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
⊢ ¬Function.Bijective ⇑S

Tactic:
rw [spectrum.mem_resolventSet_iff, ← IsUnit.neg_iff,
      ContinuousLinearMap.isUnit_iff_bijective] at h₂

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
h₂ : ¬Function.Bijective ⇑(-((algebraMap 𝕜 (X →L[𝕜] X)) μ - T))
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
⊢ ¬Function.Bijective ⇑S
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
⊢ Antitone (hT.eigenvalues hn)

Tactic:
rw [eigenvalues_def, ← Function.comp_assoc]
  refine Monotone.comp_antitone ?_ ?_
  · apply Tuple.monotone_sort
  intro _ _ h
  exact Fin.rev_le_rev.mpr h

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

Goal state before:
pp: case inl
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
⊢ ∃ g, HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨g, h₁.mono hg₃, hg₁, eLpNormEssSup_le_of_ae_bound (.of_forall fun x ↦ ?_)⟩

Goal state after:
case inl
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
ε : ℝ
hε : 0 < ε
f : E → F
h₁ : HasCompactSupport f
h₂ : Continuous f
g : E → F
hg₁ : ContDiff ℝ ∞ g
hg₂ : ∀ (x : E), dist (g x) (f x) < ε
hg₃ : Function.support g ⊆ Function.support f
x : E
⊢ ‖(f - g) x‖ ≤ ε
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ x = (P n) x

Tactic:
by rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
x✝ : ι
⊢ ‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2

pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2

Tactic:
· norm_cast

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ IsHilbertSum 𝕜 (fun b ↦ ↥(bif b then K else Kᗮ)) fun b ↦ (bif b then K else Kᗮ).subtypeₗᵢ

Tactic:
refine IsHilbertSum.mkInternal _ K.orthogonalFamily_self ?_

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ (⨆ i, bif i then K else Kᗮ).topologicalClosure
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hcg
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
⊢ Tendsto h (𝓝[s] x₀) (𝓝 0)

Tactic:
· rw [← sub_self a]
      apply Tendsto.sub hcg
      apply tendsto_const_nhds.congr'
      filter_upwards [h'ts] with x hx using by simp [hx]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun x ↦ a
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ IntegrableOn (fun a_1 ↦ φ i a_1 • a) t (μ.restrict s)

Tactic:
apply Integrable.smul_const

Goal state after:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
A : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x • h x ∂μ + (∫ (x : α) in t, φ i x ∂μ) • a) l (𝓝 a)
i : ι
hi : IntegrableOn (fun x ↦ φ i x • g x) s μ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
⊢ Integrable (φ i) ((μ.restrict s).restrict t)
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ Tendsto (fun i ↦ ∫ (x : α), φ i x • g x ∂μ) l (𝓝 a)

Tactic:
suffices Tendsto (fun i : ι ↦ ∫ x in univ, φ i x • g x ∂μ) l (𝓝 a) by simpa

Goal state after:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ Tendsto (fun i ↦ ∫ (x : α) in univ, φ i x • g x ∂μ) l (𝓝 a)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h₁ : HasCompactSupport f
h₂ : ContDiff ℝ ∞ f
k n : ℕ
g : E → ℝ := ⋯
⊢ Continuous fun x ↦ ‖iteratedFDeriv ℝ n f x‖

Tactic:
exact (h₂.of_le (mod_cast le_top)).continuous_iteratedFDeriv'.norm

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (fun x ↦ (L x).smulRight (f x)) x‖ ≤
    ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑L) x‖ * ‖iteratedFDeriv ℝ (n - i) (⇑f) x‖

Tactic:
by
          gcongr 1
          exact norm_iteratedFDeriv_le_of_bilinear_of_le_one (smulRightL ℝ G F)
            (by fun_prop) (f.smooth ⊤) x (mod_cast le_top) norm_smulRightL_le

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v 0) w) 0 =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w

Tactic:
Matrix.zero_empty,

Goal state after:
case zero_eq
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : NormedSpace ℝ V
inst✝⁴ : NormedAddCommGroup W
inst✝³ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
w : W
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v 0) w) ![] =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: 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
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
⊢ ∃ M > 0, ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε

Tactic:
rcases (hasBasis_cobounded_compl_closedBall (0 : F)).eventually_iff.1
        ((tendsto_order.1 h).2 (δ ^ finrank ℝ F * ε) (by positivity)) with ⟨M, -, hM⟩
      refine ⟨max M 1, zero_lt_one.trans_le (le_max_right _ _), fun x hx ↦ hM ?_⟩
      simp only [mem_compl_iff, mem_closedBall, dist_zero_right, le_max_iff, not_or, not_le] at hx
      simpa using hx.1

Goal state after:
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_7
W : Type u_8
x✝ : MeasurableSpace V
inst✝³ : AddCommGroup V
inst✝² : Module ℝ V
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ ∫ (v : V), Complex.exp (↑(-(L v) w) * Complex.I) • f v ∂μ = ∫ (v : V), Complex.exp (-↑((L v) w) * Complex.I) • f v ∂μ

Tactic:
Complex.ofReal_neg

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Asymptotics

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
by
  obtain ⟨C, hC⟩ := hf.bound
  obtain ⟨t, htl, ht⟩ := hC.exists_mem
  obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
  obtain ⟨w, hwl, hw⟩ := hfm.exists_mem
  refine eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩
  have : IsFiniteMeasure (μ.restrict s) := ⟨Measure.restrict_apply_univ s ▸ hμ⟩
  refine Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_
  filter_upwards [MeasureTheory.self_mem_ae_restrict hs]
  intro y hy
  exact ht (y, x) <| huv ⟨hu hy, hx.2⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Asymptotics

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x ↦ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a ≠ -1

Tactic:
apply_fun Complex.re

Goal state after:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x ↦ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ (-1).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = ↑(rexp (-x)) * (starRingEnd ℂ) (↑x ^ (s - 1))

Tactic:
cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (log ↑x * ((starRingEnd ℂ) s - 1)) = ↑(rexp (-x)) * (starRingEnd ℂ) (↑x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (log ↑x * ((starRingEnd ℂ) s - 1)) = ↑(rexp (-x)) * (starRingEnd ℂ) (↑x ^ (s - 1))

Tactic:
cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (log ↑x * ((starRingEnd ℂ) s - 1)) = ↑(rexp (-x)) * (starRingEnd ℂ) (cexp (log ↑x * (s - 1)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-x)

Tactic:
← rpow_two

Goal state after:
b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
⊢ (fun x ↦ x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)

Tactic:
← rpow_two

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
⊢ (fun x ↦ x ^ s * rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)