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

Goal state before:
pp: V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ ‖(𝓕 f).toLp 2 volume‖ = ‖f.toLp 2 volume‖

Tactic:
norm_eq_sqrt_re_inner (𝕜 := ℂ),

Goal state after:
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : FiniteDimensional ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
f : 𝓢(V, H)
⊢ √(RCLike.re ⟪(𝓕 f).toLp 2 volume, (𝓕 f).toLp 2 volume⟫) = √(RCLike.re ⟪f.toLp 2 volume, f.toLp 2 volume⟫)
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: case a
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
⊢ ∃ u, tsupport ⇑u ⊆ s ∧ (delta x) u ≠ 0

Tactic:
exact ⟨⟨u, h₃, h₂, by aesop⟩, ⟨by aesop, by simp [h₄]⟩⟩

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ = 1

Tactic:
apply le_antisymm

Goal state after:
case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1

case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ 1 ≤ ‖mFourier n‖
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✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (-f) = (Lp.toTemperedDistributionCLM F volume p) (-f')

Tactic:
simp [map_neg, hf]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g : E → ℂ
hg : Function.HasTemperateGrowth g
⊢ smulLeftCLM F (-g) = -smulLeftCLM F g

Tactic:
ext f u
  simp [SchwartzMap.smulLeftCLM_neg hg]

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

Goal state before:
pp: case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∫ (x : UnitAddTorus d), ∏ i, (fourier ((n + -m) i)) (x i) = 0

Tactic:
MeasureTheory.integral_fintype_prod_volume_eq_prod

Goal state after:
case neg
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
h : ¬m = n
⊢ ∏ i, ∫ (x : UnitAddCircle), (fourier ((n + -m) i)) x = 0
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:
rw [fourier_toTemperedDistributionCLM_eq]

Goal state after:
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
⊢ ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
by
      simp_rw [coe_mul, Pi.mul_apply,
        ← ContinuousMap.tsum_apply (summable_of_locally_summable_norm hf), tsum_mul_left]

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

Goal state before:
pp: m n : ℕ+
⊢ m.gcd n = m ↔ m ∣ n

Tactic:
apply gcd_eq_left_iff_dvd

Goal state after:
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
h : ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
⊢ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
intro n hn hnP

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
G : ℕ → R := fun n ↦ ∑ i ∈ n.divisors, f i
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
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
h : ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
⊢ ∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n

Tactic:
intro n hn hnP

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
F : ℕ → R := fun n ↦ ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2
n : ℕ
hn : n > 0
hnP : n ∈ s
⊢ ∑ i ∈ n.divisors, f i = g n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
this : Subsingleton (ℤ →+* S)
⊢ map (f.comp (Int.castRingHom R)) (cyclotomic n ℤ) = map (Int.castRingHom S) (cyclotomic n ℤ)

Tactic:
congr!

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

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

Tactic:
by
  rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
  have : Subsingleton (ℤ →+* S) := inferInstance
  congr!

Goal state after:
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
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
⊢ ∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε

Tactic:
have bdA2 := norm_setIntegral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA

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
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
bdA : ∀ v ∈ A, ‖‖f v - f (v + i w)‖‖ ≤ ε / ↑B
bdA2 : ‖∫ (x : V) in A, ‖f x - f (x + i w)‖‖ ≤ ε / ↑B * volume.real A
⊢ ∫ (v : V) in A, ‖f v - f (v + i w)‖ < 2 * ε
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic x ℤ = (∑ i ∈ range n, X ^ i) * (X - 1)

Tactic:
geom_sum_mul,

Goal state after:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x ∈ n.divisors, cyclotomic x ℤ = X ^ n - 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ✝ n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Nat.card ↥(rootsOfUnity n R) = n

Tactic:
← hζ,

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) n
hζ : ↑ζ = ζ✝
⊢ Nat.card ↥(rootsOfUnity n R) = n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ (∏ i ∈ n.properDivisors, cyclotomic i R) * cyclotomic n R = cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R

pp: case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic i R).degree

Tactic:
· rw [mul_comm]

Goal state after:
case right
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
a✝ : Nontrivial R
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K

Tactic:
| _ k hk
   => 

Goal state after:
case h
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
hk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic m K = cyclotomic' m K
ζ : K
hz : IsPrimitiveRoot ζ k
⊢ cyclotomic k K = cyclotomic' k K
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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
⊢ (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v) = (fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A

Tactic:
ext1 w

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
A : StrongDual ℝ V ≃ₗᵢ⋆[ℝ] V := (InnerProductSpace.toDual ℝ V).symm
w : StrongDual ℝ V
⊢ ∫ (v : V), 𝐞 (-w v) • f v = ((fun w ↦ ∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) ∘ ⇑A) w
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (∑ i ∈ range p, (X ^ p ^ (n_n + 1)) ^ i) * (X ^ p ^ (n_n + 1) - 1) = X ^ p ^ (n_n + 1 + 1) - 1

Tactic:
geom_sum_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    cyclotomic (p ^ (m + 1)) R = ∑ i ∈ range p, (X ^ p ^ m) ^ i ↔
      (∑ i ∈ range p, (X ^ p ^ m) ^ i) * ∏ x ∈ range (m + 1), cyclotomic (p ^ x) R = X ^ p ^ (m + 1) - 1
n_n : ℕ
n_ih : (∑ i ∈ range p, (X ^ p ^ n_n) ^ i) * ∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R = X ^ p ^ (n_n + 1) - 1
⊢ (X ^ p ^ (n_n + 1)) ^ p - 1 = X ^ p ^ (n_n + 1 + 1) - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ (∑ i ∈ range p, (X ^ p ^ k) ^ i) * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1

Tactic:
geom_sum_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ (X ^ p ^ k) ^ p - 1 = X ^ p ^ (k + 1) - 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case h
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
l : ℕ
ha : φ g ^ (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
⊢ (g ^ Nat.card G) ^ l = 1

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
case h
G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
a : G
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
φ : G →* G' := monoidHomOfForallMemZpowers hg hζg
hφg : IsPrimitiveRoot (φ g) (Nat.card G)
l : ℕ
ha : φ g ^ (Nat.card G * l) = 1
hk : g ^ (Nat.card G * l) = a
⊢ (g ^ Fintype.card G) ^ l = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (cyclotomic p ℚ * c).degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j

Tactic:
degree_mul,

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : CharZero K
p : ℕ
ζ : K
hp : Nat.Prime p
hζ : IsPrimitiveRoot ζ p
α : Fin p → ℚ
this : Fact (Nat.Prime p)
P : ℚ[X] := ∑ i, C (α i) * X ^ ↑i
hP : ∀ (i : Fin p), α i = P.coeff ↑i
x✝ : cyclotomic p ℚ ∣ P
c : ℚ[X]
hP' : (cyclotomic p ℚ).degree + c.degree ≤ ↑(p - 1)
hc : P = cyclotomic p ℚ * c
⊢ ∀ (i j : Fin p), α i = α j
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ (cyclotomic (p ^ k * m) R).IsRoot μ

Tactic:
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow,
      h, zero_pow]

Goal state after:
case inr.refine_2
m k p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst✝ : NeZero ↑m
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ k - p ^ (k - 1) ≠ 0
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
F : Type u_2
inst✝³ : Field K
inst✝² : Fintype K
inst✝¹ : Field F
inst✝ : Algebra F K
h : (X ^ Fintype.card K - X).natDegree = Fintype.card K
⊢ (Polynomial.map (algebraMap F K) (X ^ Fintype.card K - X)).Splits

Tactic:
rw [splits_iff_card_roots, Polynomial.map_sub, Polynomial.map_pow,
      map_X, h, FiniteField.roots_X_pow_card_sub_X K, ← Finset.card_def, Finset.card_univ]

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

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K[η + 1]

Tactic:
have hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by simpa using hη

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K[η + 1]
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)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k + 1) / 2 ^ k)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
Nat.pow_div (le_succ k) zero_lt_two,

Goal state after:
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)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k.succ - k))
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
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
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) =
    IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
apply le_antisymm

Goal state after:
case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := ⋯
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ≤
    IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

case a
S : Set ℕ
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension S K L
M : Type u_1
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := ⋯
htop : IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤
⊢ IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ≤
    IntermediateField.adjoin K (⇑i '' {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Module.Basis (↥(IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n))) (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ Fintype.card (GaloisField p n) = p ^ n
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) = n

Tactic:
refine dvd_antisymm ?_ ?_

Goal state after:
case refine_1
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ Monoid.exponent ↥(rootsOfUnity n M) ∣ n

case refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ n ∣ Monoid.exponent ↥(rootsOfUnity n M)
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
k : K
⊢ ∃ a, (Algebra.norm K) a = k

Tactic:
obtain rfl | ne := eq_or_ne k 0

Goal state after:
case inl
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
⊢ ∃ a, (Algebra.norm K) a = 0

case inr
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
k : K
ne : k ≠ 0
⊢ ∃ a, (Algebra.norm K) a = k
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
⊢ p = p'

Tactic:
by_contra hne

Goal state after:
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hne : ¬p = p'
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicRing n A K
⊢ x ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
⊢ ⟨x, hx⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : Rˣ
⊢ (ofUnitHom f) ↑a = ↑(f a)

Tactic:
by simp [ofUnitHom]

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
x : Rˣ
h₂ : χ ↑x = -1
⊢ (χ ↑x)⁻¹ʳ = χ ↑x

Tactic:
have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
    rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]

Goal state after: