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
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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
⊢ (if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0) =
    (RingHom.id 𝕜) c • if h : n₂ ≤ n₁ ∧ K₁ ≤ K₂ then ContDiffMapSupportedIn.of_support_subset ⋯ ⋯ else 0

Tactic:
split_ifs <;> ext

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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h✝ : n₂ ≤ n₁ ∧ K₁ ≤ K₂
a✝ : E
⊢ (ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) a✝ =
    ((RingHom.id 𝕜) c • ContDiffMapSupportedIn.of_support_subset ⋯ ⋯) a✝

case neg
𝕜 : 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
c : 𝕜
f : 𝓓^{n₁}_{K₁}(E, F)
h✝ : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
a✝ : E
⊢ 0 a✝ = ((RingHom.id 𝕜) c • 0) a✝
Module: Mathlib.Analysis.InnerProductSpace.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
⊢ (w.ofLp a * ↑(hT.eigenvalues hn a)) • (hT.eigenvectorBasis hn) a =
    (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a

Tactic:
mul_comm,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hT : T.IsSymmetric
hn : finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
⊢ (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a =
    (↑(hT.eigenvalues hn a) * w.ofLp a) • (hT.eigenvectorBasis hn) a
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:
pp: E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ x_1, star x x_1 * ∑ x, gram 𝕜 v x_1 x * y x = ∑ x_1, (starRingEnd 𝕜) (x x_1) * ∑ i, y i * ⟪v x_1, v i⟫_𝕜

Tactic:
mul_comm,

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype n
v : n → E
x y : n → 𝕜
⊢ ∑ x_1, (∑ x, y x * gram 𝕜 v x_1 x) * star x x_1 = ∑ x_1, (∑ i, y i * ⟪v x_1, v i⟫_𝕜) * (starRingEnd 𝕜) (x x_1)
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (↑↑f) (1 * ENNReal.ofReal 2) μ ^ 2 < ∞

Tactic:
one_mul,

Goal state after:
α : Type u_1
F : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (↑↑f) (ENNReal.ofReal 2) μ ^ 2 < ∞
Module: Mathlib.Geometry.Manifold.SmoothApprox

Goal state before:
pp: case pos
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
⊢ ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

Tactic:
exact ⟨f, hfU, fun y _ ↦ ⟨dist_f_f y, fun _ ↦ rfl, id⟩⟩

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

Goal state before:
pp: case pos
𝕜 : 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ ↑i ≤ n₂ → ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
intro hik

Goal state after:
case pos
𝕜 : 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₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
hik : ↑i ≤ n₂
⊢ ∀ x ∈ K₂, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
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₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
x : E
⊢ ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f * ‖φ x‖ ≤
    ‖φ x‖ * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f

Tactic:
mul_comm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
n : ℕ∞
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₂
f : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
x : E
⊢ ‖φ x‖ * (‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f) ≤
    ‖φ x‖ * ‖B‖ * (ContDiffMapSupportedIn.seminorm 𝕜 E F₁ n K 0) f
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
i j : ℕ
x : X
h : ¬i = j
h' : i < j
⊢ (P (min i j + 1)) x - (P (min i (j + 1))) x - ((P (min (i + 1) j)) x - (P (min i j)) x) = 0

Tactic:
rw [min_eq_left_of_lt h', min_eq_left (Nat.succ_le_of_lt h'),
        min_eq_left_of_lt (Nat.lt_succ_of_lt h')]
      abel

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✝ hV : OrthogonalFamily 𝕜 G V
f : ↥(lp G 2)
H : 0 < ENNReal.toReal 2
this : ‖∑' (i : ι), (V i) (↑f i)‖ ^ ENNReal.toReal 2 = ‖f‖ ^ ENNReal.toReal 2
⊢ ‖{ toFun := fun f ↦ ∑' (i : ι), (V i) (↑f i), map_add' := ⋯, map_smul' := ⋯ } f‖ = ‖f‖

Tactic:
exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this

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

Goal state before:
pp: case empty
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
hf : ∀ i ∈ ∅, Integrable (f i) haarAddCircle
⊢ fourierCoeff (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, fourierCoeff (f i)

Tactic:
ext; simp [fourierCoeff]

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
c : ℂ
n : ℤ
⊢ ∫ (t : AddCircle T), ((fourier (-n)) t * c) • f t ∂haarAddCircle =
    c • ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂haarAddCircle

Tactic:
mul_comm,

Goal state after:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
c : ℂ
n : ℤ
⊢ ∫ (t : AddCircle T), (c * (fourier (-n)) t) • f t ∂haarAddCircle =
    c • ∫ (t : AddCircle T), (fourier (-n)) t • f t ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle

Tactic:
rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]
    simp only [RCLike.inner_apply']

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ ↑(fourierBasis.repr f) i = fourierCoeff (↑↑f) i

Tactic:
by
  trans ∫ t : AddCircle T, conj ((@fourierLp T hT 2 _ i : AddCircle T → ℂ) t) * f t ∂haarAddCircle
  · rw [fourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_fourierBasis]
    simp only [RCLike.inner_apply']
  · apply integral_congr_ae
    filter_upwards [coeFn_fourierLp 2 i] with _ ht
    rw [ht, ← fourier_neg, smul_eq_mul]

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)
s2 : ↑b = ↑a
| 1 / ↑(b - a) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a))

Tactic:
mul_comm,

Goal state after:
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 / ↑(b - a))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
x : ℝ
hx : 1 ≤ x
⊢ ‖x ^ (-↑k)‖ ≤ 1 * ‖x ^ s‖

Tactic:
one_mul,

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
x : ℝ
hx : 1 ≤ x
⊢ ‖x ^ (-↑k)‖ ≤ ‖x ^ s‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
have := le_seminorm 𝕜 k n f x

Goal state after:
𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
⊢ |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f
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
n : ℕ
⊢ 0 < ∫ (x : α) in s, c x ^ n ∂μ

Tactic:
refine (setIntegral_pos_iff_support_of_nonneg_ae (J n) (I n)).2 ?_

Goal state after:
α : 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
n : ℕ
⊢ 0 < μ ((Function.support fun x ↦ c x ^ n) ∩ s)
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 : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ ∑ k ∈ Finset.range n,
      ↑((n + 1).choose (k + 1 + 1)) * ‖iteratedFDeriv ℝ (k + 1 + 1) (⇑L) x‖ *
        ‖iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f) x‖ =
    0

Tactic:
apply Finset.sum_eq_zero

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[ℝ] ℝ
k : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ ∀ x_1 ∈ Finset.range n,
    ↑((n + 1).choose (x_1 + 1 + 1)) * ‖iteratedFDeriv ℝ (x_1 + 1 + 1) (⇑L) x‖ *
        ‖iteratedFDeriv ℝ (n + 1 - (x_1 + 1 + 1)) (⇑f) x‖ =
      0
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
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 ∈ Finset.range (k + 1), ↑(k.choose i) * ↑(n + 1) ^ k * ‖L‖ ^ n * C = (2 * ↑n + 2) ^ k * (‖L‖ ^ n * C)

Tactic:
by
    simp only [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose, mul_one, ← mul_assoc,
      Nat.cast_pow, Nat.cast_ofNat, Nat.cast_add, Nat.cast_one, ← mul_pow, mul_add]

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
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f : V → E
w : W
⊢ Integrable (fun v ↦ e (-(L v) w) • f v) μ ↔ Integrable f μ

Tactic:
have aux {g : V → E} (hg : Integrable g μ) (x : W) :
      Integrable (fun v : V ↦ e (-L v x) • g v) μ := by
    have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
    simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.fun_smul hg.1), Circle.norm_smul]
    exact hg.norm
  -- then use it for both directions
  refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩
  have := aux hf (-w)
  simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_eq_mul, map_neg, neg_add_cancel,
    e.map_zero_eq_one, one_smul] at this -- the `(e _)` speeds up elaboration considerably
  exact this

Goal state after:
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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
⊢ c ^ finrank ℝ F * φ (c • x) < ε

Tactic:
have hδx : δ ≤ ‖x‖ := by
      have : x ∈ (ball 0 δ)ᶜ := fun h ↦ hx (h'u h)
      simpa only [mem_compl_iff, mem_ball, dist_zero_right, not_lt]

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 φ μ
u : Set F
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hu : 0 ∈ u
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
h'u : ball 0 δ ⊆ u
M : ℝ
Mpos : M > 0
hM : ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε
c : ℝ
hc : M / δ < c
x : F
hx : x ∈ uᶜ
cpos : 0 < c
hδx : δ ≤ ‖x‖
⊢ c ^ finrank ℝ F * φ (c • x) < ε
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
← integral_Ici_eq_integral_Ioi,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ici (-c), f x
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ ‖{ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖

Tactic:
one_mul,

Goal state after:
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ ‖{ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ ‖f‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
v : ℝ
⊢ (1 * v) • f v = (↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (v • f v)) 1

Tactic:
one_mul,

Goal state after:
case e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
hf'' : Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := (ContinuousLinearMap.mul ℝ ℝ).flip
v : ℝ
⊢ v • f v = (↑↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) (v • f v)) 1