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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
⊢ HasTemperateGrowth ⇑f

Tactic:
apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_)
  · have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv]
    simp [this]
  · exact (f.le_opNorm x).trans (by simp [mul_add])

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
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re ⟪T x, y⟫_𝕜 + re ⟪T y, x⟫_𝕜 = re 2 * re ⟪T x, y⟫_𝕜
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4

Tactic:
ofNat_re

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : (↑T).IsSymmetric
M : ℝ := ⨆ x, |T.rayleighQuotient x|
nonneg : 0 ≤ M
hM : ∀ (x : E), |re ⟪T x, x⟫_𝕜| ≤ M * ‖x‖ ^ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
key : re ⟪T x, y⟫_𝕜 + re ⟪T y, x⟫_𝕜 = 2 * re ⟪T x, y⟫_𝕜
⊢ re ⟪T x, y⟫_𝕜 ≤ M * (‖x + y‖ ^ 2 + ‖x - y‖ ^ 2) / 4
Module: Mathlib.Analysis.Distribution.TestFunction

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
m : MeasurableSpace E
inst✝¹¹ : OpensMeasurableSpace E
F₁ : Type u_6
F₂ : Type u_7
F₃ : Type u_8
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : NormedSpace ℝ F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace 𝕜 F₂
inst✝⁵ : NormedAddCommGroup F₃
inst✝⁴ : NormedSpace 𝕜 F₃
inst✝³ : Algebra ℝ 𝕜
inst✝² : IsScalarTower ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : IsScalarTower ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
hφ : ¬LocallyIntegrableOn φ (↑Ω) μ
⊢ integralAgainstBilinCLM B μ φ = 0

Tactic:
ext
  simp [hφ]

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
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Tactic:
by
  let := InnerProductSpace.rclikeToReal 𝕜 E
  let hSA := hT.isSymmetric.restrictScalars.toSelfAdjoint.prop
  exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr

Goal state after:
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
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ¬HasEigenvalue (↑T) μ
⊢ ∃ K, AntilipschitzWith K ⇑(T - μ • 1)

Tactic:
antilipschitzWith_iff_exists_mul_le_norm

Goal state after:
𝕜 : Type u_1
X : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
T : X →L[𝕜] X
μ : 𝕜
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h : ¬HasEigenvalue (↑T) μ
⊢ ∃ c > 0, ∀ (x : X), c * ‖x‖ ≤ ‖(T - μ • 1) x‖
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
⊢ IsClosedEmbedding ⇑hA.cfcAux

Tactic:
refine LinearMap.isClosedEmbedding_of_injective (𝕜 := ℝ) (E := C(spectrum ℝ A, ℝ))
    (F := Matrix n n 𝕜) (f := hA.cfcAux) <| LinearMap.ker_eq_bot'.mpr fun f hf ↦ ?_

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C(↑(spectrum ℝ A), ℝ)
f : C(↑(spectrum ℝ A), ℝ)
hf : ↑hA.cfcAux f = 0
⊢ f = 0
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

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
μ : 𝕜
hμ : μ ≠ 0
hT : IsCompactOperator (μ • ⇑LinearMap.id)
⊢ FiniteDimensional 𝕜 ↥(eigenspace (↑T) μ)

Tactic:
IsCompactOperator.smul_iff₀ hμ

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
μ : 𝕜
hμ : μ ≠ 0
hT : IsCompactOperator ⇑LinearMap.id
⊢ FiniteDimensional 𝕜 ↥(eigenspace (↑T) μ)
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAB : ((A ⊙ B).submatrix Subtype.val Subtype.val).PosSemidef
⊢ 0 ≤ x.sum fun i xi ↦ x.sum fun j xj ↦ star xi * (A ⊙ B) i j * xj

Tactic:
simpa [Finsupp.sum, ← Finset.sum_attach x.support, ← Finset.subtype_mem_eq_attach,
    ← Finsupp.subtypeDomain_apply, ← Finsupp.support_subtypeDomain] using hAB.2 _

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

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq n
v : n → E
⊢ gram 𝕜 v = 1 ↔ Orthonormal 𝕜 v

Tactic:
simp [← Matrix.ext_iff, orthonormal_iff_ite, Matrix.one_apply]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ + x⁻) a = abs a

Tactic:
abs_eq_cfcₙ_norm a ha

Goal state after:
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ cfcₙ (fun x ↦ x⁺ + x⁻) a = cfcₙ (fun x ↦ ‖x‖) a
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ EqOn (⇑g) f S ∧ support ⇑g ⊆ support f

Tactic:
let t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}

Goal state after:
E : Type u_1
F : Type u_2
H : Type u_3
M : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
f : M → F
ε : M → ℝ
n : ℕ∞
f_cont : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
ε_cont : Continuous[inst✝⁴, _] ε
ε_pos : ∀ (x : M), 0 < ε x
S U : Set M
hS : IsClosed[inst✝⁴] S
hU : U ∈ 𝓝ˢ S
hfU : ContMDiffOn I 𝓘(ℝ, F) (↑n) f U
dist_f_f : ∀ (x : M), dist (f x) (f x) < ε x
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
⊢ ∃ g, (∀ (x : M), dist (g x) (f x) < ε x) ∧ EqOn (⇑g) f S ∧ support ⇑g ⊆ support f
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g,
    HasCompactSupport g ∧
      eLpNorm (fun x ↦ f x - g x) 1 μ ≤ ε ∧
        Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g 1 μ

Tactic:
exact hf.exists_hasCompactSupport_eLpNorm_sub_le ENNReal.one_ne_top hε

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ ⟪lp.single 2 i a, f⟫ = ⟪a, ↑f i⟫

Tactic:
by
  refine (hasSum_inner (lp.single 2 i a) f).unique ?_
  simp_rw [lp.coeFn_single]
  convert! hasSum_ite_eq i ⟪a, f i⟫ using 1
  ext j
  split_ifs with h
  · subst h; rw [Pi.single_eq_same]
  · simp [Pi.single_eq_of_ne h]

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

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Tactic:
by
  simp_rw [fourier_apply, add_zsmul, toCircle_add, Circle.coe_mul]

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

Goal state before:
pp: case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (range fun n ↦ (toLp p haarAddCircle ℂ) (fourier n)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
rw [range_comp']

Goal state after:
case e'_9
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
e_3✝ : Complex.instSemiring = NormedField.toNormedCommRing.toSemiring
e_6✝ : Lp.instModule ≍ Lp.instModule
⊢ span ℂ (⇑(toLp p haarAddCircle ℂ) '' range fourier) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: 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
v : V
⊢ ‖2‖ * π * ‖(L v).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
Complex.norm_two,

Goal state after:
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
v : V
⊢ 2 * π * ‖(L v).smulRight (f v)‖ = 2 * π * ‖L v‖ * ‖f v‖
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 : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
⊢ c ∈ Ioi (M / δ) → ∀ x ∈ uᶜ, dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε

Tactic:
(hc : M / δ < c)

Goal state after:
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 : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
⊢ ∀ x ∈ uᶜ, dist (0 x) (c ^ finrank ℝ F * φ (c • x)) < ε
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
⊢ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) =
    ↑((eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ).toNNReal * 2 ^ k) *
      ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = ∫ (x : ℝ) in Iic 0 ∪ Ioi 0, f |x|

Tactic:
Iic_union_Ioi,

Goal state after:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ), f |x| = ∫ (x : ℝ) in univ, f |x|
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : 0 < a
c : ℝ
⊢ IntegrableOn (fun x ↦ rexp (a * x)) (Iic c) volume

Tactic:
have := Integrable.norm <| integrableOn_exp_mul_complex_Iic (a := a) (by simpa using! ha) c
  simpa [Complex.norm_exp] using! this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a c m : ℝ
ha : a < -1
hc : -m < c
⊢ IntegrableOn (fun x ↦ (x + m) ^ a) (Ioi c) volume

Tactic:
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x := by
    intro x hx
    convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
    · simp [show a + 1 ≠ 0 by linarith]
    left; linarith [mem_Ici.mp hx, id_eq x]
  have ht : Tendsto (fun t ↦ ((t + m) ^ (a + 1)) / (a + 1)) atTop (nhds (0 / (a + 1))) := by
    rw [← neg_neg (a + 1)]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp
      (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _
  exact integrableOn_Ioi_deriv_of_nonneg' hd
    (fun t ht ↦ rpow_nonneg (by linarith [mem_Ioi.mp ht]) a) ht

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case inr
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : -1 < s
this : IntegrableOn (fun x ↦ x ^ s) (Ioi 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this

Goal state after:
case inr
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : -1 < s
this : s < -1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (fun x ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

Tactic:
obtain hs | hs := eq_or_lt_of_le hs

Goal state after:
case inl
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (fun x ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume

case inr
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ IntegrableOn (fun x ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
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
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atTop.IsMeasurablyGenerated
inst✝ : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ

Tactic:
by
  refine integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case h
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖(-a) ^ s * rexp (-b * a ^ 2)‖ ≤ a ^ s * rexp (-b * a ^ 2)

Tactic:
have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
    filter_upwards [ae_restrict_mem this] with x hx
    have h'x : 0 ≤ x := le_of_lt hx
    rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (exp_pos _).le]
    apply mul_le_mul_of_nonneg_right _ (exp_pos _).le
    simpa [abs_of_nonneg h'x] using abs_rpow_le_abs_rpow (-x) s

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
⊢ polarCoord.source =ᵐ[volume] univ

Tactic:
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 := by
    apply Measure.addHaar_submodule
    rw [Ne, LinearMap.ker_eq_top]
    intro h
    have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
    simp at this

Goal state after:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
B : volume ↑(LinearMap.snd ℝ ℝ ℝ).ker = 0
⊢ polarCoord.source =ᵐ[volume] univ
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e_f.e_a.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 = ↑p.1 ^ 2

Tactic:
conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]

Goal state after:
case e_f.e_a.e_a
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ (↑p.1 * Complex.cos ↑p.2) ^ 2 + (↑p.1 * Complex.sin ↑p.2) ^ 2 =
    (Complex.sin ↑p.2 ^ 2 + Complex.cos ↑p.2 ^ 2) * ↑p.1 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0

Tactic:
have :=
      integral_boundary_rect_eq_zero_of_differentiableOn (fun z => cexp (-b * z ^ 2)) (-T)
        (T + c * I)
        (by
          refine Differentiable.differentiableOn (Differentiable.const_mul ?_ _).cexp
          exact differentiable_pow 2)

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
this :
  (((∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(-↑T).im * I) ^ 2)) -
          ∫ (x : ℝ) in (-↑T).re..(↑T + ↑c * I).re, cexp (-b * (↑x + ↑(↑T + ↑c * I).im * I) ^ 2)) +
        I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(↑T + ↑c * I).re + ↑y * I) ^ 2)) -
      I • ∫ (y : ℝ) in (-↑T).im..(↑T + ↑c * I).im, cexp (-b * (↑(-↑T).re + ↑y * I) ^ 2) =
    0
⊢ I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_3
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ c ^ 2 * ↑‖w‖ ^ 2 = ∑ i, (c * ↑(w.ofLp i)) ^ 2

Tactic:
· simp only [EuclideanSpace.norm_eq, Real.norm_eq_abs, sq_abs, mul_pow, ← Finset.mul_sum]
    congr
    norm_cast
    rw [sq_sqrt]
    exact Finset.sum_nonneg (fun i _hi ↦ by positivity)

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

Goal state before:
pp: E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((𝓕 g) x)

Tactic:
by
  simpa using! VectorFourier.integral_bilin_fourierIntegral_eq_flip M (L := innerₗ V)
    continuous_fourierChar continuous_inner f.integrable g.integrable

Goal state after:
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case a
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ dsupport ⇑(TemperedDistribution.delta x) ⊆ {x}

Tactic:
intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Goal state after:
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case a
E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
⊢ dsupport ⇑(delta x) ⊆ {x}

Tactic:
intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁ + -f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + -⟪f₂, g⟫_[𝕜, w]

Tactic:
wInner_add_left,

Goal state after:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f₁ f₂ g : (i : ι) → E i
⊢ ⟪f₁, g⟫_[𝕜, w] + ⟪-f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + -⟪f₂, g⟫_[𝕜, w]