mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
a : R
ha : a ≠ 0
⊢ (nthRoots n a).Nodup

Tactic:
by
  obtain (rfl | hn) := n.eq_zero_or_pos; · simp
  by_cases! h : ∃ α, α ^ n = a
  · obtain ⟨α, hα⟩ := h
    by_cases hα' : α = 0
    · exact (ha (by rwa [hα', zero_pow hn.ne', eq_comm] at hα)).elim
    rw [nthRoots_eq h hα, Multiset.nodup_map_iff_inj_on (Multiset.nodup_range n)]
    exact h.injOn_pow_mul hα'
  · suffices nthRoots n a = 0 by simp [this]
    simpa only [Multiset.card_eq_zero, Multiset.eq_zero_iff_forall_notMem, mem_nthRoots hn]

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

Goal state before:
pp: case inr.inl
n : ℕ
hnzero : n > 0
h : n ≠ 0
⊢ IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)

Tactic:
exact isCoprime_one_right

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

Goal state before:
pp: case refine_2
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
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n✝ : ℕ
a✝ : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) → ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ m)) i)
⊢ (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
    ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ (n + 1))) i)

Tactic:
intro hx
    rw [pow_succ]
    exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin

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

Goal state before:
pp: R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) R = cyclotomic n R ^ (p - 1)

Tactic:
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1) by
    rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]

Goal state after:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hn : ¬p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
⊢ cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ (p - 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case succ.succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic (0 + 1 + 1) R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic (0 + 1 + 1) R))

Tactic:
simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]

Goal state after:
case succ.succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)
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
⊢ 2 * n = orderOf (-1) * orderOf ζ

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
⊢ (orderOf (-1)).Coprime (orderOf ζ)

Tactic:
· simp [hζ.eq_orderOf]

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
⊢ (orderOf (-1)).Coprime (orderOf ζ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} ⊆ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

pp: case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} ⊆ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
· rintro x ⟨n, hn₁ | hn₂, hnpow⟩
      · left; exact ⟨n, hn₁, hnpow⟩
      · right; exact ⟨n, hn₂, hnpow⟩

Goal state after:
case refine_2
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} ⊆ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
⊢ IsCyclotomicExtension S A C

Tactic:
let : Algebra B C := f.toAlgHom.toRingHom.toAlgebra

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := (↑f).toAlgebra
⊢ IsCyclotomicExtension S A C
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_1
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))
⊢ K⟮η⟯ ≤ K⟮η + 1⟯

Tactic:
rw [IntermediateField.adjoin_simple_le_iff]

Goal state after:
case refine_1
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))
⊢ η ∈ K⟮η + 1⟯
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: 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
H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r
x : B
hx : x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ f x = g x

Tactic:
induction hx using Algebra.adjoin_induction with

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

Goal state before:
pp: case refine_2
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))
⊢ K⟮η + 1⟯ ≤ K⟮η⟯

Tactic:
rw [IntermediateField.adjoin_simple_le_iff]

Goal state after:
case refine_2
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))
⊢ η + 1 ∈ K⟮η⟯
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case e'_1
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))
⊢ {p ^ (k - s + 1)} = {p ^ (k + 1 - s)}

Tactic:
rw [Nat.sub_add_comm hs]

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

Goal state before:
pp: case e'_4
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))
this : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
⊢ p ^ (k - s + 1) = p ^ (k + 1 - s)

Tactic:
rw [Nat.sub_add_comm hs]

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

Goal state before:
pp: N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d * (↑a₀ * p + ↑N₀ * q) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
mul_comm _ p,

Goal state after:
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
p q : ℤ
hpq : ↑d * (p * ↑a₀ + ↑N₀ * q) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ (X ^ (n✝ + 1) - X).Splits

Tactic:
rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ (Polynomial.map (algebraMap (ZMod p) K) (X ^ Fintype.card K - X)).Splits

Tactic:
exact (FiniteField.isSplittingField_sub K (ZMod p)).splits

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

Goal state before:
pp: C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
⊢ a ≠ 0 → ψ.mulShift a ≠ 1

Tactic:
ha

Goal state after:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
⊢ ψ.mulShift a ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
⊢ (zmodChar n ⋯) a = 1 → a = 0

Tactic:
ha

Goal state after:
C : Type v
inst✝¹ : CommMonoid C
n : ℕ
inst✝ : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : (zmodChar n ⋯) a = 1
⊢ a = 0
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?refine_2.refine_1⟩
⊢ orderOf ⋯.unit ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
← Subgroup.orderOf_mk

Goal state after:
case refine_2.refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?refine_2.refine_1⟩
⊢ orderOf ⟨⋯.unit, ?refine_2.refine_2.ha⟩ ∣ Monoid.exponent ↥(rootsOfUnity n M)

case refine_2.refine_2.ha
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⟨⋯.unit, ?refine_2.refine_1⟩
⊢ ⋯.unit ∈ ?m.87

M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
ζ' : ↥(rootsOfUnity n M) := ⋯
⊢ Subgroup Mˣ
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case h
n : ℕ
inst✝² : NeZero n
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
hm✝ : HasEnoughRootsOfUnity M n
e : ↥(rootsOfUnity n M) ≃* ↥(rootsOfUnity n N)
m : M
hm : IsPrimitiveRoot m n
⊢ IsPrimitiveRoot hm.toRootsOfUnity n

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, ← IsPrimitiveRoot.coe_units_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : R
⊢ ¬IsUnit a → (if IsUnit a then 1 else 0) = 0

Tactic:
ha

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
a : R
ha : ¬IsUnit a
⊢ (if IsUnit a then 1 else 0) = 0
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
⊢ ¬IsUnit a → (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0

Tactic:
ha

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : R
ha : ¬IsUnit a
⊢ (if hx : IsUnit a then ↑(f hx.unit) else 0) = 0
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 * (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.2 *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1

Tactic:
ha

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
⊢ (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.1 *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.1 =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) (a.1 * b.1, ⟨↑a.2 * ↑b.2, ⋯⟩).1
Module: Mathlib.NumberTheory.MulChar.Lemmas

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
⊢ ∃ χ, orderOf χ = n

Tactic:
have h' : ζ' ^ (Fintype.card Fˣ : ℕ) = 1 :=
    Units.ext_iff.mpr <| (hζ.pow_eq_one_iff_dvd _).mpr <| Fintype.card_units (α := F) ▸ h

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
n : ℕ
h : n ∣ Fintype.card F - 1
ζ : R
hζ : IsPrimitiveRoot ζ n
hn₀ : 0 < n
e : MulChar F R ≃* ↥(rootsOfUnity (Fintype.card Fˣ) R) := equiv_rootsOfUnity F R
ζ' : Rˣ := ⋯.unit
h' : ζ' ^ Fintype.card Fˣ = 1
⊢ ∃ χ, orderOf χ = n
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case a
n : ℕ
inst✝⁴ : NeZero n
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ A[ζ] ≤ adjoin A {b | n ≠ 0 ∧ b ^ n = 1}

Tactic:
· exact adjoin_mono <| Set.singleton_subset_iff.mpr ⟨NeZero.ne n, hζ.pow_eq_one⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
this✝ : (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter = χ.primitiveCharacter
this : ((changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter) ↑a = χ.primitiveCharacter ↑a
⊢ ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a

Tactic:
changeLevel_eq_cast_of_dvd' _ _ ha

Goal state after:
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
this✝ : (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter = χ.primitiveCharacter
this : ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a
⊢ ((changeLevel hm) χ).primitiveCharacter ↑a = χ.primitiveCharacter ↑a
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
⊢ (changeLevel ⋯) ((changeLevel hm) χ).primitiveCharacter = (changeLevel ⋯) χ.primitiveCharacter

Tactic:
changeLevel_primitiveCharacter,

Goal state after:
case pos
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : Nontrivial R
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
χ : DirichletCharacter R n
a : ℤ
ha : IsCoprime a ↑χ.conductor
⊢ (changeLevel hm) χ = (changeLevel ⋯) χ.primitiveCharacter
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ χ * ψ = (changeLevel ⋯) χ.primitiveCharacter * (changeLevel ⋯) ψ.primitiveCharacter

Tactic:
changeLevel_primitiveCharacter,

Goal state after:
case inr
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ ψ : DirichletCharacter R n
hn : NeZero n
h : χ.conductor.lcm ψ.conductor ∣ n
⊢ χ * ψ = χ * (changeLevel ⋯) ψ.primitiveCharacter
Module: Mathlib.NumberTheory.DirichletCharacter.GaussSum

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
⊢ e.mulShift ↑(↑(↑u).val - 1) = 1

Tactic:
ha

Goal state after:
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
χ : DirichletCharacter R N
d : ℕ
hd : d ∣ N
he : e.mulShift ↑d = 1
u : (ZMod N)ˣ
hu : (ZMod.unitsMap hd) u = 1
a : ℤ
ha : ↑(↑u).val - 1 = ↑d * a
this : ↑u - 1 = ↑(↑(↑u).val - 1)
⊢ e.mulShift ↑(↑d * a) = 1
Module: Mathlib.Order.Grade

Goal state before:
pp: case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (n✝ + 1)) α
a : Fin (n✝ + 1)
h : IsMin a
⊢ IsMin ↑a

Tactic:
h.eq_bot,

Goal state after:
case succ
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : Preorder 𝕆
inst✝³ : Preorder ℙ
inst✝² : Preorder α
inst✝¹ : Preorder β
n✝ : ℕ
inst✝ : GradeMinOrder (Fin (n✝ + 1)) α
a : Fin (n✝ + 1)
h : IsMin a
⊢ IsMin ↑⊥
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ χ (↑p ^ n) ^ p * gaussSum χ ψ ^ p = χ (↑p ^ (n + 1)) * gaussSum χ ψ

Tactic:
hχ.gaussSum_frob _ hp,

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
n : ℕ
ih : gaussSum χ ψ ^ p ^ n = χ (↑p ^ n) * gaussSum χ ψ
⊢ χ (↑p ^ n) ^ p * (χ ↑p * gaussSum χ ψ) = χ (↑p ^ (n + 1)) * gaussSum χ ψ
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ auxDFT ((fun Φ k ↦ (↑N)⁻¹ • auxDFT Φ (-k)) Φ) = Φ

Tactic:
ext1 j
    simp only [← Pi.smul_def, auxDFT_smul, auxDFT_neg, auxDFT_auxDFT, neg_neg, ← mul_smul,
      inv_mul_cancel₀ (NeZero.ne _), one_smul]

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))

Tactic:
have hchar := Algebra.ringChar_eq F FF

Goal state after:
F : Type u_1
inst✝¹ : Fintype F
inst✝ : Field F
hF : ringChar F ≠ 2
hp2 : ∀ (n : ℕ), 2 ^ n ≠ 0
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
FF : Type u_1 := CyclotomicField 8 F
hchar : ringChar F = ringChar FF
⊢ 2 ^ (Fintype.card F / 2) = ↑(χ₈ ↑(Fintype.card F))
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ⊆ u ∧ u ⊂ t ↔ u ∈ image (fun x ↦ s ∪ x) (t \ s).ssubsets

Tactic:
mem_image,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ⊆ u ∧ u ⊂ t ↔ ∃ a ∈ (t \ s).ssubsets, s ∪ a = u