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
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ 0 ≤ c.sum fun i xi ↦ c.sum fun j xj ↦ star xi * (‖f‖ ^ 2 • gram 𝕜 v - gram 𝕜 (⇑f ∘ v)) i j * xj

Tactic:
simp_rw [Finsupp.sum, Matrix.sub_apply, Matrix.smul_apply, mul_sub, sub_mul,
    Finset.sum_sub_distrib, sub_nonneg]

Goal state after:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ∑ x ∈ c.support, ∑ x_1 ∈ c.support, star (c x) * gram 𝕜 (⇑f ∘ v) x x_1 * c x_1 ≤
    ∑ x ∈ c.support, ∑ x_1 ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x x_1 * c x_1
Module: Mathlib.Analysis.InnerProductSpace.GramMatrix

Goal state before:

Tactic:
∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * gram 𝕜 (f ∘ v) x y * c y
    _ = (‖f (∑ x ∈ c.support, c x • v x)‖ : 𝕜) ^ 2 := ?h1
    _ ≤ ‖f‖ ^ 2 • (‖∑ i ∈ c.support, c i • v i‖ : 𝕜) ^ 2 := by
      norm_cast
      grw [f.le_opNorm _, smul_eq_mul, ← mul_pow]
    _ = ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y := ?h2

Goal state after:
case h1
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * gram 𝕜 (⇑f ∘ v) x y * c y = ↑‖f (∑ x ∈ c.support, c x • v x)‖ ^ 2

case h2
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
v : n → E
f : E →L[𝕜] F
c : n →₀ 𝕜
⊢ ‖f‖ ^ 2 • ↑‖∑ i ∈ c.support, c i • v i‖ ^ 2 =
    ∑ x ∈ c.support, ∑ y ∈ c.support, star (c x) * ‖f‖ ^ 2 • gram 𝕜 v x y * c y
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 : ℕ∞
K : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
⊢ (ContDiffMapSupportedIn.seminorm ℝ E F' n K i) ((postcompLM T') f) ≤
    ‖T'‖ * (ContDiffMapSupportedIn.seminorm ℝ E F n K i) f

Tactic:
ContDiffMapSupportedIn.seminorm_le_iff ℝ (by positivity)

Goal state after:
𝕜 : 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 : ℕ∞
K : Compacts E
inst✝ : LinearMap.CompatibleSMul F F' ℝ 𝕜
i : ℕ
T : F →L[𝕜] F'
f : 𝓓^{n}_{K}(E, F)
T' : F →L[ℝ] F' := ContinuousLinearMap.restrictScalars ℝ T
⊢ ↑i ≤ n →
    ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑((postcompLM T') f)) x‖ ≤ ‖T'‖ * (ContDiffMapSupportedIn.seminorm ℝ E F n K i) f
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
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y

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

Tactic:
· refine ⟨U, mem_nhdsSet_iff_forall.mp hU x hx, ?_⟩
    exact ⟨f, hfU, fun y _ ↦ ⟨dist_f_f y, fun _ ↦ rfl, id⟩⟩

Goal state after:
case neg
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
⊢ ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) (↑n) g U ∧ ∀ y ∈ U, g y ∈ t y
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
K : Compacts E
i : ℕ
f : 𝓓_{K}(E, F)
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) ⊤ K i) ((fderivLM 𝕜 ⊤ ⊤) f) =
    (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K (i + 1)) f

Tactic:
by
  simp [ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.norm_eq_iSup_norm,
    norm_iteratedFDeriv_fderiv]

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
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:
simp_rw [smul_apply, map_smul, smul_apply, integral_smul c, RingHom.id_apply]

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ ⨆ i, bif i then K else Kᗮ

Tactic:
iSup_bool_eq,

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)
⊢ ⊤ ≤ (bif true then K else Kᗮ) ⊔ bif false then K else Kᗮ
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
n : ℤ
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x = fourierCoeffOn hab g n

Tactic:
fourierCoeffOn_eq_integral

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
hab : a < b
f g : ℝ → E
h : f =ᵐ[volume.restrict (Ioc a b)] g
n : ℤ
⊢ (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x =
    (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • g x
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) * ((f b - f a) * (↑(b - a) * (1 / (-2 * ↑π * I * ↑n)) * (fourier (-n)) ↑a)) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a)

Tactic:
conv_lhs => rw [mul_comm, mul_div, mul_one]

Goal state after:
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) / ↑(b - a) =
    1 / (-2 * ↑π * I * ↑n) * ((f b - f a) * (fourier (-n)) ↑a)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h
ι : 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‖ ≤ @SchwartzMap.seminormAux E F inst✝⁹ inst✝⁸ inst✝⁷ inst✝⁶ k n f * ‖c‖

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

Tactic:
rw [← Nat.sum_range_choose m.1]

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
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose 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✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ ContinuousSMul 𝕜 𝓢(E, F)

Tactic:
(schwartz_withSeminorms 𝕜 E F).withSeminorms_eq

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
⊢ ContinuousSMul 𝕜 𝓢(E, F)
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₂
f : 𝓢(E, F)
⊢ (smulLeftCLM F g₁) ((smulLeftCLM F g₂) f) = (smulLeftCLM F (g₁ * g₂)) f

Tactic:
by
  ext x
  simp [smul_smul, hg₁, hg₂, hg₁.mul hg₂]

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✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
⊢ ∃ k C,
    ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
by
  -- Apply Hölder's inequality `‖f‖_p ≤ ‖f₁‖_p * ‖f₂‖_∞` to obtain the `L^p` norm of `f = f₁ • f₂`
  -- using `f₁ = (1 + ‖x‖) ^ (-k)` and `f₂ = (1 + ‖x‖) ^ k • f x`.
  rcases hμ.exists_eLpNorm_lt_top p with ⟨k, hk⟩
  refine ⟨k, (eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ).toNNReal * 2 ^ k, fun f ↦ ?_⟩
  have h_one_add (x : E) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)
  calc eLpNorm (⇑f) p μ
  _ = eLpNorm ((fun x : E ↦ (1 + ‖x‖) ^ (-k : ℝ)) • fun x ↦ (1 + ‖x‖) ^ k • f x) p μ := by
    refine congrArg (eLpNorm · p μ) (funext fun x ↦ ?_)
    simp [(h_one_add x).ne']
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ * eLpNorm (fun x ↦ (1 + ‖x‖) ^ k • f x) ⊤ μ := by
    refine eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top p _ ?_
    refine Continuous.aestronglyMeasurable ?_
    exact .rpow_const (by fun_prop) fun x ↦ .inl (h_one_add x).ne'
  _ ≤ eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ *
      (2 ^ k * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)) := by
    gcongr
    refine eLpNormEssSup_le_of_ae_nnnorm_bound (ae_of_all μ fun x ↦ ?_)
    rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]
    simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using!
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x
  _ = _ := by
    rw [ENNReal.coe_mul, ENNReal.coe_toNNReal hk.ne]
    simp only [ENNReal.coe_pow, ENNReal.coe_ofNat]
    ring

Goal state after:
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
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily ℝ E F)) f)
⊢ eLpNorm (⇑f) p μ < ∞

Tactic:
exact lt_of_le_of_lt (hC f) (ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top)

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

Goal state before:
pp: case h
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
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
⊢ ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) v‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖v‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f v‖

Tactic:
apply norm_iteratedFDeriv_fourierPowSMulRight _ hf (mod_cast hn) _

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
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
⊢ ∀ i ≤ n,
    ∀ j ≤ k,
      ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖v‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f v‖
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x

Tactic:
have : ¬ Integrable (fun x => f |x|) := by
      contrapose hf
      exact hf.integrableOn

Goal state after:
case neg
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : ¬IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
this : ¬Integrable (fun x ↦ f |x|) volume
⊢ ∫ (x : ℝ), f |x| = 2 * ∫ (x : ℝ) in Ioi 0, f x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ p)) (Ioi 0) volume

Tactic:
rw [show 0 = b ^ (-p⁻¹) * 0 by rw [mul_zero], ← integrableOn_Ioi_comp_mul_left_iff _ _ hib]

Goal state after:
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
this : IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume
⊢ IntegrableOn (fun x ↦ (b ^ (-p⁻¹) * x) ^ s * rexp (-b * (b ^ (-p⁻¹) * x) ^ p)) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * ↑(volume.real (Ioo (-π) π)) = ↑π / b

Tactic:
rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * ↑(π - -π) = ↑π / b
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫⁻ (p : ι → ℝ × ℝ), f p

Tactic:
← setLIntegral_univ f,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
⊢ (∫⁻ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target,
      (∏ i, ENNReal.ofReal (p i).1) * f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫⁻ (x : ι → ℝ × ℝ) in Set.univ, f x
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
⊢ ContinuousOn (fun {b} ↦ ∫ (x : ℝ), cexp (-b * ↑x ^ 2)) {c | 0 < c.re}

Tactic:
exact continuousOn_of_forall_continuousAt continuousAt_gaussian_integral

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

Goal state before:
pp: case pos
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.succ

Tactic:
exact_mod_cast lt_of_le_of_lt (Nat.floor_le h) (by linarith : 1 - s.re < n + 1)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
x : V →ᵇ ℂ
hx : x ∈ (charAlgHom he hL).range
⊢ star x ∈ (charAlgHom he hL).range

Tactic:
by
  simp only [AlgHom.mem_range] at hx ⊢
  obtain ⟨y, rfl⟩ := hx
  let z := y.map (starRingEnd _).toAddMonoidHom
  let f : W ↪ W := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩
  refine ⟨.ofCoeff <| z.coeff.embDomain f, ?_⟩
  ext
  simp [charAlgHom_apply, Finsupp.sum_embDomain, z, Finsupp.sum_mapRange_index, f]

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
hψ : ψ 0 ≠ 1
⊢ False

Tactic:
exact hψ ψ.map_zero_eq_one

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ (2 * n.natAbs).Coprime q.den

Tactic:
convert! q.reduced

Goal state after:
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ 2 * n.natAbs = q.num.natAbs
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → k ∣ l

Tactic:
by
    rw [h.eq_orderOf]
    intro l hl
    rw [← map_pow, ← map_one f] at hl
    exact orderOf_dvd_of_pow_eq_one (hf hl)

Goal state after: