mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Layercake

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
inst✝ : SFinite μ
f_nn : 0 ≤ f
f_mble : Measurable f
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_mble : Measurable g
g_nn : ∀ t > 0, 0 ≤ g t
g_intble' : ∀ (t : ℝ), 0 ≤ t → IntervalIntegrable g volume 0 t
integrand_eq : ∀ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) = ∫⁻ (t : ℝ) in Ioc 0 (f ω), ENNReal.ofReal (g t)
s : ℝ
a : α
h_copy : s ∉ Ioc 0 (f a)
h : 0 < s → f a < s
h' : ¬0 < s
this : s ∉ Ioi 0
⊢ (Ioc 0 (f a)).indicator (fun t ↦ ENNReal.ofReal (g t)) s =
    ENNReal.ofReal (g s) * (Ioi 0).indicator (fun x ↦ 1) s * (Ici s).indicator (fun x ↦ 1) (f a)

Tactic:
simp only [this, h', indicator_of_notMem, not_false_iff, mul_zero,
            zero_mul, mem_Ioc, false_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
g : ℝ → ℝ
μ : Measure α
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
G : ℝ → ℝ
G_mble : Measurable G
G_nn : 0 ≤ G
g_eq_G : g =ᵐ[volume.restrict (Ioi 0)] G
g_eq_G_on : ∀ (t : ℝ), g =ᵐ[volume.restrict (Ioc 0 t)] G
G_intble : ∀ t > 0, IntervalIntegrable G volume 0 t
F : α → ℝ
F_mble : Measurable F
F_nn : 0 ≤ F
f_eq_F : f =ᵐ[μ] F
eq₁ :
  ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t) =
    ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ F a} * ENNReal.ofReal (G t)
ω : α
fω_nn✝ : f ω = F ω
fω_nn : 0 ≤ F ω
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc 0 (F ω)), g x = G x

Tactic:
exact g_eq_G_on (F ω)

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

Goal state before:
pp: case neg
H : Type u_8
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
r : ℝ
t : Set ℝ := {y | 1 / 2 < y}
ht : (Set.range fun x ↦ 1 + ‖x‖ ^ 2) ⊆ t
hdiff : ContDiffOn ℝ ∞ (fun x ↦ x ^ r) t
hunique : UniqueDiffOn ℝ t
N k : ℕ
hk : max r ((↑N - r) * Real.log 2 / Real.log (3 / 2)) ≤ ↑k
hk₁ : r ≤ ↑k
hk₂ : Real.log 2 * (↑N - r) ≤ Real.log (3 / 2) * ↑k
n : ℕ
hn : n ≤ N
x : ℝ
hx : x ∈ t
this : ContDiffAt ℝ (↑n) (fun x ↦ x ^ r) x
hx' : 1 / 2 < x
hx'' : 0 < x
h✝ : r - ↑n < 0
h : 0 < ↑n - r
⊢ |x| ^ (r - ↑n) ≤ (1 + |x|) ^ k

Tactic:
calc
    /- In the case `0 < n - r`, we need the factor `Real.log 2 / (Real.log (3 / 2))` to control
    the growth near `‖x‖ = 1/2`. -/
    _ = x ^ (-(n - r)) := by
      rw [neg_sub]
      congr
      simpa using hx''.le
    _ ≤ (2 : ℝ) ^ (n - r) := by
      simp only [one_div, Set.mem_ofPred_eq, t] at hx
      rw [Real.rpow_neg_eq_inv_rpow]
      gcongr
      exact ((inv_lt_comm₀ hx'' (by norm_num)).mpr hx).le
    _ = Real.exp (Real.log 2 * (n - r)) := by
      rw [Real.rpow_def_of_pos]
      norm_num
    _ ≤ Real.exp (Real.log (3 / 2) * k) := by
      gcongr 1
      apply le_trans _ hk₂
      gcongr
    _ ≤ (3 / 2) ^ k := by
      rw [← Real.rpow_natCast, Real.rpow_def_of_pos]
      norm_num
    _ ≤ _ := by
      gcongr
      grind

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

Goal state before:
pp: C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)

Tactic:
rcases le_total x 1 with h'x | h'x

Goal state after:
case inl
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : x ≤ 1
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)

case inr
C₁ C₂ : ℝ
k l : ℕ
x f : ℝ
hx : 0 ≤ x
hf : 0 ≤ f
h₁ : f ≤ C₁
h₂ : x ^ (k + l) * f ≤ C₂
this✝ : 0 ≤ C₂
this : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-↑l) = ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
h'x : 1 ≤ x
⊢ x ^ k * f ≤ ((1 + x) / 2) ^ (-↑l) * (C₁ + C₂)
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: case refine_1
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono ⇑(Equiv.trans σ (graphEquiv₁ f))
i j : Fin n
hij : i < j
hfij : f (σ i) = f (σ j)
⊢ σ i < σ j

Tactic:
exact ((Prod.Lex.toLex_lt_toLex.1 <| h hij).resolve_left hfij.not_lt).2

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
μ : 𝕜
inst✝ : CompleteSpace X
hT : IsCompactOperator ⇑T
hμ : μ ≠ 0
h₁ : ¬HasEigenvalue (↑T) μ
h₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - μ • 1
⊢ False

Tactic:
obtain ⟨K, hK : AntilipschitzWith K S⟩ := antilipschitz_of_not_hasEigenvalue hT hμ 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₂ : μ ∉ resolventSet 𝕜 T
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
⊢ False
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))).charpoly

Tactic:
conjStarAlgAut_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).charpoly
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ hA.eigenvalues))).rank

Tactic:
conjStarAlgAut_apply,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
| (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).rank
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: n : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
| (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ⋯.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ ⋯.eigenvalues))).trace = 0

Tactic:
conjStarAlgAut_apply,

Goal state after:
n : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
| (↑⋯.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⋯.eigenvalues) * star ↑⋯.eigenvectorUnitary).trace = 0
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ Set.range ⇑f ⊆
    spectrum ℝ
      (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) ha.eigenvectorUnitary)
        (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩)))

Tactic:
conjStarAlgAut_apply,

Goal state after:
case a
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
a : Matrix n n 𝕜
ha : a.IsHermitian
f : C(↑(spectrum ℝ a), ℝ)
⊢ Set.range ⇑f ⊆
    spectrum ℝ
      (↑ha.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨ha.eigenvalues i, ⋯⟩) *
        star ↑ha.eigenvectorUnitary)
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
f : ℝ → ℝ
⊢ (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues))).charpoly =
    ∏ i, (X - C ↑(f (hA.eigenvalues i)))

Tactic:
conjStarAlgAut_apply,

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
f : ℝ → ℝ
⊢ (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ f ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).charpoly =
    ∏ i, (X - C ↑(f (hA.eigenvalues i)))
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ ((∫⁻ (a : α), ‖↑↑f a‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2)) ^ ↑2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

Tactic:
←
      ENNReal.rpow_mul,

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ‖↑↑f a‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2 * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ Complex.exp (↑(2 * π / T * (↑n * (T / 2 / ↑n))) * Complex.I) = -1

Tactic:
convert Complex.exp_pi_mul_I

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ 2 * π / T * (↑n * (T / 2 / ↑n)) = π
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
n : ℤ
x : ℝ
hx : f x = g x
⊢ (fourier (-n)) ↑x • f x = (fourier (-n)) ↑x • g x

Tactic:
rw [hx]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n m : ℤ
⊢ ↑(fourierBasis.repr (fourierLp 2 n)) m = Pi.single n 1 m

Tactic:
HilbertBasis.repr_apply_apply,

Goal state after:
T : ℝ
hT : Fact (0 < T)
n m : ℤ
⊢ inner ℂ (fourierBasis m) (fourierLp 2 n) = Pi.single n 1 m
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case cont
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 μ
n : ℕ
hn : ↑n ≤ N
⊢ Integrable (fun v ↦ fourierPowSMulRight L f v n) μ

Tactic:
exact integrable_fourierPowSMulRight L (hf n hn) h'f

Goal state after:
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
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
⊢ ContDiff ℝ (↑N) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)

Tactic:
by
  by_cases h'f : Integrable f μ
  · exact (hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff
  · have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by
      ext w; simp [fourierIntegral, integral, h'f]
    simpa [this] using! contDiff_const

Goal state after:
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
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
hn : ↑n ≤ N
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n

Tactic:
induction n with
  | zero =>
    ext w m
    simp only [iteratedFDeriv_zero_apply, fourierPowSMulRight_apply, pow_zero, Finset.univ_eq_empty,
      neg_apply, ContinuousLinearMap.flip_apply, Finset.prod_empty, one_smul,
      fourierIntegral_continuousMultilinearMap_apply' ((h'f 0 bot_le))]
  | succ n ih =>
    ext w m
    have J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ := by
      specialize h'f (n + 1) hn
      rwa [iteratedFDeriv_succ_eq_comp_left, Function.comp_def,
          LinearIsometryEquiv.integrable_comp_iff (𝕜 := ℝ) (φ := fderiv ℝ (iteratedFDeriv ℝ n f))]
        at h'f
    suffices H : (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w)
          (m 0) (Fin.tail m) =
        (-(2 * π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -L (m x) w) • ∫ v, 𝐞 (-L v w) • f v ∂μ by
      rw [fourierIntegral_continuousMultilinearMap_apply' (h'f _ hn)]
      simp only [iteratedFDeriv_succ_apply_left, fourierPowSMulRight_apply, neg_apply,
        ContinuousLinearMap.flip_apply]
      rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)),
          ← fourierIntegral_continuousLinearMap_apply' J]
      exact H
    have h'n : n < N := (Nat.cast_lt.mpr n.lt_succ_self).trans_le hn
    rw [fourierIntegral_fderiv _ (h'f n h'n.le)
      (hf.differentiable_iteratedFDeriv (mod_cast h'n)) J]
    simp only [ih h'n.le, fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply,
      neg_smul, smul_neg, neg_neg, smul_apply, fourierPowSMulRight_apply, ← coe_smul (E := E),
      smul_smul]
    congr 1
    simp only [ofReal_prod, ofReal_neg, pow_succ, mul_neg, Fin.prod_univ_succ, neg_mul,
      ofReal_mul, neg_neg, Fin.tail_def]
    ring

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

Goal state before:
pp: case h
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✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
this : ↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) =ᵐ[μ] ↑↑f - g
⊢ (eLpNorm (↑↑f - g) p μ).toReal ≤ ε

Tactic:
grw [hg₃, ENNReal.toReal_ofReal hε.le]

Goal state after:
case hb
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✝³ : SecondCountableTopologyEither E F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
p : ℝ≥0∞
hp : p ≠ ∞
hp' : Fact (1 ≤ p)
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : IsFiniteMeasureOnCompacts μ
f : ↥(Lp F p μ)
ε : ℝ
hε : 0 < ε
g : E → F
hg₁ : HasCompactSupport g
hg₂ : ContDiff ℝ ∞ g
hg₃ : eLpNorm (↑↑f - g) p μ ≤ ENNReal.ofReal ε
this : ↑↑f - ↑↑((hg₁.toSchwartzMap hg₂).toLp p μ) =ᵐ[μ] ↑↑f - g
⊢ ENNReal.ofReal ε ≠ ∞
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 < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem

Goal state after:
α : 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 < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i ↦ f (i, x)) s μ
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✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
⊢ (fun x ↦ ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g

Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem

Goal state after:
α : 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✝¹ : NormedSpace ℝ E
inst✝ : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ (fun x ↦ ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
⊢ False

Tactic:
rcases le_or_gt s (-1) with hs | hs

Goal state after:
case inl
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : s ≤ -1
⊢ False

case inr
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
hs : -1 < s
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0)

Tactic:
apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul

Goal state after:
case left
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (fun x ↦ ↑x ^ (s - 1)) (Ioi 0)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioc 0 Y)

Tactic:
apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul

Goal state after:
case left
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ContinuousOn (fun x ↦ ↑x ^ (s - 1)) (Ioc 0 Y)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : NormedCommRing 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hf : ∀ (i : ι), Integrable (f i) (μ i)
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
by
  let e := (equivFin ι).symm
  simp_rw [← (measurePreserving_piCongrLeft _ e).integrable_comp_emb
    (MeasurableEquiv.measurableEmbedding _),
    ← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Function.comp_def,
    Equiv.piCongrLeft_apply_apply]
  exact .fin_nat_prod (fun i ↦ hf _)

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ ∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹

Tactic:
by
  have hb' : b ≠ 0 := by contrapose! hb; rw [hb, zero_re]
  have A : ∀ x : ℂ, HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2))
    (x * cexp (-b * x ^ 2)) x := by
    intro x
    convert! ((hasDerivAt_pow 2 x).const_mul (-b)).cexp.const_mul (-(2 * b)⁻¹) using 1
    field
  have B : Tendsto (fun y : ℝ ↦ -(2 * b)⁻¹ * cexp (-b * (y : ℂ) ^ 2))
    atTop (𝓝 (-(2 * b)⁻¹ * 0)) := by
    refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)
    simp_rw [norm_cexp_neg_mul_sq b]
    exact tendsto_exp_atBot.comp
      ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))
  convert!
    integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => (A ↑x).comp_ofReal)
      (integrable_mul_cexp_neg_mul_sq hb).integrableOn B using 1
  simp only [mul_zero, ofReal_zero, zero_pow, Ne,
    not_false_iff, Complex.exp_zero, mul_one, sub_neg_eq_add, zero_add, reduceCtorEq]

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

Goal state before:
pp: f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (↑polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p)

Tactic:
by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]

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

Goal state before:
pp: b : ℂ
c T : ℝ
⊢ rexp (-((↑b.re + ↑b.im * I) * (↑T + ↑c * I) ^ 2).re) =
    rexp (-((↑b.re + ↑b.im * I).re * T ^ 2 - 2 * (↑b.re + ↑b.im * I).im * c * T - (↑b.re + ↑b.im * I).re * c ^ 2))

Tactic:
simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]

Goal state after:
b : ℂ
c T : ℝ
⊢ rexp
      (-(b.re * ((T + (c * 0 - 0 * 1)) * (T + (c * 0 - 0 * 1)) - (0 + (c * 1 + 0 * 0)) * (0 + (c * 1 + 0 * 0))) -
          b.im * ((T + (c * 0 - 0 * 1)) * (0 + (c * 1 + 0 * 0)) + (0 + (c * 1 + 0 * 0)) * (T + (c * 0 - 0 * 1))))) =
    rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ 1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t) =
    1 / ↑r * (1 / ↑r) ^ (a - 1) * ∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
← MeasureTheory.integral_const_mul,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ∫ (a_1 : ℝ) in Ioi 0, 1 / ↑r * ((1 / ↑r) ^ (a - 1) * ↑a_1 ^ (a - 1) * cexp (-↑a_1)) =
    ∫ (a_1 : ℝ) in Ioi 0, 1 / ↑r * (1 / ↑r) ^ (a - 1) * (↑a_1 ^ (a - 1) * cexp (-↑a_1))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (↑π / b) ^ (↑Finset.univ.card * 2⁻¹) * ∏ x, cexp (c x ^ 2 / (4 * b)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))

Tactic:
← Complex.exp_sum,

Goal state after:
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ι → ℂ
⊢ (↑π / b) ^ (↑Finset.univ.card * 2⁻¹) * cexp (∑ x, c x ^ 2 / (4 * b)) =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i, c i ^ 2) / (4 * b))
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
u : 𝓢(E, ℂ)
hu : x ∉ tsupport ⇑u
⊢ (TemperedDistribution.delta x) u = 0

Tactic:
apply image_eq_zero_of_notMem_tsupport hu

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

Goal state before:
pp: E : Type u_11
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
u : 𝓓^{n}(Ω, ℝ)
hu : x ∉ tsupport ⇑u
⊢ (delta x) u = 0

Tactic:
apply image_eq_zero_of_notMem_tsupport hu

Goal state after: