mathlib-initiative/mathlib-tactics huggingface dataset:
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) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
this : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
m n : ℕ
⊢ m < n → ‖μ‖ ≤ ‖T (f m) - T (f n)‖

Tactic:
hmn

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) μ
S : X →L[𝕜] X := T - μ • 1
K : NNReal
hK : AntilipschitzWith K ⇑S
h₂ : ¬Function.Surjective ⇑S
c : 𝕜
hc : 1 < ‖c‖
f : ℕ → X
hf_norm_lower : ∀ (n : ℕ), 1 ≤ ‖f n‖
hf_norm_upper : ∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1
hf_far : ∀ (n : ℕ), ∀ y ∈ LinearMap.range (↑S ^ (n + 1)), 1 ≤ ‖f n - y‖
hf_mem : ∀ {n m : ℕ}, m ≤ n → f n ∈ (↑S ^ m).range
hf_mem' : ∀ {n m : ℕ}, m ≤ n → S (f n) ∈ (↑S ^ (m + 1)).range
this : Std.Symm fun x₁ x₂ ↦ ‖μ‖ ≤ ‖T (f x₁) - T (f x₂)‖
m n : ℕ
hmn : m < n
⊢ ‖μ‖ ≤ ‖T (f m) - T (f n)‖
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
this : Fintype ↑(spectrum ℝ A) := Fintype.ofFinite ↑(spectrum ℝ A)
⊢ Function.Surjective fun i ↦ ⟨hA.eigenvalues i, ⋯⟩

Tactic:
rw [← Function.Surjective.of_comp_iff'
      (Equiv.setCongr hA.spectrum_real_eq_range_eigenvalues).bijective]

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA✝ : IsSelfAdjoint A
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
this : Fintype ↑(spectrum ℝ A) := Fintype.ofFinite ↑(spectrum ℝ A)
⊢ Function.Surjective (⇑(Equiv.setCongr ⋯) ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)
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 α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ |g x| = g x

Tactic:
abs_of_nonneg (hg_range x).1

Goal state after:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.OuterRegular
hp : p ≠ ∞
s u : Set α
s_closed : IsClosed[inst✝⁶] s
u_open : IsOpen[inst✝⁶] u
hsu : s ⊆ u
hs : μ s ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
η : ℝ≥0
η_pos : 0 < η
hη : ∀ (s : Set α), μ s ≤ ↑η → eLpNorm (s.indicator fun _x ↦ c) p μ ≤ ε
ηpos : 0 < ↑η
V : Set α
sV : V ⊇ s
V_open : IsOpen[inst✝⁶] V
h'V : μ V < ∞
hV : μ (V \ s) < ↑η
v : Set α := u ∩ V
hsv : s ⊆ v
hμv : μ v < ∞
g : C(α, ℝ)
hgv : EqOn (⇑g) 0 (u ∩ V)ᶜ
hgs : EqOn (⇑g) 1 s
hg_range : ∀ (x : α), g x ∈ Icc 0 1
x : α
⊢ g x = g x
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 α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
f g : α → E
f_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
f_mem : MemLp f p μ
hf : HasCompactSupport f
g_cont : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_mem : MemLp g p μ
hg : HasCompactSupport g
⊢ Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f + g) ∧
    MemLp (f + g) p μ ∧ HasCompactSupport (f + g)

Tactic:
exact ⟨f_cont.add g_cont, f_mem.add g_mem, hf.add hg⟩

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
n : ℤ
a : ℝ
this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z ↦ (fourier (-n)) z • f z) ↑x
⊢ fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fun z ↦ (fourier (-n)) z • f z) ↑x

Tactic:
rw [fourierCoeff, AddCircle.intervalIntegral_preimage T a (fun z => _ • _),
    volume_eq_smul_haarAddCircle, integral_smul_measure, ENNReal.toReal_ofReal hT.out.le,
    ← smul_assoc, smul_eq_mul, one_div_mul_cancel hT.out.ne', one_smul]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
a✝ : AddCircle T
ht : ↑↑(fourierLp 2 i) a✝ = (fourier i) a✝
⊢ (starRingEnd ℂ) (↑↑(fourierLp 2 i) a✝) * ↑↑f a✝ = (fourier (-i)) a✝ • ↑↑f a✝

Tactic:
rw [ht, ← fourier_neg, smul_eq_mul]

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 t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
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₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball 0 δ
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn (fun x ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : ‖∫ (x : α) in s ∩ u, φ i x • g x ∂μ‖ ≤ 2 * δ
⊢ 0 ≤ᵐ[μ.restrict s] fun a ↦ ‖g a‖

Tactic:
filter_upwards with x using norm_nonneg _

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✝⁹ : NormedField 𝕜
inst✝⁸ : NormedField 𝕜'
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
A : 𝓢(D, E) → F → G
hadd : ∀ (f g : 𝓢(D, E)) (x : F), A (f + g) x = A f x + A g x
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x : F), A (a • f) x = σ a • A f x
hsmooth : ∀ (f : 𝓢(D, E)), ContDiff ℝ ∞ (A f)
hbound :
  ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : F),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
f : 𝓢(D, E)
⊢ ∀ (k n : ℕ), ∃ C, ∀ (x : F), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (A f) x‖ ≤ C

Tactic:
by
        intro k n
        rcases hbound ⟨k, n⟩ with ⟨s, C, _, h⟩
        exact ⟨C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f, h f⟩

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

Goal state before:
pp: case right
ι : 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
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f x)) (g x)) x‖ ≤
    ‖B‖ * (↑n + 1) * ↑(n.choose (n / 2)) * (C * 2 ^ (l + k)) *
      ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f

Tactic:
grw [hnorm_mul]

Goal state after:
case right
ι : 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
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
⊢ ‖x‖ ^ k *
      (‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
        ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖) ≤
    ‖B‖ * (↑n + 1) * ↑(n.choose (n / 2)) * (C * 2 ^ (l + k)) *
      ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
hnc : ∀ x ∈ s, 0 ≤ c x
hmg : IntegrableOn g s μ
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x ∈ u → 0 < μ (u ∩ s)
h'c : ∀ y ∈ s, y ≠ x → c y < c x
hnc₀ : 0 < c x
h₀ : x ∈ s
hcg : ContinuousWithinAt g s x
x₀u : x ∈ u
⊢ False

Tactic:
exact hx.2 x₀u

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

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
⊢ μ (v ∩ s) ≠ ∞

Tactic:
exact (lt_of_le_of_lt (measure_mono inter_subset_right) hs.measure_lt_top).ne

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‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖) = (2 * π * ‖L‖) ^ n * (‖v‖ ^ (n + 1) * ‖f v‖)

Tactic:
by rw [pow_succ]; ring

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

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun x ↦ -log⁻¹ x) (x⁻¹ / log x ^ 2) x

pp: c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ioi c, 0 ≤ x⁻¹ / log x ^ 2

Tactic:
· intro t _
    convert! (hasDerivAt_inv_log (by grind : t ≠ 0) (by grind) (by grind)).neg using 1
    field

Goal state after:
c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ioi c, 0 ≤ x⁻¹ / log x ^ 2
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
fourier_real_eq,

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ ∫ (v : ℝ), 𝐞 (-(v * w)) • f v = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case convert_1
c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun t ↦ -(log t)⁻¹) (x⁻¹ / log x ^ 2) x

pp: case convert_2
c : ℝ
hc : 1 < c
⊢ Tendsto (fun t ↦ -(log t)⁻¹) atTop (𝓝 0)

Tactic:
· intro t _
    convert! (hasDerivAt_inv_log (by grind : t ≠ 0) (by grind) (by grind)).neg using 1
    field

Goal state after:
case convert_2
c : ℝ
hc : 1 < c
⊢ Tendsto (fun t ↦ -(log t)⁻¹) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case left.inl
x y : ℝ
hxy : (x, y) ∈ {q | 0 < q.1}
⊢ 0 < x ^ 2 + y ^ 2

pp: case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
· dsimp at hxy; linarith [sq_pos_of_ne_zero hxy.ne', sq_nonneg y]

Goal state after:
case left.inr
x y : ℝ
hxy : (x, y) ∈ {q | q.2 ≠ 0}
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable
    ((fun x ↦ f 0 (x 0) * ∏ i, f i.succ (x i.succ)) ∘
      ⇑{ toFun := fun f ↦ Fin.insertNth 0 f.1 f.2, invFun := fun f ↦ (f 0, Fin.removeNth 0 f), left_inv := ⋯,
          right_inv := ⋯ })
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))

Tactic:
Fin.insertNth_zero

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] {f : (i : Fin n) → E i → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable
    ((fun x ↦ f 0 (x 0) * ∏ i, f i.succ (x i.succ)) ∘
      ⇑{ toFun := fun f ↦ Fin.cons f.1 fun j ↦ cast ⋯ (f.2 j), invFun := fun f ↦ (f 0, Fin.removeNth 0 f),
          left_inv := ⋯, right_inv := ⋯ })
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) (volume.restrict (Ioi 0))

Tactic:
← IntegrableOn,

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬IntegrableOn (fun x ↦ rexp (-b * x ^ 2)) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_2
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    2 * ∫ (x : ℝ) in Ioi 0, rexp (-1 * x ^ 2)

Tactic:
rw [← integral_const_mul]
    refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
    have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ := by
      rw [← rpow_mul (le_of_lt hx)]
      norm_num
      rw [rpow_neg (le_of_lt hx), rpow_one]
    rw [smul_eq_mul, this]
    simp [field, (ne_of_lt (show 0 < x from hx)).symm]
    norm_num

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

Goal state before:
pp: case e'_3
⊢ √π = 2 * (√π / 2)

Tactic:
← mul_div_assoc,

Goal state after:
case e'_3
⊢ √π = 2 * √π / 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 : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (↑T - ↑x * I) ^ 2))

Tactic:
simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
      change I₁ T = I₂ T + I * (I₄ T - I₅ T)
      rw [mul_sub, ← C]
      abel

Goal state after:
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)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
⊢ Tendsto I₁ atTop (𝓝 ((↑π / b) ^ (1 / 2)))

Tactic:
have : I₁ = fun T : ℝ => I₂ T + verticalIntegral b c T := by
    ext1 T
    specialize C T
    rw [sub_eq_zero] at C
    unfold verticalIntegral
    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_sub]
    · simp_rw [(fun a b => by rw [sq]; ring_nf : ∀ a b : ℂ, (a - b * I) ^ 2 = (-a + b * I) ^ 2)]
      change I₁ T = I₂ T + I * (I₄ T - I₅ T)
      rw [mul_sub, ← C]
      abel
    all_goals apply Continuous.intervalIntegrable; fun_prop

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)
C : ∀ (T : ℝ), I₂ T - I₁ T + I * I₄ T - I * I₅ T = 0
this : I₁ = fun T ↦ I₂ T + verticalIntegral b c T
⊢ Tendsto I₁ atTop (𝓝 ((↑π / b) ^ (1 / 2)))
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
g : 𝓢(E, ℂ)
⊢ (toTemperedDistribution f) g = ∫ (x : E), g x • ↑↑f x ∂μ

Tactic:
by
  simp only [toTemperedDistribution, toPointwiseConvergenceCLM_apply, comp_apply _, toLpCLM_apply,
    lpPairing_eq_integral, lsmul_flip_apply, toSpanSingleton_apply]
  apply integral_congr_ae
  filter_upwards [g.coeFn_toLp (1 - p⁻¹)⁻¹ μ] with x hg
  rw [hg]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
⊢ (besselPotential E F (-2)) (Δ f) = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2 * (1 + ‖x‖ ^ 2) ^ (-1))) f

Tactic:
by
  rw [laplacian_eq_fourierMultiplierCLM, besselPotential,
    ContinuousLinearMap.map_smul_of_tower,
    fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]
  congr
  ext x
  simp

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Tactic:
refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fun f ↦ ⇑f) (mFourier (Pi.single i 1)) x ≠ (fun f ↦ ⇑f) (mFourier (Pi.single i 1)) y
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (mFourier (Pi.single i 1)) x ≠ (mFourier (Pi.single i 1)) y

Tactic:
mFourier_single,

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fourier 1) (x i) ≠ (mFourier (Pi.single i 1)) y
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fourier 1) (x i) ≠ (mFourier (Pi.single i 1)) y

Tactic:
mFourier_single,

Goal state after:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fourier 1) (x i) ≠ (fourier 1) (y i)