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

Goal state before:
pp: b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
x w : V
⊢ b ≠ 0

Tactic:
contrapose! hb

Goal state after:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
x w : V
hb : b = 0
⊢ b.re ≤ 0
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ ∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
    ∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      (2 ^ volume.integrablePower * ∫ (x : V), (1 + ‖x‖) ^ (-↑volume.integrablePower)) * 2 *
        ((Finset.range (n + volume.integrablePower + 1) ×ˢ Finset.range (k + 1)).sup (schwartzSeminormFamily 𝕜 V E)) f

Tactic:
by
      gcongr with p
      apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans
      simp only [mul_assoc, two_mul]
      gcongr
      · have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)
      · have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all
        apply Seminorm.le_def.mp (Finset.le_sup (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2) this)

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

Goal state before:
pp: case right
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
⊢ eLpNorm (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume < ∞

Tactic:
eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (by norm_num) (by norm_num)

Goal state after:
case right
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
⊢ ∫⁻ (a : E), ‖(1 + ‖a‖ ^ 2) ^ (-s / 2)‖ₑ ^ ENNReal.toReal 2 < ∞
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
⊢ (smulLeftCLM F (g * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)))) (𝓕 f) =
    (smulLeftCLM F ⇑g') ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f))

Tactic:
smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by apply hg₁)

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
⊢ (smulLeftCLM F (g * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2)))) (𝓕 f) =
    (smulLeftCLM F ((fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) * ⇑g')) (𝓕 f)
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
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
rw [norm_norm, ContinuousMap.norm_le _ (by positivity)]

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
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: 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:
constructor
  · intro h
    let G := fun (n : ℕ) => (∑ i ∈ n.divisors, f i)
    intro n hn hnP
    suffices ∑ d ∈ n.divisors, μ (n / d) • G d = f n by
      rw [sum_divisorsAntidiagonal' (f := fun x y => μ x • g y), ← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
    rw [← sum_divisorsAntidiagonal' (f := fun x y => μ x • G y)]
    apply sum_eq_iff_sum_smul_moebius_eq.mp _ n hn
    intro _ _; rfl
  · intro h
    let F := fun (n : ℕ) => ∑ x ∈ n.divisorsAntidiagonal, μ x.fst • g x.snd
    intro n hn hnP
    suffices ∑ d ∈ n.divisors, F d = g n by
      rw [← this, sum_congr rfl]
      intro d hd
      rw [← h d (pos_of_mem_divisors hd) <| hs d n (dvd_of_mem_divisors hd) hnP]
    apply sum_eq_iff_sum_smul_moebius_eq.mpr _ n hn
    intro _ _; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
hs₀ : 0 ∉ s
P : ℕ → Prop
⊢ (∀ n ∈ s, P n) ↔ ∀ n > 0, n ∈ s → P n

Tactic:
refine forall_congr' (fun n ↦ ⟨fun h _ ↦ h, fun h hn ↦ h ?_ hn⟩)
    contrapose! hs₀
    simpa [nonpos_iff_eq_zero.mp hs₀] using hn

Goal state after:
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))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
rw [tsum_eq_zero_of_not_summable h]
    simp only [coe_zero, Pi.zero_apply]

Goal state after:
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).degree

Tactic:
rw [bot_lt_iff_ne_bot]

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
⊢ (∏ i ∈ n.properDivisors, cyclotomic' i K).degree ≠ ⊥
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑(if i * 2 ≤ n then ↑i else ↑i - ↑n) / ↑n * (2 * Real.pi)

Tactic:
split_ifs with h₂

Goal state after:
case pos
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑↑i / ↑n * (2 * Real.pi)

case neg
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (Complex.cos (↑i / ↑n * (2 * ↑Real.pi)) + Complex.sin (↑i / ↑n * (2 * ↑Real.pi)) * Complex.I).arg =
    ↑(↑i - ↑n) / ↑n * (2 * Real.pi)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inr
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
Bint : ∃ q, map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint

Goal state after:
case h.inr
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
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ X ^ n - 1

Tactic:
by
  rcases n.eq_zero_or_pos with (rfl | h0)
  · simp
  apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
  simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow,
    aeval_one, map_sub, sub_self]

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) (cyclotomic n S) = f (eval q (cyclotomic n R))

Tactic:
rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
⊢ IsUnit u → IsPrimitiveRoot μ n✝ → u.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ u)

Tactic:
hunit

Goal state after:
case refine_2
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ u : ℕ
hunit : IsUnit u
⊢ IsPrimitiveRoot μ n✝ → u.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ u)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
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 [bot_lt_iff_ne_bot]

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 refine_2
R : Type u_1
inst✝ : CommRing R
p : ℕ
hpri : Nat.Prime p
hp : p ≠ 2
a r : R
h₁ : r ∣ a ^ p
h₂ : r ∣ ↑p * a
⊢ C r ∣ ↑p * (C a * X)

Tactic:
simp only [map_mul, map_natCast, ← mul_assoc, dvd_mul_right, (_root_.map_dvd C h₂).trans]

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

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ q - 1 < ‖↑q - ζ‖

Tactic:
suffices ¬SameRay ℝ (q : ℂ) ζ by
      convert! lt_norm_sub_of_not_sameRay this <;>
        simp only [hζ.norm'_eq_one hn.ne', Real.norm_of_nonneg hq.le, Complex.norm_real]

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬SameRay ℝ (↑q) ζ
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
refine
    ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩

Goal state after:
case refine_1
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
s : ℕ
hs : s ∈ S
⊢ s ≠ 0 → ∃ r, IsPrimitiveRoot r s

case refine_2
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
_root_.map_intCast,

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (Polynomial.map (Int.castRingHom E) (cyclotomic n ℤ)) = ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case right
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = f r
⊢ f (g r) = g (f r)

Tactic:
obtain ⟨mg, -, hg⟩ := hr.eq_pow_of_pow_eq_one (show g r ^ n = 1 by rw [← map_pow, hr.1, map_one])

Goal state after:
case right
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsCyclotomicExtension S A B
inst✝ : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = f r
mg : ℕ
hg : r ^ mg = g r
⊢ f (g r) = g (f r)
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
this✝ : Finite K
this : Fintype K
i : Fin (Module.finrank K L)
⊢ x ^ Nat.card K ^ ↑i = (frobeniusAlgEquivOfAlgebraic K L ^ ↑i) x

Tactic:
rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : (n % ↑m).gcd ↑m = 1
⊢ IsCoprime (↑m) n

Tactic:
Int.gcd_emod

Goal state after:
case inr
n : ℤ
m : ℕ
hm : m ≠ 0
this : NeZero m
u : (ZMod m)ˣ
hu : ↑u = ↑n
h_coprime : n.gcd ↑m = 1
⊢ IsCoprime (↑m) 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
⊢ Nat.card ↥(rootsOfUnity n M) = n

Tactic:
← IsCyclic.exponent_eq_card

Goal state after:
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
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_3
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (y + z) * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑(a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
map_mul,

Goal state after:
case refine_3
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ (y + z) *
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * ↑b.2 + b.1 * ↑a.2, ⟨↑a.2 * ↑b.2, ⋯⟩).1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ R → R'

Tactic:
classical exact fun x => if IsUnit x then 1 else 0

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

Goal state before:
pp: case refine_4
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ y * z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑(a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
map_mul,

Goal state after:
case refine_4
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✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑n
x : CyclotomicField n K
this : NeZero ↑n
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  y * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  z * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1
⊢ y * z *
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
        (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.2) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
⊢ Function.LeftInverse ofUnitHom toUnitHom

Tactic:
intro χ
    ext x
    rw [ofUnitHom_coe, coe_toUnitHom]

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

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Finite F
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
χ : MulChar F R
n : ℕ
inst✝ : NeZero n
hχ : χ ^ n = 1
μ : R
hμ : IsPrimitiveRoot μ n
a : F
h : a ≠ 0
⊢ χ a ∈ ℤ[μ]

Tactic:
· obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h
    rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁
    obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁
    exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k

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

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) ((changeLevel ⋯) ⋯.choose)

Tactic:
← (factorsThrough_conductor (Classical.choose hd.2)).2.choose_spec

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
d : ℕ
hd : d ∈ χ.conductorSet
⊢ χ = (changeLevel ⋯) (Classical.choose ⋯)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
have hζ := hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)

Goal state after:
A : Type u
B : Type v
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension {n₁} A ↥C₁
h₂ : IsCyclotomicExtension {n₂} A ↥C₂
inst✝¹ : NeZero n₁
inst✝ : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot ((algebraMap (↥C₁) B) ζ₁) n₁
hζ₂ : IsPrimitiveRoot ((algebraMap (↥C₂) B) ζ₂) n₂
hζ :
  IsPrimitiveRoot
    ((algebraMap (↥C₁) B) ζ₁ ^ (n₁ / n₁.factorizationLCMLeft n₂) *
      (algebraMap (↥C₂) B) ζ₂ ^ (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)