mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t ↦ ‖↑t ^ a‖) (Ioi c) volume

Tactic:
refine (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => ?_) measurableSet_Ioi
  rw [Complex.norm_cpow_eq_rpow_re_of_pos (hc.trans hx)]

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

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ (fun x ↦ rexp (-b * x ^ 2)) =o[atTop] fun x ↦ rexp (-x)

Tactic:
simp_rw [← rpow_two]
  exact exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

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

Goal state before:
pp: s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x ↦ x ^ s * rexp (-b * x ^ p)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)

Tactic:
apply ((isBigO_refl (fun x : ℝ => x ^ s) atTop).mul_isLittleO
      (exp_neg_mul_rpow_isLittleO_exp_neg hb hp)).trans

Goal state after:
s b p : ℝ
hp : 1 < p
hb : 0 < b
⊢ (fun x ↦ x ^ s * rexp (-x)) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
x : ℝ
⊢ rexp (x ^ 2 * -b.re) = rexp (-b.re * x ^ 2)

Tactic:
mul_comm

Goal state after:
b : ℂ
x : ℝ
⊢ rexp (-b.re * x ^ 2) = rexp (-b.re * x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ × ℝ → E
⊢ ∫ (p : ℝ × ℝ) in polarCoord.source, f p = ∫ (p : ℝ × ℝ) in polarCoord.target, |p.1| • f (↑polarCoord.symm p)

Tactic:
rw [← OpenPartialHomeomorph.symm_target,
      integral_target_eq_integral_abs_det_fderiv_smul volume
      (fun p _ ↦ hasFDerivAt_polarCoord_symm p), OpenPartialHomeomorph.symm_source]
      simp_rw [det_fderivPolarCoordSymm]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E j.succ)),
      f 0 (Fin.cons x.1 (fun j ↦ x.2 j) 0) * ∏ x_1, f x_1.succ (x.2 x_1) ∂(μ 0).prod (Measure.pi fun j ↦ μ j.succ) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun j ↦ μ j.succ)

Tactic:
Fin.cons_zero

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)

Tactic:
refine eventually_of_mem ((continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds hd') ?_

Goal state after:
b : ℂ
hb : 0 < b.re
f : ℂ → ℝ → ℂ := fun c x ↦ cexp (-c * ↑x ^ 2)
d : ℝ
hd : 0 < d
hd' : d < b.re
⊢ ∀ x ∈ re ⁻¹' Ioi d, ∀ᵐ (x_1 : ℝ), ‖f x x_1‖ ≤ rexp (-d * x_1 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

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

Tactic:
conv_lhs => rw [mul_assoc]

Goal state after:
case hbc
b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ 2 * (b.im * y) ≤ 2 * |b.im| * |c|
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case a
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
| 2 * |c|

pp: case a
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
| rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
mul_comm

Goal state after:
case a
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
| |c| * 2

case a
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
| rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
y : ℝ
hy : y ∈ uIoc 0 c
absy : |(-y)| ≤ |c|
⊢ ‖cexp (-b * (↑T - ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
simpa only [neg_mul, ofReal_neg] using! vert_norm_bound hT absy

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

Goal state before:
pp: case e_a.e_f
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
⊢ ↑x ^ (a - 1) * cexp (-↑x) = cexp (-↑x) * ↑x ^ (a - 1)

Tactic:
mul_comm

Goal state after:
case e_a.e_f
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
x : ℝ
⊢ cexp (-↑x) * ↑x ^ (a - 1) = cexp (-↑x) * ↑x ^ (a - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Ioi 0
⊢ rexp (-x) * x ^ (s - 1) ≠ 0

Tactic:
exact mul_ne_zero (exp_pos _).ne' (rpow_pos_of_pos hx _).ne'

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

Goal state before:
pp: case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2 + ↑2 * (↑(finrank ℝ V) / 2)) * ‖x‖ ^ (↑2 * (↑(finrank ℝ V) / 2))

Tactic:
mul_comm

Goal state after:
case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ π ^ (↑(finrank ℝ V) / 2) * ‖x‖ ^ ↑(finrank ℝ V) =
    π ^ (-↑(finrank ℝ V) / 2 + ↑2 * (↑(finrank ℝ V) / 2)) * ‖x‖ ^ (↑2 * (↑(finrank ℝ V) / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b)) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
mul_comm

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ cexp (-t ^ 2 / (4 * b)) * (↑π / b) ^ (1 / 2) = cexp (-t ^ 2 / (4 * b)) * (↑π / b) ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_2.e'_7.e'_6
b : ℂ
ι : Type u_2
inst✝ : Fintype ι
hb : 0 < b.re
c : ℂ
w : EuclideanSpace ℝ ι
y : ι → ℝ
⊢ ∑ i, c * (↑(y i) * ↑(w.ofLp i)) = ∑ x, c * (↑(w.ofLp x) * ↑(y x))

Tactic:
mul_comm

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

Goal state before:
pp: case h
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
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ ¬e (-(L v') ((a / ((L v) w - (L v') w)) • w) + (L v) ((a / ((L v) w - (L v') w)) • w)) = 1

Tactic:
simp only [map_sub, LinearMap.sub_apply, LinearMap.zero_apply, AddChar.one_apply,
    map_smul, smul_eq_mul] at ha hw ⊢

Goal state after:
case h
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
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
h : v ≠ v'
w : W
a : ℝ
ha : e a ≠ 1
hw : (L v) w - (L v') w ≠ 0
⊢ ¬e (-(a / ((L v) w - (L v') w) * (L v') w) + a / ((L v) w - (L v') w) * (L v) w) = 1
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ (mFourierSubalgebra d).SeparatesPoints

Tactic:
classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi

Goal state after:
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✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ y : E
⊢ Integrable (fun x ↦ ↑(𝐞 (-inner ℝ x ξ)) • B (f₁ x)) volume

Tactic:
simpa [Circle.smul_def] using
        (Real.fourierIntegral_convergent_iff ξ).2 (B.integrable_comp hf₁)

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
h : ∫⁻ (a : E), ENNReal.ofReal ‖(1 + ‖a‖ ^ 2) ^ (-s)‖ < ∞
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞

Tactic:
norm_cast
        simp_rw [ofReal_norm] at h
        simp_rw [← enorm_pow]
        convert h
        rw [← Real.rpow_mul_natCast (by positivity)]
        simp

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃+ ⨁ (i : ι), ZMod (n i))

Tactic:
by
  classical
  obtain ⟨ι, hι, p, hp, n, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite G
  refine ⟨{i : ι // n i ≠ 0}, inferInstance, fun i ↦ p i ^ n i, ?_,
    ⟨e.trans (directSumNeZeroMulEquiv ι _ _).symm⟩⟩
  rintro ⟨i, hi⟩
  exact one_lt_pow₀ (hp _).one_lt hi

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

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
x : E
⊢ (g * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) x = ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * ⇑g') x

Tactic:
mul_comm

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
x : E
⊢ ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * g) x = ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * ⇑g') x
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
⊢ ‖x‖ ^ 2 * ‖m‖ ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)

Tactic:
mul_comm

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m x : E
h₁ : |(1 + ‖x‖ ^ 2) ^ (-1 / 2)| ^ 2 = (1 + ‖x‖ ^ 2)⁻¹
⊢ ‖m‖ ^ 2 * ‖x‖ ^ 2 ≤ ‖m‖ ^ 2 * (1 + ‖x‖ ^ 2)
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ Summable fun i ↦
    ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (e * f.comp (ContinuousMap.addRight ↑i))‖

Tactic:
convert! hf ⟨uIcc 0 1, isCompact_uIcc⟩ using 1

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ (fun i ↦
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (e * f.comp (ContinuousMap.addRight ↑i))‖) =
    fun n ↦ ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (f.comp (ContinuousMap.addRight ↑n))‖
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ 𝐞 (-⟪v, w⟫) • f (v + i w) = (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)

Tactic:
simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_add]

Goal state after:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (↑(2 * π * -⟪v, w⟫) * I) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w) =
    -((cexp (↑(2 * π * -⟪v, w⟫) * I) * cexp (↑(2 * π * -(1 / 2)) * I)) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w))
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n m : ℕ+
h : 0 < (↑n).gcd ↑m * (↑n).lcm ↑m
⊢ 0 < (↑n).lcm ↑m

Tactic:
mul_comm

Goal state after:
n m : ℕ+
h : 0 < (↑n).lcm ↑m * (↑n).gcd ↑m
⊢ 0 < (↑n).lcm ↑m
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime n → (m * k).gcd n = m.gcd n

Tactic:
mul_comm

Goal state after:
m n k : ℕ+
⊢ k.Coprime n → (k * m).gcd n = m.gcd n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime m → m.gcd (n * k) = m.gcd n

Tactic:
mul_comm

Goal state after:
m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
mul_comm

Goal state after:
a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (a * b).gcd m
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
    -- This `have` unfolds the function composition in `Equiv.summable_iff`.

    -- This `have` unfolds the function composition in `Equiv.summable_iff`.
    have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
    simp_rw [← tsum_apply h, ← tsum_apply this]
    simp [Equiv.coe_addRight, comp_apply, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = i.gcd k * b
⊢ b = k

Tactic:
mul_comm

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ b = k
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K) * cyclotomic' n K =
    cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
mul_comm

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic' i K).Monic
⊢ cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K = cyclotomic' n K * ∏ i ∈ n.properDivisors, cyclotomic' i K
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝ : CommRing R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
k : ℕ
⊢ (X ^ (n * k) - 1).IsRoot ζ

Tactic:
simp [pow_mul, hζ.pow_eq_one]

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

Goal state before:
pp: 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] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Tactic:
mul_comm

Goal state after:
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] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_1
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
n : ℤ
hξ : ζ ^ n ∈ rootsOfUnity k R
hk0 : 0 < ↑k
i : ℤ := n % ↑k
i₀ : ℕ
hi₀ : ↑i₀ = i
⊢ i < ↑k

Tactic:
exact Int.emod_lt_of_pos _ hk0

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

Goal state before:
pp: R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (f q) (map f (cyclotomic n R)) = f (eval q (cyclotomic n R))

Tactic:
eval_map,

Goal state after:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval₂ f (f q) (cyclotomic n R) = f (eval q (cyclotomic n R))
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : IsUnit (map (Int.castRingHom (ZMod p)) P)
⊢ False

Tactic:
replace hunit := degree_eq_zero_of_isUnit hunit

Goal state after:
case neg.inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod : map (Int.castRingHom (ZMod p)) P ^ 2 * R ∣ X ^ n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : ↑1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (X ^ n - 1)
hfree : Squarefree (X ^ n - 1)
hunit : (map (Int.castRingHom (ZMod p)) P).degree = 0
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ (nthRoots n a).Nodup

Tactic:
suffices nthRoots n a = 0 by simp [this]

Goal state after:
case neg
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h✝ : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
hn : n > 0
h : ∀ (α : R), α ^ n ≠ a
⊢ nthRoots n a = 0
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (fun w ↦ ∫ (v : ℝ), 𝐞 (-(v * w)) • f v) (cocompact ℝ) (𝓝 0)

Tactic:
mul_comm

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
⊢ Tendsto (fun w ↦ ∫ (v : ℝ), 𝐞 (-(w * v)) • f v) (cocompact ℝ) (𝓝 0)