mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
⊢ (gram 𝕜 v).PosDef

Tactic:
have := Fintype.ofFinite n

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Finite n
v : n → E
h_li : LinearIndependent 𝕜 v
this : Fintype n
⊢ (gram 𝕜 v).PosDef
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
⊢ ‖f‖ ^ 2 = RCLike.re (∫ (a : α), ⟪↑↑f a, ↑↑f a⟫ ∂μ)

Tactic:
integral_inner_eq_sq_eLpNorm,

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
⊢ ‖f‖ ^ 2 = RCLike.re ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : 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
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B (c • f x)) (φ x) ∂μ = (RingHom.id 𝕜) c • ∫ (x : E), (B (f x)) (φ x) ∂μ

Tactic:
map_smul,

Goal state after:
case pos
𝕜 : 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
m : MeasurableSpace E
inst✝¹⁰ : OpensMeasurableSpace E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝⁹ : NormedAddCommGroup F₁
inst✝⁸ : NormedSpace 𝕜 F₁
inst✝⁷ : NormedSpace ℝ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace 𝕜 F₃
inst✝² : SMulCommClass ℝ 𝕜 F₁
inst✝¹ : NormedSpace ℝ F₃
inst✝ : SMulCommClass ℝ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
μ : Measure E
φ : E → F₂
c : 𝕜
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (c • B (f x)) (φ x) ∂μ = (RingHom.id 𝕜) c • ∫ (x : E), (B (f x)) (φ x) ∂μ
Module: Mathlib.Analysis.Normed.Lp.SmoothApprox

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
⊢ ∃ g, HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε

Tactic:
have hε₂' : 0 < ENNReal.ofReal (ε / 2) := by positivity

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : MeasurableSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ F
μ : Measure E
inst✝ : IsFiniteMeasureOnCompacts μ
p : ℝ≥0∞
hp : p ≠ ∞
hp₂ : 1 ≤ p
f : E → F
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hε₂ : 0 < ε / 2
hε₂' : 0 < ENNReal.ofReal (ε / 2)
⊢ ∃ g, HasCompactSupport g ∧ ContDiff ℝ ∞ g ∧ eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
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✝ hV : OrthogonalFamily 𝕜 G V
c : 𝕜
f : ↥(lp G 2)
⊢ ∑' (i : ι), (V i) (↑(c • f) i) = (RingHom.id 𝕜) c • ∑' (i : ι), (V i) (↑f i)

Tactic:
by
    simpa only [LinearIsometry.map_smul, Pi.smul_apply, lp.coeFn_smul] using!
      (hV.summable_of_lp f).tsum_const_smul c

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

Goal state before:
pp: T : ℝ
n : ℤ
⊢ (fourier n) 0 = 1

Tactic:
rw [← QuotientAddGroup.mk_zero, fourier_coe_apply, Complex.ofReal_zero, mul_zero,
    zero_div, Complex.exp_zero]

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

Goal state before:
pp: T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)

Tactic:
rw [← neg_smul, ← fourier_apply]

Goal state after:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)
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
⊢ b.repr (↑f i • b i) = b.repr (↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))

Tactic:
map_smul,

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 • b.repr (b i) = b.repr (↑b.repr.symm ((fun i ↦ lp.single 2 i (↑f i)) i))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn ⋯ f n

Tactic:
by
  rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T]
  · congr 1
    refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)
    rw [liftIoc_coe_apply]
    rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx

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

Tactic:
by
        use f.seminormAux k n * ‖c‖
        intro x
        calc
          ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ * ‖c‖ := by
            rw [mul_comm _ ‖c‖, ← mul_assoc]
            exact decay_smul_aux k n f c x
          _ ≤ SchwartzMap.seminormAux k n f * ‖c‖ := by
            gcongr
            apply f.le_seminormAux

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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
this : Tendsto (fun i ↦ ∫ (x : α) in univ, φ i x • g x ∂μ) l (𝓝 a)
⊢ Tendsto (fun i ↦ ∫ (x : α), φ i x • g x ∂μ) l (𝓝 a)

Tactic:
by simpa

Goal state after:
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
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ ∑ i ∈ Finset.range (m.1 + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
gcongr ∑ _i ∈ Finset.range (m.1 + 1), ?_ with i hi

Goal state after:
case h
𝕜 : 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
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ↑(m.1.choose i) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ ∀ᶠ (i : ι) in l, ∀ x ∈ univ, 0 ≤ φ i x

Tactic:
by simpa

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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict univ)

Tactic:
by simpa

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₀ : α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
t : Set α
ht : MeasurableSet t
h'ts : t ∈ 𝓝 x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ
hmg : Integrable g μ
hcg : Tendsto g (𝓝 x₀) (𝓝 a)
⊢ IntegrableOn g univ μ

Tactic:
by simpa

Goal state after:
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✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ - g₂) = smulLeftCLM F g₁ - smulLeftCLM F g₂

Tactic:
by
  ext f x
  simp [hg₁, hg₂, hg₁.sub hg₂, sub_smul]

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

Goal state before:
pp: a : ℂ
ha : a.re < 0
c : ℝ
⊢ 0 < -a.re

Tactic:
by simpa

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

Goal state before:
pp: a : ℂ
ha : 0 < a.re
c : ℝ
⊢ (-a).re < 0

Tactic:
by simpa

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

Goal state before:
pp: a : ℝ
ha : 0 < a
c : ℝ
⊢ -a < 0

Tactic:
by simpa

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

Goal state before:
pp: a c : ℝ
ha : a < -1
hc : 0 < c
⊢ -0 < c

Tactic:
by simpa

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

Goal state before:
pp: p : ℝ × ℝ
⊢ HasFDerivAt (↑polarCoord.symm) (fderivPolarCoordSymm p) p

Tactic:
unfold fderivPolarCoordSymm
  rw [Matrix.toLin_finTwoProd_toContinuousLinearMap]
  convert!
    HasFDerivAt.prodMk (𝕜 := ℝ)
      (hasFDerivAt_fst.mul ((hasDerivAt_cos p.2).comp_hasFDerivAt p hasFDerivAt_snd))
      (hasFDerivAt_fst.mul ((hasDerivAt_sin p.2).comp_hasFDerivAt p hasFDerivAt_snd)) using
    2 <;>
  simp [smul_smul, add_comm, neg_mul, smul_neg, neg_smul _ (ContinuousLinearMap.snd ℝ ℝ ℝ)]

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

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) = |∏ i, (x i).1| • f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
Finset.abs_prod,

Goal state after:
case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) = (∏ x_1, |(x x_1).1|) • f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, ENNReal.ofReal (x i).1) * f fun i ↦ ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |∏ i, (x i).1| * f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
Finset.abs_prod,

Goal state after:
case e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, ENNReal.ofReal (x i).1) * f fun i ↦ ↑polarCoord.symm (x i)) =
    ENNReal.ofReal (∏ x_1, |(x x_1).1|) * f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ |b.im * y| ≤ |b.im| * |c|

Tactic:
rw [abs_mul]

Goal state after:
case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ |b.im| * |y| ≤ |b.im| * |c|
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
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
⊢ 0 < (↑c⁻¹).re

Tactic:
by simpa

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

Goal state before:
pp: s : ℝ
⊢ (starRingEnd ℂ) (Complex.Gamma ↑s) = Complex.Gamma ↑s

Tactic:
← Complex.Gamma_conj,

Goal state after:
s : ℝ
⊢ Complex.Gamma ((starRingEnd ℂ) ↑s) = Complex.Gamma ↑s
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
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ 0 < (↑c⁻¹).re

Tactic:
by simpa

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

Goal state before:
pp: case succ
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
hs' : -↑(n✝ + 1) < s
this : Gamma (s + 1) ≠ 0
⊢ s ≠ 0

Tactic:
· simpa using hs 0

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

Goal state before:
pp: case e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * ↑‖WithLp.toLp 2 v‖ ^ 2) + c * ↑⟪w, WithLp.toLp 2 v⟫ = -b * ∑ i, ↑(v i) ^ 2 + ∑ i, c * ↑(w.ofLp i) * ↑(v i)

Tactic:
simp only [EuclideanSpace.norm_eq, norm_eq_abs, sq_abs, PiLp.inner_apply, RCLike.inner_apply,
    conj_trivial, ofReal_sum, ofReal_mul, Finset.mul_sum, neg_mul, Finset.sum_neg_distrib,
    mul_assoc]

Goal state after:
case e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
v : ι → ℝ
⊢ -(b * ↑√(∑ x, v x ^ 2) ^ 2) + ∑ i, c * (↑(v i) * ↑(w.ofLp i)) = -∑ x, b * ↑(v x) ^ 2 + ∑ x, c * (↑(w.ofLp x) * ↑(v x))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e_f
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))

Tactic:
convert! integral_cexp_quadratic this (c i) 0 using 1

Goal state after:
case e'_2
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x + 0)

case e'_3
ι : Type u_2
inst✝ : Fintype ι
b : ι → ℂ
hb : ∀ (i : ι), 0 < (b i).re
c : ι → ℂ
i : ι
this : (-b i).re < 0
⊢ (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i)) = (↑π / - -b i) ^ (1 / 2) * cexp (0 - c i ^ 2 / (4 * -b i))
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ ((2 * ↑π * Complex.I) •
        (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)))
          ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f))
      x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x

Tactic:
map_smul,

Goal state after:
case e_f
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ inner ℝ x (b i) ^ 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ ((2 * ↑π * Complex.I) •
        (2 * ↑π * Complex.I) •
          (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i)) f))
      x =
    -(2 * π) ^ 2 • ((fourierMultiplierCLM F fun x ↦ inner ℝ x (b i) ^ 2) f) x
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ((2 * ↑π * Complex.I) •
        (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)))
          ((2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) f))
      x =
    (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x

Tactic:
map_smul,

Goal state after:
case e_f
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this : ∀ i ∈ Finset.univ, Function.HasTemperateGrowth fun x ↦ ↑(inner ℝ x (b i)) ^ 2
i : Fin (Module.finrank ℝ E)
x : 𝓢(E, ℂ)
⊢ ((2 * ↑π * Complex.I) •
        (2 * ↑π * Complex.I) •
          (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) ((fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i))) f))
      x =
    (-(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x (b i)) ^ 2) f) x
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    ↑(Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
      (2 ^ volume.integrablePower *
        ((∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) *
          (2 *
            ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E))
              f)))

Tactic:
calc
    _ ≤ ∑ _ ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
        2 ^ integrablePower (volume : Measure V) *
          (∫ x : V, (1 + ‖x‖) ^ (- integrablePower (volume : Measure V) : ℝ)) * 2 *
          (Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
          (schwartzSeminormFamily 𝕜 V E) f := by
      gcongr with p
      apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans
      simp only [mul_assoc, two_mul]
      gcongr
      · have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
      · have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
    _ = _ := by simp [mul_assoc]

Goal state after: