mathlib-initiative/mathlib-tactics huggingface dataset:
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) fun v ↦ fourierPowSMulRight L f v n

Tactic:
ext w : 1

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
w : W
⊢ iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fun v ↦ fourierPowSMulRight L f v n) w
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
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 *
      ∫ (a : V), ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖ ∂μ

Tactic:
← integral_const_mul

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), ‖iteratedFDeriv ℝ n (fun v ↦ fourierPowSMulRight L f v k) v‖ ∂μ ≤
    ∫ (a : V),
      (2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖a‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f a‖ ∂μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ (↑a).re < 0

Tactic:
by simpa using! ha

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

Goal state before:
pp: a : ℝ
ha : 0 < a
c : ℝ
⊢ 0 < (↑a).re

Tactic:
by simpa using! ha

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

Goal state before:
pp: s : ℝ
⊢ ¬IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume

Tactic:
intro h

Goal state after:
s : ℝ
h : IntegrableOn (fun x ↦ x ^ s) (Ioi 0) volume
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
⊢ ¬IntegrableOn (fun x ↦ ↑x ^ s) (Ioi 0) volume

Tactic:
intro h

Goal state after:
s : ℂ
h : IntegrableOn (fun x ↦ ↑x ^ s) (Ioi 0) volume
⊢ False
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
  simpa only [mul_comm] using Real.Gamma_integrand_isLittleO s

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s

Tactic:
have der_ible :=
    (Gamma_integrand_deriv_integrable_A hs hX).add (Gamma_integrand_deriv_integrable_B hs hX)

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
⊢ ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s =
    (s * ∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
n : ℕ
E : Fin n → Type u_3
mE : (i : Fin n) → MeasurableSpace (E i)
μ : (i : Fin n) → Measure (E i)
inst✝ : ∀ (i : Fin n), SigmaFinite (μ i)
f : (i : Fin n) → E i → 𝕜
hf : ∀ (i : Fin n), Integrable (f i) (μ i)
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
by
  induction n with
  | zero => simp only [Finset.univ_eq_empty, Finset.prod_empty, isFiniteMeasure_iff,
      integrable_const_iff, pi_empty_univ, ENNReal.one_lt_top, or_true]
  | succ n n_ih =>
      have := ((measurePreserving_piFinSuccAbove μ 0).symm)
      rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]
      simp_rw [MeasurableEquiv.piFinSuccAbove_symm_apply, Fin.insertNthEquiv,
        Fin.prod_univ_succ, Fin.insertNth_zero]
      simp only [Fin.zero_succAbove, Function.comp_def]
      have : Integrable (fun (x : (j : Fin n) → E (Fin.succ j)) ↦ ∏ j, f (Fin.succ j) (x j))
          (Measure.pi (fun i ↦ μ i.succ)) :=
        n_ih (fun i ↦ hf _)
      exact Integrable.mul_prod (hf 0) this

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

Goal state before:
pp: A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0

Tactic:
intro h

Goal state after:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℝ × ℝ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p

Tactic:
symm
  calc
    _ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
      rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
        polarCoord.symm_image_target_eq_source]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) := by
      rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
        (fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
      · simp_rw [det_fderivPolarCoordSymm]; rfl
      exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
    _ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) := by
      refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
      rw [abs_of_pos hx.1]

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = (s + 1).partialGamma X

Tactic:
partialGamma_add_one hs (mem_Ici.mp hX)

Goal state after:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : X ∈ Ici 0
⊢ (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) X = s * s.partialGamma X - ↑(rexp (-X)) * ↑X ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c✝ T✝ : ℝ
hT✝ : 0 ≤ T✝
T : ℝ
hT : 0 ≤ T
c y : ℝ
hy : |y| ≤ |c|
⊢ ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
norm_cexp_neg_mul_sq_add_mul_I b

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

Goal state before:
pp: case e'_2
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    2 * ∫ (x : ℝ) in Ioi 0, rexp (-1 * x ^ 2)

Tactic:
← integral_const_mul

Goal state after:
case e'_2
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    ∫ (a : ℝ) in Ioi 0, 2 * rexp (-1 * a ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c d : ℂ
⊢ (-b).re < 0

Tactic:
simpa using hb

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

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
u : E → ℝ
h₁ : tsupport u ⊆ s
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑⊤) u
h₄ : u x = 1
h₁' : tsupport (⇑Complex.ofRealCLM ∘ u) ⊆ s
h₂' : HasCompactSupport (⇑Complex.ofRealCLM ∘ u)
⊢ (TemperedDistribution.delta x) (h₂'.toSchwartzMap ⋯) ≠ 0

Tactic:
by simp [h₄]

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

Goal state before:
pp: case mp
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✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F (-s)) f = g → (besselPotential E F s) g = f

Tactic:
intro h

Goal state after:
case mp
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✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F (-s)) f = g
⊢ (besselPotential E F s) g = f
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case mpr
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✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
⊢ (besselPotential E F s) g = f → (besselPotential E F (-s)) f = g

Tactic:
intro h

Goal state after:
case mpr
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✝ : NormedSpace ℂ F
s : ℝ
f g : 𝓢'(E, F)
h : (besselPotential E F s) g = f
⊢ (besselPotential E F (-s)) f = g
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_11
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
Ω : Opens E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
x : E
hx : x ∈ Ω
s : Set E
hxs : x ∈ s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
t : Set E := s ∩ ↑Ω
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htx : x ∈ t
u : E → ℝ
h₁ : tsupport u ⊆ t
h₂ : HasCompactSupport u
h₃ : ContDiff ℝ (↑n) u
h₄ : u x = 1
⊢ (delta x) { toFun := u, contDiff' := h₃, hasCompactSupport' := h₂, tsupport_subset' := ⋯ } ≠ 0

Tactic:
by simp [h₄]

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

Goal state before:
pp: p : ℕ+
pp : p.Prime
⊢ ¬p ∣ 1

Tactic:
dvd_iff

Goal state after:
p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n

Tactic:
dvd_iff

Goal state after:
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n
Module: Mathlib.Data.PNat.Prime

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
rw [← coprime_coe]

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

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

Tactic:
intro h

Goal state after:
m n k : ℕ+
h : 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 (k * n) = m.gcd n

Tactic:
intro h

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

Goal state before:
pp: m k n : ℕ+
⊢ m ∣ k → k.Coprime n → m.Coprime n

Tactic:
dvd_iff

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n

Tactic:
rw [← coprime_coe]

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

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → m.Coprime n

Tactic:
rw [← coprime_coe]

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

Goal state before:
pp: m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Tactic:
rw [← coprime_coe]

Goal state after:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
n : ℕ
⊢ μ n ≠ 0 → Squarefree n

Tactic:
intro h

Goal state after:
case mp
n : ℕ
h : μ n ≠ 0
⊢ Squarefree n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
n : ℕ
⊢ Squarefree n → μ n ≠ 0

Tactic:
intro h

Goal state after:
case mpr
n : ℕ
h : Squarefree n
⊢ μ n ≠ 0
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
hf : Integrable f volume
⊢ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v = (1 / 2) • ∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))

Tactic:
by
  simp_rw [smul_sub]
  rw [integral_sub, fourierIntegral_half_period_translate hw, sub_eq_add_neg, neg_neg, ←
    two_smul ℂ _, ← @smul_assoc _ _ _ _ _ _ (IsScalarTower.left ℂ), smul_eq_mul]
  · simp
  exacts [(Real.fourierIntegral_convergent_iff w).2 hf,
    (Real.fourierIntegral_convergent_iff w).2 (hf.comp_add_right _)]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' → μ • g' = f'

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : ↑ζ • f' = g'
⊢ μ • g' = f'
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ μ • g' = f' → ↑ζ • f' = g'

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
h : μ • g' = f'
⊢ ↑ζ • f' = g'
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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B₀ : ℝ≥0∞ := volume A
hc : B₀ < ∞
⊢ volume A ≤ ↑B₀.toNNReal + 1

Tactic:
ENNReal.coe_toNNReal hc.ne

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
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B₀ : ℝ≥0∞ := volume A
hc : B₀ < ∞
⊢ volume A ≤ B₀ + 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) → ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
⊢ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
⊢ (fun x ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x ↦ |x| ^ (-b)

Tactic:
by
  -- First establish an explicit estimate on decay of inverse powers.
  -- This is logically independent of the rest of the proof, but of no mathematical interest in
  -- itself, so it is proved in-line rather than being formulated as a separate lemma.
  have claim : ∀ x : ℝ, max 0 (-2 * R) < x → ∀ y : ℝ, x + R ≤ y →
      y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b) := fun x hx y hy ↦ by
    rw [max_lt_iff] at hx
    obtain ⟨hx1, hx2⟩ := hx
    rw [← mul_rpow] <;> try positivity
    apply rpow_le_rpow_of_nonpos <;> linarith
  -- Now the main proof.
  obtain ⟨c, hc, hc'⟩ := hf.exists_pos
  simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢
  obtain ⟨d, hd⟩ := hc'
  refine ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => ?_⟩⟩
  rw [max_le_iff] at hx
  have hx' : max 0 (-2 * R) < x := by linarith
  rw [max_lt_iff] at hx'
  rw [norm_norm, ContinuousMap.norm_le _ (by positivity)]
  refine fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans ?_
  have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity
  rw [mul_assoc, mul_le_mul_iff_right₀ hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]
  convert! claim x (by linarith only [hx.1]) y.1 y.2.1
  · apply abs_of_nonneg; linarith [y.2.1]
  · exact abs_of_pos hx'.1

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) → ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
⊢ ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
⊢ IsPrimitiveRoot ζ 1 → ζ = 1

Tactic:
intro h

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
ζ : M
h : IsPrimitiveRoot ζ 1
⊢ ζ = 1
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case neg
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))
⊢ 0 (x + p) = 0 x

Tactic:
simp only [coe_zero, Pi.zero_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ ↑(range n)
j : ℕ
hj : j ∈ ↑(range n)
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j

Tactic:
Finset.coe_range,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ Set.Iio n
j : ℕ
hj : j ∈ Set.Iio n
e : (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) j
⊢ i = j
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Odd q.num
⊢ cexp (↑π * I * ↑q) = cexp (2 * ↑π * I * ↑(q / 2))

pp: case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (q / 2).den

Tactic:
· push_cast
    ring_nf

Goal state after:
case e'_4
q : ℚ
h : Odd q.num
⊢ 2 * q.den = (q / 2).den
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ IsPrimitiveRoot ζ n → ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ

Tactic:
intro h

Goal state after:
case mp
ζ : ℂ
n : ℕ
hn : n ≠ 0
hn0 : ↑n ≠ 0
h : IsPrimitiveRoot ζ n
⊢ ∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
by_cases h0 : 0 ≤ l

Goal state after:
case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : 0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l