mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := ⋯
hw₃1 : ∑ k, w₃ k = 1
hw₃i : w₃ i = 0
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

Tactic:
rcases h0.lt_or_gt with h | h

Goal state after:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
hw₃1 : ∑ k, w₃ k = 1
hw₃i : w₃ i = 0
h : w₁ i < 0
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹

case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
hs : SignType.sign (w₁ i) = SignType.sign (w₂ i)
h0 : w₁ i ≠ 0
h0' : w₂ i ≠ 0
j : Fin (n + 1)
hj : j ≠ i
hj' : s.points j ∈ affineSpan R (Set.range (s.faceOpposite i).points)
w₃ : Fin (n + 1) → R := w₂ - w₂ i • (w₁ i)⁻¹ • (w₁ - Pi.single j 1)
hw₃1 : ∑ k, w₃ k = 1
hw₃i : w₃ i = 0
h : 0 < w₁ i
⊢ 0 ≤ w₂ i * (w₁ i)⁻¹
Module: Mathlib.Analysis.Convex.Side

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁶ : Field R
inst✝⁵ : LinearOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex R P n
w₁ w₂ : Fin (n + 1) → R
hw₁ : ∑ j, w₁ j = 1
hw₂ : ∑ j, w₂ j = 1
i : Fin (n + 1)
⊢ (affineSpan R (Set.range (s.faceOpposite i).points)).WSameSide ((Finset.affineCombination R Finset.univ s.points) w₁)
      ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
    SignType.sign (w₁ i) = SignType.sign (w₂ i) ∨ w₁ i = 0 ∨ w₂ i = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · by_cases h0 : w₁ i = 0
    · simp [h0]
    by_cases h0' : w₂ i = 0
    · simp [h0']
    exact .inl ((s.sSameSide_affineSpan_faceOpposite_iff hw₁ hw₂).1 ⟨h,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).not.2 h0,
      (s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).not.2 h0'⟩).1
  · by_cases h0 : w₁ i = 0
    · exact wSameSide_of_left_mem _ ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₁).2 h0)
    · by_cases h0' : w₂ i = 0
      · exact wSameSide_of_right_mem _
          ((s.affineCombination_mem_affineSpan_faceOpposite_iff hw₂).2 h0')
      simp only [h0, h0', or_self, or_false] at h
      exact (s.sSameSide_affineSpan_faceOpposite_of_sign_eq hw₁ hw₂ h h0).wSameSide

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

Goal state before:
pp: case insert
ι : Type u_1
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → F
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x ↦ ∑ i ∈ s, f i x
hf : ∀ i ∈ insert a s, HasTemperateGrowth (f i)
⊢ HasTemperateGrowth fun x ↦ ∑ i ∈ insert a s, f i x

Tactic:
obtain ⟨hf, h⟩ := by simpa using! hf

Goal state after:
case insert
ι : Type u_1
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ι → E → F
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, HasTemperateGrowth (f i)) → HasTemperateGrowth fun x ↦ ∑ i ∈ s, f i x
hf✝ : ∀ i ∈ insert a s, HasTemperateGrowth (f i)
hf : HasTemperateGrowth (f a)
h : ∀ a ∈ s, HasTemperateGrowth (f a)
⊢ HasTemperateGrowth fun x ↦ ∑ i ∈ insert a s, f i x
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: case hf
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Differentiable ℝ _root_.id

pp: case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : E), ‖_root_.id x‖ ≤ 1 * (1 + ‖x‖) ^ 1

Tactic:
· apply differentiable_id

Goal state after:
case h
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : E), ‖_root_.id x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Module: Mathlib.Analysis.Distribution.TemperateGrowth

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ∞
x : E
⊢ ‖(1 + ‖x‖) ^ (-↑k * ↑p)‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p

Tactic:
Real.rpow_mul (h_one_add x).le

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x ↦ (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ∞
x : E
⊢ ‖((1 + ‖x‖) ^ (-↑k)) ^ ↑p‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p
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 : ℕ∞
K : Compacts E
i : ℕ
f : 𝓓^{n}_{K}(E, F)
⊢ ⇑((iteratedFDerivLM 𝕜 n k i) f) = if k + ↑i ≤ n then iteratedFDeriv ℝ i ⇑f else 0

Tactic:
rw [ContDiffMapSupportedIn.iteratedFDerivLM]
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝ : RCLike 𝕜
A B : Matrix n n 𝕜
h₁ : A ≤ B
h₂ : B ≤ A
⊢ (-(B - A)).PosSemidef

Tactic:
simpa only [← neg_sub B, le_iff] using h₂

Goal state after:
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
i : ℕ
hin : n < ↑i
⊢ ContDiffMapSupportedIn.seminorm 𝕜 E F n K i = ⊥

Tactic:
by
  have : ¬(i ≤ n) := by simpa using hin
  ext f
  simp [ContDiffMapSupportedIn.seminorm_apply, BoundedContinuousFunction.ext_iff,
    structureMapCLM_apply, this]

Goal state after:
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 g : ↥(Lp E 2 μ)
x : α
⊢ ‖⟪↑↑f x, ↑↑g x⟫‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖

Tactic:
calc
      ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
      _ ≤ 2 * ‖f x‖ * ‖g x‖ := by
        gcongr
        exact le_mul_of_one_le_left (norm_nonneg _) one_le_two
      -- TODO(kmill): the type ascription is getting around an elaboration error
      _ ≤ ‖(‖f x‖ ^ 2 + ‖g x‖ ^ 2 : ℝ)‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)

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₂
f g : 𝓓^{n}_{K}(E, F₁)
hφ : IntegrableOn φ (↑K) μ
⊢ ∫ (x : E), (B ((f + g) x)) (φ x) ∂μ = ∫ (x : E), (B (f x)) (φ x) ∂μ + ∫ (x : E), (B (g x)) (φ x) ∂μ

Tactic:
simp_rw [add_apply, map_add, add_apply,
        integral_add (f.integrable_bilin B hφ) (g.integrable_bilin B hφ)]

Goal state after:
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₂ : Fact (1 ≤ p)
⊢ Dense {f | ∃ g, ↑↑f =ᵐ[μ] g ∧ HasCompactSupport g ∧ ContDiff ℝ ∞ g}

Tactic:
intro f
  refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
  obtain ⟨g, hg₁, hg₂, hg₃⟩ := exist_eLpNorm_sub_le hp hp₂.out (Lp.memLp f) hε
  have hg₄ : MemLp g p μ := hg₂.continuous.memLp_of_hasCompactSupport hg₁
  use hg₄.toLp
  use ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩
  rw [Metric.mem_closedBall, dist_comm, Lp.dist_def,
    ← le_ofReal_iff_toReal_le ((Lp.memLp f).sub (Lp.memLp hg₄.toLp)).eLpNorm_ne_top hε.le]
  convert! hg₃ using 1
  apply eLpNorm_congr_ae
  gcongr
  exact hg₄.coeFn_toLp

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

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑((n • x).toCircle * toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x

Tactic:
Metric.unitSphere.coe_mul

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • x).toCircle * ↑(toCircle ↑(n • (T / 2 / ↑n))) = -(fourier n) x
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:
fourierBasis.repr_apply_apply f i,

Goal state after:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
i : ℤ
⊢ inner ℂ (fourierBasis i) f = ∫ (t : AddCircle T), (starRingEnd ℂ) (↑↑(fourierLp 2 i) t) * ↑↑f t ∂haarAddCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ (fourier n) ↑y) (2 * ↑π * I * ↑n / ↑T * (fourier n) ↑x) x

Tactic:
simp_rw [fourier_coe_apply]

Goal state after:
T : ℝ
n : ℤ
x : ℝ
⊢ HasDerivAt (fun y ↦ cexp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) x
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
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f - ⇑g) x‖ ≤
    @SchwartzMap.seminormAux E F inst✝³ inst✝² inst✝¹ inst✝ k n f +
      @SchwartzMap.seminormAux E F inst✝³ inst✝² inst✝¹ inst✝ k n g

Tactic:
← f.le_seminormAux k n x,

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
f g : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f - ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + @SchwartzMap.seminormAux E F inst✝³ inst✝² inst✝¹ inst✝ k n g
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
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
n : ℕ
⊢ ∫ (x : α) in s, φ n x ∂μ = 1

Tactic:
rw [integral_const_mul, inv_mul_cancel₀ (P n).ne']

Goal state after:
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
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
⊢ φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n

Tactic:
have B : t' ^ n * μ.real (v ∩ s) ≤ ∫ y in s, c y ^ n ∂μ :=
        calc
          t' ^ n * μ.real (v ∩ s) = ∫ _ in v ∩ s, t' ^ n ∂μ := by simp [mul_comm]
          _ ≤ ∫ y in v ∩ s, c y ^ n ∂μ := by
            apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
            · refine integrableOn_const (C := t' ^ n) ?_
              exact (lt_of_le_of_lt (measure_mono inter_subset_right) hs.measure_lt_top).ne
            · exact (I n).mono inter_subset_right le_rfl
            · intro x hx
              exact pow_le_pow_left₀ t'_pos.le (hv hx).le _
          _ ≤ ∫ y in s, c y ^ n ∂μ :=
            setIntegral_mono_set (I n) (J n) (Eventually.of_forall inter_subset_right)

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
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
n : ℕ
x : α
hx : x ∈ s \ u
B : t' ^ n * μ.real (v ∩ s) ≤ ∫ (y : α) in s, c y ^ n ∂μ
⊢ φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
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
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x ↦ g (x₀ - x)
If : Integrable f μ
⊢ ContinuousAt g (x₀ - 0)

Tactic:
simpa using h'g

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
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
v : V
w : W
⊢ |(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w‖ ≤
    (2 * π) ^ n * (|(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w‖)

Tactic:
by
    apply le_mul_of_one_le_left (by positivity)
    apply one_le_pow₀
    linarith [one_le_pi_div_two]

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

Goal state before:
pp: a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun t ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))

Tactic:
apply Tendsto.div_const

Goal state after:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun a_1 ↦ a_1 ^ (a + 1)) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.ExpDecay

Goal state before:
pp: a b : ℝ
h : 0 < b
this : Tendsto (fun x ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x ↦ rexp (-b * x)) (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonneg' (fun x _ => ?_) (fun x _ => (exp_pos _).le) this

Goal state after:
a b : ℝ
h : 0 < b
this : Tendsto (fun x ↦ -rexp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x ↦ -rexp (-b * x) / b) (rexp (-b * x)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
⊢ Gamma s = 0 → ∃ m, s = -↑m

Tactic:
contrapose!; exact Gamma_ne_zero

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

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
⊢ Integrable (fun v ↦ cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫)) volume

Tactic:
let e := (stdOrthonormalBasis ℝ V).repr.symm

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ Integrable (fun v ↦ cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫)) volume
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
simp_rw [← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, Complex.exp_sum, ← neg_mul]
  rw [integral_fintype_prod_volume_eq_prod (f := fun i (v : ℝ) ↦ cexp (-b i * v ^ 2 + c i * v))]
  congr with i
  have : (-b i).re < 0 := by simpa using hb i
  convert! integral_cexp_quadratic this (c i) 0 using 1 <;> simp [div_neg]

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

Goal state before:
pp: b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ), cexp (-(b * ↑‖WithLp.toLp 2 x‖ ^ 2) + c * ↑⟪w, WithLp.toLp 2 x⟫) ∂volume =
    (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
convert! integral_cexp_neg_mul_sum_add hb (fun i ↦ c * w i) using 5 with _x y

Goal state after:
case e'_2.e'_7.e'_5
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ -(b * ↑‖WithLp.toLp 2 y‖ ^ 2) = -b * ∑ i, ↑(y i) ^ 2

case e'_2.e'_7.e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ c * ↑⟪w, WithLp.toLp 2 y⟫ = ∑ i, c * ↑(w.ofLp i) * ↑(y i)

case e'_3
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
⊢ c ^ 2 * ↑‖w‖ ^ 2 = ∑ i, (c * ↑(w.ofLp i)) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
let e := (stdOrthonormalBasis ℝ V).repr.symm

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
⊢ ∀ (x : V), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑(𝓕 f)) x‖ ≤ ‖f.toLp 1 volume‖

Tactic:
by simpa using norm_fourier_apply_le_toLp_one f

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

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
x : α
⊢ x ∈ dsupport f ↔ ∀ (s : Set α), x ∈ s → IsOpen[inst✝²] s → ¬IsVanishingOn f s

Tactic:
by
  grind only [notMem_dsupport_iff]

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ {x}ᶜ
⊢ (TemperedDistribution.delta x) u = 0

Tactic:
rw [Set.subset_compl_singleton_iff] at hu

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
u : 𝓢(E, ℂ)
hu : x ∉ tsupport ⇑u
⊢ (TemperedDistribution.delta x) u = 0
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_11
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
u : 𝓓^{n}(Ω, ℝ)
hu : tsupport ⇑u ⊆ {x}ᶜ
⊢ (delta x) u = 0

Tactic:
rw [Set.subset_compl_singleton_iff] at hu

Goal state after:
E : Type u_11
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
x : E
u : 𝓓^{n}(Ω, ℝ)
hu : x ∉ tsupport ⇑u
⊢ (delta x) u = 0