mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
h0 : P 0 = 0
⊢ ∑ i ∈ Finset.range 0, succSub P i = P 0

Tactic:
simp [h0]

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

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
V : Type u_7
F : Type u_8
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ E
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
x✝ : ℕ × ℕ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (fderiv ℝ ⇑f) x‖ ≤ 1 * ({(k, n + 1)}.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
by
      simpa only [schwartzSeminormFamily_apply, Seminorm.comp_apply, Finset.sup_singleton,
        one_smul, norm_iteratedFDeriv_fderiv, one_mul] using f.le_seminorm 𝕜 k (n + 1) x

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
inst✝ : ∀ (i : ι), CompleteSpace (G i)
hVortho : OrthogonalFamily 𝕜 G V
hVtotal : ⊤ ≤ (⨆ i, (V i).range).topologicalClosure
⊢ Function.Surjective ⇑hVortho.linearIsometry.toLinearMap

Tactic:
exact LinearMap.range_eq_top.mp
        (eq_top_iff.mpr <| hVtotal.trans_eq hVortho.range_linearIsometry.symm)

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
b : HilbertBasis ι 𝕜 E
f : ↥(lp (fun x ↦ 𝕜) 2)
H : (fun i ↦ ↑f i • b i) = fun b_1 ↦ ↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) b_1)
this : HasSum (fun i ↦ lp.single 2 i (↑f i)) f
⊢ HasSum (fun b_1 ↦ ↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) b_1)) (b.repr.symm f)

Tactic:
exact (↑b.repr.symm.toContinuousLinearEquiv : ℓ²(ι, 𝕜) →L[𝕜] E).hasSum this

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 : ι → E
hv : Orthonormal 𝕜 v
hsp : (span 𝕜 (Set.range v))ᗮ = ⊥
⊢ (span 𝕜 (Set.range v))ᗮ = ⊥

Tactic:
hsp

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 : ι → E
hv : Orthonormal 𝕜 v
hsp : (span 𝕜 (Set.range v))ᗮ = ⊥
⊢ ⊥ = ⊥
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case e'_6
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
⊢ (fun a_1 ↦ ‖liftIoc (b - a) a f a_1‖ ^ 2) =ᵐ[haarAddCircle] fun a_1 ↦ ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) a_1‖ ^ 2

Tactic:
filter_upwards [h.coeFn_toLp] with x hx

Goal state after:
a b : ℝ
f : ℝ → ℂ
hab : a < b
hL2 : MemLp f 2 (volume.restrict (Ioc a (a + (b - a))))
this : Fact (0 < b - a)
h : MemLp (liftIoc (b - a) a f) 2 haarAddCircle
x : AddCircle (b - a)
hx : ↑↑(MemLp.toLp (liftIoc (b - a) a f) h) x = liftIoc (b - a) a f x
⊢ ‖liftIoc (b - a) a f x‖ ^ 2 = ‖↑↑(MemLp.toLp (liftIoc (b - a) a f) h) x‖ ^ 2
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i ↦ fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a ↦ ‖fourierCoeff (⇑f) a • fourier a‖

Tactic:
simp_rw [norm_smul, fourier_norm, mul_one]

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
sum_L2 : HasSum (fun i ↦ fourierCoeff (⇑f) i • fourierLp 2 i) ((toLp 2 haarAddCircle ℂ) f)
⊢ Summable fun a ↦ ‖fourierCoeff (⇑f) a‖
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‖ * ‖f v‖) = 2 * π * ‖L v‖ * ‖f v‖

Tactic:
← mul_assoc

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‖ * ‖f v‖ = 2 * π * ‖L v‖ * ‖f v‖
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✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖)

Tactic:
← mul_assoc

Goal state after:
ι : 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✝⁴ : NormedSpace 𝕜 F
inst✝³ : SMulCommClass ℝ 𝕜 F
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖c‖ * ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) 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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
rw [add_comm, add_pow]

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * 1 ^ (k - m) * ↑(k.choose m)) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    2 ^ m.1 * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
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[ℝ] ℝ
c : 𝕜
g : 𝓢(E, F)
x : E
⊢ (L x).smulRight ((c • g) x) = (RingHom.id 𝕜) c • (L x).smulRight (g x)

Tactic:
ext v

Goal state after:
ι : 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[ℝ] ℝ
c : 𝕜
g : 𝓢(E, F)
x : E
v : G
⊢ ((L x).smulRight ((c • g) x)) v = ((RingHom.id 𝕜) c • (L x).smulRight (g x)) v
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case neg
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 : ¬Integrable f μ
⊢ ContDiff ℝ (↑N) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)

Tactic:
have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by
      ext w; simp [fourierIntegral, integral, h'f]

Goal state after:
case neg
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 : ¬Integrable f μ
this : fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f = 0
⊢ ContDiff ℝ (↑N) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f)
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✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' : ∀ (N : ℕ), 1 ≤ N → N ≤ n → ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this : ‖iteratedFDeriv ℝ n (⇑f ∘ g) x‖ ≤ ↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k * (↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * ↑n ! * 2 ^ k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
⊢ (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k' * seminorm_f) ≤
    (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k') * ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
← mul_assoc

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✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
hbound : ∀ i ≤ n, ‖iteratedFDeriv ℝ i (⇑f) (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' : ∀ (N : ℕ), 1 ≤ N → N ≤ n → ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this : ‖iteratedFDeriv ℝ n (⇑f ∘ g) x‖ ≤ ↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k * (↑n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * ↑n ! * 2 ^ k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
⊢ (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k') * seminorm_f ≤
    (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * ↑n ! * 2 ^ k') * ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
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 φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ = ∫ (x : F) in closedBall 0 1, c ^ finrank ℝ F * φ (c • x) ∂μ

Tactic:
rw [integral_const_mul, setIntegral_comp_smul_of_pos _ _ _ hc, smul_eq_mul, ← mul_assoc,
      mul_inv_cancel₀ (by positivity), _root_.smul_closedBall _ _ zero_le_one]

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 φ μ
this : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1)
c : ℝ
hc : 0 < c
⊢ ∫ (x : F) in closedBall 0 c, φ x ∂μ = 1 * ∫ (x : F) in closedBall (c • 0) (‖c‖ * 1), φ x ∂μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ ∫ (t : ℝ) in Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)

Tactic:
by
  refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) ?_
  suffices
    Tendsto (fun x : ℝ => ((x : ℂ) ^ (a + 1) - (c : ℂ) ^ (a + 1)) / (a + 1)) atTop
      (𝓝 <| -c ^ (a + 1) / (a + 1)) by
    refine this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
    dsimp only
    rw [integral_cpow, id]
    refine Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩
    apply_fun Complex.re
    rw [Complex.neg_re, Complex.one_re]
    exact ha.ne
  simp_rw [← zero_sub, sub_div]
  refine (Tendsto.div_const ?_ _).sub_const _
  rw [tendsto_zero_iff_norm_tendsto_zero]
  refine
    (tendsto_rpow_neg_atTop (by linarith : 0 < -(a.re + 1))).congr'
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
  simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]

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

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (fun x ↦ -x - -b * x ^ p) atTop atTop

Tactic:
refine Tendsto.congr' ?_ this
    refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)
    rw [mem_Ioi] at hx
    rw [rpow_sub_one hx.ne']
    field

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

Goal state before:
pp: r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
rcases eq_or_ne θ 0 with (rfl | h'θ)

Goal state after:
case inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

case inr
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
h'θ : θ ≠ 0
⊢ ((r, θ).1 * cos (r, θ).2, (r, θ).1 * sin (r, θ).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case inl
r : ℝ
hr : r ∈ Ioi 0
hθ : 0 ∈ Ioo (-π) π
⊢ ((r, 0).1 * cos (r, 0).2, (r, 0).1 * sin (r, 0).2) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}

Tactic:
simpa using! hr

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

Goal state before:
pp: ⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0} →
      ((√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            cos (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2,
          (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).1 *
            sin (√(x.1 ^ 2 + x.2 ^ 2), (Complex.equivRealProd.symm x).arg).2) =
        x

Tactic:
rintro ⟨x, y⟩ _

Goal state after:
x y : ℝ
a✝ : (x, y) ∈ {q | 0 < q.1} ∪ {q | q.2 ≠ 0}
⊢ ((√((x, y).1 ^ 2 + (x, y).2 ^ 2), (Complex.equivRealProd.symm (x, y)).arg).1 *
        cos (√((x, y).1 ^ 2 + (x, y).2 ^ 2), (Complex.equivRealProd.symm (x, y)).arg).2,
      (√((x, y).1 ^ 2 + (x, y).2 ^ 2), (Complex.equivRealProd.symm (x, y)).arg).1 *
        sin (√((x, y).1 ^ 2 + (x, y).2 ^ 2), (Complex.equivRealProd.symm (x, y)).arg).2) =
    (x, 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:
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.Gamma.Basic

Goal state before:
pp: case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
rw [Nat.floor_of_nonpos]
    · lia
    · linarith

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ GammaAux ⌊1⌋₊ 0 = 0

Tactic:
Nat.floor_one,

Goal state after:
⊢ GammaAux 1 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : c ∈ {c | 0 < c.re}
| ↑π / c

Tactic:
rw [← cpow_one (↑π / c)]

Goal state after:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : c ∈ {c | 0 < c.re}
| (↑π / c) ^ 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ (↑s).GammaIntegral.re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
Complex.GammaIntegral_ofReal,

Goal state after:
s : ℝ
hs : 0 < s
⊢ (↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑((c ^ (1 / 2)) ^ finrank ℝ V) * (↑(π ^ (↑(finrank ℝ V) / 2)) * cexp ↑(-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2)) =
    (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)

Tactic:
← mul_assoc

Goal state after:
case e_f.e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun c ↦ ∫ (w : V), (c ^ finrank ℝ V * φ (c • (v - w))) • f w) atTop (𝓝 (f v))
B : Tendsto (fun c ↦ ∫ (w : V), ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w) atTop (𝓝 (f v))
c : ℝ
hc : 0 < c
w : V
⊢ ↑((c ^ (1 / 2)) ^ finrank ℝ V) * ↑(π ^ (↑(finrank ℝ V) / 2)) * cexp ↑(-π ^ 2 * ‖c ^ (1 / 2) • (v - w)‖ ^ 2) =
    (↑π * ↑c) ^ (↑(finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext v

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕⁻ (𝓕 f) v = f v
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext v

Goal state after:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕 (𝓕⁻ f) v = f v
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
x : UnitAddTorus d
⊢ (mFourier (-n)) x = (starRingEnd ℂ) ((mFourier n) x)

Tactic:
by
  simp only [mFourier, Pi.neg_apply, fourier_neg, ContinuousMap.coe_mk, map_prod]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ 𝓕 (f₁ ⋆[B, volume] f₂) ξ = 𝓕 (f₂ ⋆[B.flip, volume] f₁) ξ

Tactic:
rw [convolution_flip]

Goal state after: