mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case inr.inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
hn : n ≠ 0
Z :
  ‖0‖ ^ n * (‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖) ≤
    ‖0‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖0‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) 0‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

pp: case inr.inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
hw : w ≠ 0
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
· simp [hn]
    positivity

Goal state after:
case inr.inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
hw : w ≠ 0
⊢ ‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
x : ℝ
⊢ deriv (𝓕 f) x = 𝓕 (fun x ↦ (-2 * ↑π * I * ↑x) • f x) x

Tactic:
exact (hasDerivAt_fourier hf hf' x).deriv

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:
by
  simp_rw [← rpow_two]
  exact exp_neg_mul_rpow_isLittleO_exp_neg hb one_lt_two

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
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ 𝓕 (iteratedDeriv n f) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
change 𝓕 (fun x ↦ iteratedDeriv n f x) x = _

Goal state after:
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
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ 𝓕 (fun x ↦ iteratedDeriv n f x) x = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

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

Tactic:
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]

Goal state after:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.snd ℝ ℝ ℝ).ker
h : LinearMap.snd ℝ ℝ ℝ = 0
this : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = 0 (0, 1)
⊢ False
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), f 0 x ∂μ 0) * ∏ i, ∫ (x : E i.succ), f i.succ x ∂μ i.succ = ∏ i, ∫ (x : E i), f i x ∂μ i

Tactic:
by rw [Fin.prod_univ_succ]

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

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ 0 < (↑b).re

Tactic:
by rwa [ofReal_re]

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

Goal state before:
pp: 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
hf : Integrable f volume
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : V), ‖cexp (-↑n⁻¹ * ↑‖a‖ ^ 2) • f a‖ ≤ ‖f a‖

Tactic:
· filter_upwards [Ici_mem_atTop (0 : ℝ)] with c (hc : 0 ≤ c)
    filter_upwards with v
    simp only [ofReal_inv, neg_mul, norm_smul]
    norm_cast
    conv_rhs => rw [← one_mul (‖f v‖)]
    gcongr
    simp only [norm_eq_abs, abs_exp, exp_le_one_iff, Left.neg_nonpos_iff]
    positivity

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

Goal state before:
pp: case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ Gamma (↑(n + 1) + 1) = ↑(n + 1)!

Tactic:
rw [Gamma_add_one n.succ <| Nat.cast_ne_zero.mpr <| Nat.succ_ne_zero n]

Goal state after:
case succ
n : ℕ
hn : Gamma (↑n + 1) = ↑n !
⊢ ↑n.succ * Gamma ↑n.succ = ↑(n + 1)!
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: ⊢ (Complex.Gamma 1).re = 1

Tactic:
Complex.Gamma_one,

Goal state after:
⊢ Complex.re 1 = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
by rwa [ofReal_re]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ‖x‖ ^ 2) f

Tactic:
let ι := Fin (Module.finrank ℝ E)

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ‖x‖ ^ 2) f
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f

Tactic:
let ι := Fin (Module.finrank ℝ E)

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢'(E, F)
ι : Type := Fin (Module.finrank ℝ E)
⊢ Δ f = -(2 * π) ^ 2 • (fourierMultiplierCLM F fun x ↦ ↑(‖x‖ ^ 2)) f
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ toTemperedDistribution (f.toLp p μ) = (toTemperedDistributionCLM E F μ) f

Tactic:
ext g

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ (toTemperedDistribution (f.toLp p μ)) g = ((toTemperedDistributionCLM E F μ) f) g
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
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
⊢ ∃ w, (char he hL w) v ≠ (char he hL w) v'

Tactic:
use (a / (L (v - v') w)) • w

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
hw : (L (v - v')) w ≠ 0 w
a : ℝ
ha : e a ≠ 1 a
⊢ (char he hL ((a / (L (v - v')) w) • w)) v ≠ (char he hL ((a / (L (v - v')) w) • w)) v'
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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ MemSobolev s p ((SchwartzMap.toTemperedDistributionCLM E F volume) f)

Tactic:
use (SchwartzMap.fourierMultiplierCLM F (fun x ↦ ((1 + ‖x‖ ^ 2) ^ (s / 2) : ℝ)) f).toLp p
  rw [besselPotential, Lp.toTemperedDistribution_toLp_eq,
    fourierMultiplierCLM_toTemperedDistributionCLM_eq (by fun_prop)]
  congr 1
  apply SchwartzMap.fourierMultiplierCLM_ofReal ℂ
    (Function.hasTemperateGrowth_one_add_norm_sq_rpow E (s / 2))

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(E, F)
⊢ 𝓕 ((toTemperedDistributionCLM E F volume) f) = (toTemperedDistributionCLM E F volume) (𝓕 f)

Tactic:
ext g

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ (𝓕 ((toTemperedDistributionCLM E F volume) f)) g = ((toTemperedDistributionCLM E F volume) (𝓕 f)) g
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: case h
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
⊢ ¬‖w‖ ^ 2 = 0

Tactic:
sq_eq_zero_iff,

Goal state after:
case h
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
⊢ ¬‖w‖ = 0
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 : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ c * ‖|↑y| ^ (-b)‖ ≤ c * ((1 / 2) ^ (-b) * ‖|x| ^ (-b)‖)

Tactic:
mul_le_mul_iff_right₀ hc,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ (b_1 : ℝ), d ≤ b_1 → ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ ‖|↑y| ^ (-b)‖ ≤ (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 0 R = ∅

Tactic:
rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ primitiveRoots n R, X - C i ≠ 0

Tactic:
intro z

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
⊢ z ∈ primitiveRoots n R → X - C z ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ i ∈ primitiveRoots n K, (X - C i).Splits

Tactic:
intro z

Goal state after:
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
⊢ z ∈ primitiveRoots n K → (X - C z).Splits
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst✝ : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
⊢ False

Tactic:
have hp : Fact p.Prime := CharP.char_is_prime_of_pos R p

Goal state after:
R : Type u_4
ζ : R
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ := ringChar R
n : ℕ
inst✝ : NeZero (p * n)
hζ : IsPrimitiveRoot ζ (p * n)
h : p ≠ 0 ∧ n ≠ 0
this : NeZero p
hp : Fact (Nat.Prime p)
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case neg
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
⊢ False

Tactic:
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)

Goal state after:
case neg
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
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = n

Tactic:
by
    refine Eq.trans ?_ hμ.eq_orderOf.symm -- `rw [hμ.eq_orderOf]` gives "motive not type correct"
    rw [← hμ.val_toRootsOfUnity_coe, orderOf_units, Subgroup.orderOf_coe]

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

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ (cyclotomic n ℤ).natDegree ≤ (minpoly ℤ μ).natDegree

Tactic:
simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
this✝ : B.gen ^ n = (aeval B.gen) Q
hQ : ¬Q = 0
this : Nontrivial R := Nontrivial.of_polynomial_ne hQ
⊢ Q.degree < (minpoly R B.gen).degree

Tactic:
exact degree_modByMonic_lt _ (minpoly.monic hB)

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

Goal state before:
pp: case h.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 < ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)

pp: case h.inr.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 = ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)

pp: case h.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)

Tactic:
· apply pos_of_mul_pos_left
    · rwa [this]
    rw [eval_prod]
    refine Finset.prod_nonneg fun i hi => ?_
    simp only [Finset.mem_erase, mem_properDivisors] at hi
    rw [geom_sum_pos_iff hn'.ne'] at h
    rcases h with hk | hx
    · refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl
      · exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
      · exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk
    · rcases eq_or_ne i 2 with (rfl | hk)
      · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
      refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
      rintro rfl
      exact hn'.ne' <| zero_dvd_iff.mp hi.2.1

Goal state after:
case h.inr.inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : 0 = ∑ i ∈ range n, x ^ i
⊢ 0 < eval x (cyclotomic n R)

case h.inr.inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
hn'' : 1 < n
this : eval x (cyclotomic n R) * eval x (∏ x ∈ n.properDivisors.erase 1, cyclotomic x R) = ∑ i ∈ range n, x ^ i
h : ∑ i ∈ range n, x ^ i < 0
⊢ 0 < eval x (cyclotomic n R)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : (cyclotomic l K).IsRoot x
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r

Tactic:
rw [isRoot_cyclotomic_iff] at hlroot

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
hnegζ : IsPrimitiveRoot (-ζ) (2 * n)
k : ℕ
hkpos : 0 < k
hkn : x ^ k = 1
l : ℕ
hl : l ∈ k.divisors
hlroot : IsPrimitiveRoot x l
hlzero : NeZero l
this : NeZero ↑l
⊢ ∃ r, x = (-ζ) ^ r
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: q : ℝ
hq' : 1 < q
⊢ (q - 1) ^ φ 1 ≤ eval q (cyclotomic 1 ℝ)

Tactic:
simp only [totient_one, pow_one, cyclotomic_one, eval_sub, eval_X, eval_one, le_refl]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L

Tactic:
have := charZero_of_injective_algebraMap (algebraMap K L).injective

Goal state after:
S : Set ℕ
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this : CharZero L
⊢ FiniteDimensional ℚ L
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n m : ℕ
hm : NeZero m
h : n ∣ m
⊢ Function.Surjective ⇑(unitsMap h)

Tactic:
suffices ∀ x : ℕ, x.Coprime n → ∃ k : ℕ, (x + k * n).Coprime m by
    intro x
    have ⟨k, hk⟩ := this x.val.val (val_coe_unit_coprime x)
    refine ⟨unitOfCoprime _ hk, Units.ext ?_⟩
    have : NeZero n := ⟨fun hn ↦ hm.out (eq_zero_of_zero_dvd (hn ▸ h))⟩
    simp [unitsMap_def, -castHom_apply]

Goal state after:
n m : ℕ
hm : NeZero m
h : n ∣ m
⊢ ∀ (x : ℕ), x.Coprime n → ∃ k, (x + k * n).Coprime m
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
have := hζ.pow_of_dvd
    (fun h => two_ne_zero (eq_zero_of_pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))
  rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this
  have H : (-1 : L) - (1 : L) = algebraMap K L (-2) := by
    simp only [map_neg, map_ofNat]
    ring
  replace hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K) := by simp [hirr]
  rw [this.eq_neg_one_of_two_right, H, Algebra.norm_algebraMap,
    IsCyclotomicExtension.finrank L hirr, totient_prime_pow Nat.prime_two (zero_lt_succ k),
    succ_sub_succ_eq_sub, tsub_zero]
  simp

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
h : d = N
⊢ False

Tactic:
by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

Goal state after: