mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : End R M
μ : R
⊢ f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ

Tactic:
rw [hasEigenvalue_iff, eigenspace_def, ← det_eq_zero_iff_ker_ne_bot, det_eq_sign_charpoly_coeff]
  simp [Polynomial.coeff_zero_eq_eval_zero, charpoly_sub_smul]

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

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : hA.eigenvalues = hB.eigenvalues
⊢ A.charpoly = B.charpoly

pp: case mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
⊢ hA.eigenvalues = hB.eigenvalues

Tactic:
· rw [hA.charpoly_eq, hB.charpoly_eq, h]

Goal state after:
case mpr
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
⊢ hA.eigenvalues = hB.eigenvalues
Module: Mathlib.Analysis.Matrix.HermitianFunctionalCalculus

Goal state before:
pp: n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑(star f) ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)) =
    star
      (((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
        (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)))

Tactic:
simp only [star_trivial, ← map_star, star_eq_conjTranspose, diagonal_conjTranspose, Pi.star_def,
      Function.comp_apply, RCLike.star_def, RCLike.conj_ofReal]

Goal state after:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : C(↑(spectrum ℝ A), ℝ)
⊢ ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (diagonal (RCLike.ofReal ∘ ⇑f ∘ fun i ↦ ⟨hA.eigenvalues i, ⋯⟩)) =
    ((conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (diagonal fun i ↦ ↑(f ⟨hA.eigenvalues i, ⋯⟩))
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (CFC.sqrt A ^ 2)⁻¹ = A⁻¹

Tactic:
CFC.sq_sqrt A

Goal state after:
𝕜 : Type u_1
n : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ A⁻¹ = A⁻¹
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosDef
hB : B.PosDef
x : ι →₀ 𝕜
hx : x ≠ 0
hAB : ((A ⊙ B).submatrix Subtype.val Subtype.val).PosDef
⊢ Finsupp.subtypeDomain (fun x_1 ↦ x_1 ∈ x.support) x ≠ 0

Tactic:
simpa [← Finsupp.support_nonempty_iff] using Finsupp.support_nonempty_iff.mpr hx

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖abs a‖ = ‖a‖

Tactic:
← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _),

Goal state after:
A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖abs a‖ ^ 2 = ‖a‖ ^ 2
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
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
⊢ (fun a ↦ ⟪↑↑(indicatorConstLp 2 hs hμs c) a, ↑↑f a⟫) x = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x

Tactic:
have : ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = s.indicator (fun x ↦ ⟪c, f x⟫) x := by
    by_cases hxs : x ∈ s <;> simp [hx, hxs]

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : μ s ≠ ∞
x : α
hx : ↑↑(indicatorConstLp 2 hs hμs c) x = s.indicator (fun x ↦ c) x
this : ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫ = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x
⊢ (fun a ↦ ⟪↑↑(indicatorConstLp 2 hs hμs c) a, ↑↑f a⟫) x = s.indicator (fun x ↦ ⟪c, ↑↑f x⟫) x
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
hdecomp :
  (GeneralSchauderBasis.proj b A) x =
    (GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x
⊢ ‖(GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x‖ ≤
    (Finset.image (fun B ↦ ‖(GeneralSchauderBasis.proj b B) x‖) A₀.powerset).sup' ⋯ _root_.id + 1

Tactic:
have htail : ‖b.proj (A \ A₀) x‖ < 1 := by
    rw [GeneralSchauderBasis.proj_apply]
    exact hA₀ (A \ A₀) Finset.sdiff_disjoint

Goal state after:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace 𝕜 X
β : Type u_3
b : UnconditionalSchauderBasis β 𝕜 X
inst✝ : CompleteSpace X
x : X
A₀ : Finset β
hA₀ : ∀ (t : Finset β), Disjoint t A₀ → ‖∑ i ∈ t, (b.coord i) x • ↑b i‖ < 1
A : Finset β
hdecomp :
  (GeneralSchauderBasis.proj b A) x =
    (GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x
htail : ‖(GeneralSchauderBasis.proj b (A \ A₀)) x‖ < 1
⊢ ‖(GeneralSchauderBasis.proj b (A ∩ A₀)) x + (GeneralSchauderBasis.proj b (A \ A₀)) x‖ ≤
    (Finset.image (fun B ↦ ‖(GeneralSchauderBasis.proj b B) x‖) A₀.powerset).sup' ⋯ _root_.id + 1
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)
| 1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f x =
    1 / (-2 * ↑π * I * ↑n) *
      ((fourier (-n)) ↑a * (f b - f a) - ↑(b - a) * (1 / ↑(b - a) * ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x * f' x))

Tactic:
pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [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)
x : ℝ
| f x * (fourier (-n)) ↑x

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)
| (f b - f a) * (fourier (-n)) ↑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)
x : ℝ
| f' x * (fourier (-n)) ↑x
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hφ
α : 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₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ Integrable (φ i) (μ.restrict (s ∩ u))

pp: case hf
α : 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₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ MemLp g ∞ (μ.restrict (s ∩ u))

Tactic:
· exact IntegrableOn.mono_set I ut

Goal state after:
case hf
α : 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₀ : α
s t : Set α
φ : ι → α → ℝ
a : E
hs : MeasurableSet s
h'st : t ∈ 𝓝[s] x₀
hlφ : ∀ (u : Set α), IsOpen[inst✝³] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun e ↦ ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
u : Set α
u_open : IsOpen[inst✝³] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1
h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1
h''i : AEStronglyMeasurable (φ i) (μ.restrict s)
I : IntegrableOn (φ i) t μ
A : IntegrableOn (fun x ↦ φ i x • g x) (s \ u) μ
⊢ MemLp g ∞ (μ.restrict (s ∩ u))
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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
⊢ (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ f) w) y =
    (fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w) y

Tactic:
suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
    rw [fourierIntegral_continuousLinearMap_apply' hf']
    simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply_apply_apply,
      fourierSMulRight_apply, neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
      smul_neg, ← smul_smul, coe_smul, neg_neg]

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
hf : Integrable f μ
h'f : Differentiable ℝ f
hf' : Integrable (fderiv ℝ f) μ
w : W
y : V
g : V → ℂ := fun v ↦ ↑(𝐞 (-(L v) w))
⊢ ∫ (x : V), g x • (fderiv ℝ f x) y ∂μ = ∫ (x : V), (2 * ↑π * I * ↑((L y) w) * g x) • f x ∂μ
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case inr
α : 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
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
⊢ ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t

Tactic:
refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩

Goal state after:
case inr
α : 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
h : (s \ u).Nonempty
x : α
hx : x ∈ s \ u
h'x : ∀ y ∈ s \ u, c y ≤ c x
⊢ x ≠ 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
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
⊢ ∃ s C,
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (⇑f ∘ g) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 E F)) f

Tactic:
let k' := kg * (k + l * n)

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✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
⊢ ∃ s C,
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (⇑f ∘ g) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 E F)) f
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:

Tactic:
_ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
        rw [← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
          Iic_union_Ioi, restrict_univ]
      _ = 2 * ∫ x in Ioi 0, f x := by
        rw [two_mul, eq]
        congr! 1
        rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
        refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)
        rw [abs_eq_neg_self.mpr (by exact hx)]

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

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ x⁻¹ ≤ x ^ s

Tactic:
rw [← Real.rpow_neg_one x]

Goal state after:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ x ^ (-1) ≤ x ^ s
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ Integrable (fun x ↦ (1 + x ^ 2)⁻¹) volume

Tactic:
suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]

Goal state after:
⊢ Integrable (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-2 / 2)) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ IntegrableOn (fun x ↦ ↑(rexp (-x)) * ↑x ^ (s - 1)) (Ioi 0) volume

Tactic:
by
  constructor
  · refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
    apply continuousOn_of_forall_continuousAt
    intro x hx
    have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x :=
      continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx
    exact ContinuousAt.comp this continuous_ofReal.continuousAt
  · rw [← hasFiniteIntegral_norm_iff]
    refine HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 ?_
    apply (ae_restrict_iff' measurableSet_Ioi).mpr
    filter_upwards with x hx
    rw [norm_mul, Complex.norm_of_nonneg <| le_of_lt <| exp_pos <| -x,
      norm_cpow_eq_rpow_re_of_pos hx _]
    simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
⊢ 𝓕 (iteratedDeriv n f) = fun x ↦ (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
by
  ext x : 1
  have A : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) := by
    intro n hn
    rw [iteratedFDeriv_eq_equiv_comp]
    exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)
  change 𝓕 (fun x ↦ iteratedDeriv n f x) x = _
  simp_rw [iteratedDeriv, ← fourier_continuousMultilinearMap_apply (A n hn),
    fourier_iteratedFDeriv hf A hn]
  simp [← coe_smul, smul_smul, ← mul_pow, innerSL_apply_apply ℝ]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ (∫ (x : ℝ), cexp (-b * ↑x ^ 2)) ^ 2 = ↑π / b

Tactic:
calc
    (∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 =
        ∫ p : ℝ × ℝ, cexp (-b * (p.1 : ℂ) ^ 2) * cexp (-b * (p.2 : ℂ) ^ 2) := by
      rw [pow_two, ← integral_prod_mul]; rfl
    _ = ∫ p : ℝ × ℝ, cexp (-b * ((p.1 : ℂ) ^ 2 + (p.2 : ℂ) ^ 2)) := by
      congr
      ext1 p
      rw [← Complex.exp_add, mul_add]
    _ = ∫ p in polarCoord.target, p.1 •
        cexp (-b * ((p.1 * Complex.cos p.2) ^ 2 + (p.1 * Complex.sin p.2) ^ 2)) := by
      rw [← integral_comp_polarCoord_symm]
      simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]
    _ = (∫ r in Ioi (0 : ℝ), r * cexp (-b * (r : ℂ) ^ 2)) * ∫ θ in Ioo (-π) π, 1 := by
      rw [← setIntegral_prod_mul]
      congr with p : 1
      rw [mul_one]
      congr
      conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
      ring
    _ = ↑π / b := by
      simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply,
        univ_inter, real_smul, mul_one, integral_mul_cexp_neg_mul_sq hb]
      rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]
      simp
      ring

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

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux n s = GammaAux (n + 1) s

Tactic:
by
  rcases n with - | n
  · simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]
    rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]
    rintro rfl
    rw [zero_re] at h1
    exact h1.false
  · dsimp only [GammaAux]
    have : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1) := by
      have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
      rw [GammaAux_recurrence1 (s + 1) n hh1]
    rw [this]

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

Goal state before:
pp: s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
rw [setIntegral_pos_iff_support_of_nonneg_ae]

Goal state after:
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < volume ((Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0)

case hf
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 ≤ᵐ[volume.restrict (Ioi 0)] fun x ↦ rexp (-x) * x ^ (s - 1)

case hfi
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ 𝓕⁻ (fun y ↦ 𝓕 (⇑f ⋆[B, volume] ⇑g) y) x = (⇑f ⋆[B, volume] ⇑g) x

Tactic:
rw [Continuous.fourierInv_fourier_eq]
    · refine BddAbove.continuous_convolution_right_of_integrable B ?_ f.integrable g.continuous
      exact ⟨SchwartzMap.seminorm ℝ 0 0 g, fun x ⟨y, hy⟩ ↦ hy ▸ norm_le_seminorm ℝ g y⟩
    · exact f.integrable.integrable_convolution B g.integrable
    · have : Integrable (fun ξ ↦ B (𝓕 f ξ) (𝓕 g ξ)) volume := (pairing B (𝓕 f) (𝓕 g)).integrable
      convert! this
      rw [← fourier_convolution_apply B f g, fourier_convolution, pairing_apply_apply]

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: p : ℕ+
pp : p.Prime
contra : p = 1
⊢ False

Tactic:
apply Nat.Prime.ne_one pp

Goal state after:
p : ℕ+
pp : p.Prime
contra : p = 1
⊢ ↑p = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
⊢ IsPrimitiveRoot 1 1

Tactic:
exact one

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case right
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
⊢ degree 0 < B.degree

Tactic:
simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero

Goal state after: