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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C

Tactic:
have : (∀ x, ‖iteratedFDeriv ℝ i f x‖ ≤ C) ↔ (∀ x ∈ K, ‖iteratedFDeriv ℝ i f x‖ ≤ C) := by
    congrm ∀ x, ?_
    by_cases hx : x ∈ K
    · simp [hx]
    · simp [hx, f.iteratedFDeriv_zero_on_compl hx, hC]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n : ℕ∞
K : Compacts E
C : ℝ
hC : 0 ≤ C
i : ℕ
f : 𝓓^{n}_{K}(E, F)
this : (∀ (x : E), ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C) ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n K i) f ≤ C ↔ ↑i ≤ n → ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB : ((A ⊙ B).submatrix Subtype.val Subtype.val).PosDef
⊢ 0 <
    ∑ x_1 ∈ Finset.subtype (fun x_1 ↦ x_1 ∈ x.support) x.support,
      ∑ x_2 ∈ Finset.subtype (fun x_2 ↦ x_2 ∈ x.support) x.support,
        (starRingEnd 𝕜) (x ↑x_1) * (A ↑x_1 ↑x_2 * B ↑x_1 ↑x_2) * x ↑x_2

Tactic:
← Finsupp.subtypeDomain_apply,

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB : ((A ⊙ B).submatrix Subtype.val Subtype.val).PosDef
⊢ 0 <
    ∑ x_1 ∈ Finset.subtype (fun x_1 ↦ x_1 ∈ x.support) x.support,
      ∑ x_2 ∈ Finset.subtype (fun x_2 ↦ x_2 ∈ x.support) x.support,
        (starRingEnd 𝕜) ((Finsupp.subtypeDomain (fun x_3 ↦ x_3 ∈ x.support) x) x_1) * (A ↑x_1 ↑x_2 * B ↑x_1 ↑x_2) *
          (Finsupp.subtypeDomain (fun x_3 ↦ x_3 ∈ x.support) x) x_2
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
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

Tactic:
suffices ∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x by
    rcases this with ⟨g, hg⟩
    exact ⟨g, fun x ↦ (hg x).1, fun x ↦ (hg x).2.1, fun x ↦ mt (hg x).2.2⟩

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), g x ∈ t x
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
⊢ eLpNorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ

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‖₊ ^ 2 ∂μ ≠ ∞

Tactic:
· rw [← ENNReal.rpow_natCast, eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top, eLpNorm', ←
      ENNReal.rpow_mul, one_div, h_two]
    simp [enorm_eq_nnnorm]

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‖₊ ^ 2 ∂μ ≠ ∞
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
t : M → Set F := fun x ↦ {y | dist y (f x) < ε x ∧ (x ∈ S → y = f x) ∧ (f x = 0 → y = 0)}
t_conv : ∀ (x : M), Convex ℝ (t x)
x : M
hx : x ∉ S
this✝ : ∀ᶠ (y : M) in 𝓝 x, y ∉ S ∧ dist (f x) (f y) < ε y
this : ∀ᶠ (y : M) in 𝓝 x, (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)
y : M
hy : y ∈ {x_1 | (fun y ↦ (y ∉ S ∧ dist (f x) (f y) < ε y) ∧ (f y = 0 → f x = 0)) x_1}
⊢ y ∈ S → (fun x_1 ↦ f x) y = f y

Tactic:
by simp [hy.1.1]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ E
inst✝¹⁷ : NormedAddCommGroup F
inst✝¹⁶ : NormedSpace ℝ F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : SMulCommClass ℝ 𝕜 F
inst✝¹³ : NormedAddCommGroup F'
inst✝¹² : NormedSpace ℝ F'
inst✝¹¹ : NormedSpace 𝕜 F'
inst✝¹⁰ : SMulCommClass ℝ 𝕜 F'
n n₁ n₂ k✝ : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
hcont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
    (Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖
C₀ : ℝ
hC₀ : ∀ x ∈ ↑K, ‖(Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖‖ ≤ C₀
hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ K
⊢ ‖B‖ * (2 ^ k * ((Finset.Iic k).sup fun m ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K m) φ * ‖C₀‖) =
    ‖B‖ * 2 ^ k * ‖C₀‖ * ((Finset.Iic k).sup fun m ↦ ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K m) φ

Tactic:
ring

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ 2 * ↑π / ↑T * (↑n * ↑x) * Complex.I = 2 * ↑π * Complex.I * ↑n * ↑x / ↑T

Tactic:
ring

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ ↑(toCircle (n • ↑x)) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
by
  rw [← fourier_apply]; exact fourier_coe_apply

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i : ι
x : G i
⊢ ∑' (i_1 : ι), (V i_1) (↑(lp.single 2 i x) i_1) = (V i) x

Tactic:
← tsum_ite_eq i (fun _ ↦ V i x)

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
inst✝ : DecidableEq ι
i : ι
x : G i
⊢ ∑' (i_1 : ι), (V i_1) (↑(lp.single 2 i x) i_1) = ∑' (b' : ι), if b' = i then (V i) x else 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
⊢ ∀ {a : C(AddCircle T, ℂ)}, a ∈ (adjoin ℂ (range fourier)).carrier → star a ∈ (adjoin ℂ (range fourier)).carrier

Tactic:
change Algebra.adjoin ℂ (range (fourier (T := T))) ≤
      star (Algebra.adjoin ℂ (range (fourier (T := T))))
    refine adjoin_le ?_
    rintro - ⟨n, rfl⟩
    exact subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩

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
v : E
i : ι
⊢ ↑(b.repr v) i = ⟪b.repr (b i), b.repr v⟫

Tactic:
b.repr_self,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
v : E
i : ι
⊢ ↑(b.repr v) i = ⟪lp.single 2 i 1, b.repr v⟫
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
i j : ι
⊢ ⟪b.repr (b i), b.repr (b j)⟫ = if i = j then 1 else 0

Tactic:
b.repr_self,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪lp.single 2 i 1, b.repr (b j)⟫ = if i = j then 1 else 0
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
i j : ι
⊢ ⟪lp.single 2 i 1, b.repr (b j)⟫ = if i = j then 1 else 0

Tactic:
b.repr_self,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪lp.single 2 i 1, lp.single 2 j 1⟫ = if i = j then 1 else 0
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)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i ↦ 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ ↑f i • b.repr (b i) = b.repr (↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))

Tactic:
b.repr_self,

Goal state after:
ι : 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)
i : ι
this✝ : NormedSpace 𝕜 ↥(lp (fun _i ↦ 𝕜) 2) := inferInstance
this : lp.single 2 i (↑f i) = ↑f i • lp.single 2 i 1
⊢ ↑f i • lp.single 2 i 1 = b.repr (↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))
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)
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ((innerSL 𝕜) (b i)) (b j) = Pi.single j 1 i

Tactic:
simpa [innerSL_apply_apply, Pi.single_apply] using orthonormal_iff_ite.mp b.orthonormal i j

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

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
α β : ℂ
⊢ α * cexp β = cexp β * α

Tactic:
ring

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

Goal state before:
pp: case e'_8
T : ℝ
n : ℤ
x : ℝ
y : ℂ
⊢ 2 * ↑π * I * ↑n * y / ↑T = y * (2 * ↑π * I * ↑n / ↑T)

Tactic:
ring

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

Goal state before:
pp: case e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y * ↑T / (-2 * ↑π * I * ↑n)

Tactic:
ring

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

Goal state before:
pp: a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
u✝ v✝ w✝ : ℂ
⊢ u✝ * (↑(b - a) / v✝ * w✝) = ↑(b - a) / v✝ * (u✝ * w✝)

Tactic:
ring

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

Goal state before:
pp: a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
⊢ ↑(b - a) / (-2 * ↑π * I * ↑n) = ↑(b - a) * (1 / (-2 * ↑π * I * ↑n))

Tactic:
ring

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

Goal state before:
pp: case e_a
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ (f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a) * ↑(b - a)

Tactic:
ring

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

Goal state before:
pp: case e_a
a b : ℝ
hab : a < b
f f' : ℝ → ℂ
n : ℤ
hn : n ≠ 0
hf : ContinuousOn f [[a, b]]
hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x
hf' : IntervalIntegrable f' volume a b
hT : Fact (0 < b - a)
this : ∀ (u v w : ℂ), u * (↑(b - a) / v * w) = ↑(b - a) / v * (u * w)
s2 : ↑b = ↑a
⊢ 1 / ↑(b - a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x) =
    1 / (-2 * ↑π * I * ↑n) * (↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, f' x * (fourier (-n)) ↑x))

Tactic:
ring

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

Goal state before:
pp: case e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' ↦ (L v) w') (L v) w
e_8✝ : addCommGroup = instNormedAddCommGroup.toAddCommGroup
e_9✝ : NormedSpace.complexToReal.toModule ≍ instInnerProductSpaceRealComplex.toModule
y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = ↑((L v) y) * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))

Tactic:
ring

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = 2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))

Tactic:
ring

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v y : V
w : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L y) w) = 2 * ↑π * I * ↑((L y) w) * ↑(𝐞 (-(L v) w))

Tactic:
ring

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
v : V
⊢ 2 * π * (‖L‖ * ‖v‖) * ‖f v‖ = 2 * π * ‖L‖ * ‖v‖ * ‖f v‖

Tactic:
ring

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
v : V
n : ℕ
m : Fin n → W
⊢ 2 ^ n * π ^ n * ((‖L‖ ^ n * ‖v‖ ^ n * ∏ x, ‖m x‖) * ‖f v‖) = 2 ^ n * π ^ n * ‖L‖ ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ x, ‖m x‖

Tactic:
ring

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

Goal state before:
pp: case inl
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
m : ℕ
hm : m ≤ n
⊢ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m =
    ↑(n.descFactorial m) * (‖L‖ ^ m * ‖L‖ ^ (n - m)) * ‖v‖ ^ (n - m)

Tactic:
ring

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

Goal state before:
pp: case e_f
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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : ↑k ≤ K
v : V
hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C
T : (W →L[ℝ] ℝ) [×n]→L[ℝ] W [×n]→L[ℝ] ℝ :=
  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight
I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x ↦ L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤
      ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x ↦ L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A : ContDiff ℝ K fun y ↦ T fun x ↦ L y
i : ℕ
⊢ ↑(k.choose i) * (↑(n.descFactorial i) * ‖L‖ ^ n * ‖v‖ ^ (n - i)) * ‖iteratedFDeriv ℝ (k - i) f v‖ =
    ↑(k.choose i) * ↑(n.descFactorial i) * ‖L‖ ^ n * (‖v‖ ^ (n - i) * ‖iteratedFDeriv ℝ (k - i) f v‖)

Tactic:
ring

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

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

Tactic:
ring

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

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

Tactic:
ring

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAlgebra ℝ 𝕜
inst✝⁴ : NormedAddCommGroup D
inst✝³ : NormedSpace ℝ D
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace 𝕜 F
L : E →L[ℝ] G →L[ℝ] ℝ
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) +
      ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f) =
    2 * ‖L‖ * ↑(max 1 n) * max ((SchwartzMap.seminorm 𝕜 (k + 1) n) f) ((SchwartzMap.seminorm 𝕜 k (n - 1)) f)

Tactic:
ring

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 : Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
v : V
⊢ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖f v‖)

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ

Tactic:
refine (norm_integral_le_integral_norm _).trans (le_of_eq ?_)
  simp_rw [Circle.norm_smul]

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 * ‖v‖ * ‖f v‖)

Tactic:
ring

Goal state after: