mathlib-initiative/mathlib-tactics huggingface dataset:
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
bdA2 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ (↑B).toReal < 2 * ↑B

Tactic:
rw [ENNReal.coe_toReal, two_mul]

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 : ∫ (v : V) in A, ‖f v - f (v + i w)‖ ≤ ε / ↑B * volume.real A
this : ‖∫ (v : V) in A, ‖f v - f (v + i w)‖‖ = ∫ (v : V) in A, ‖f v - f (v + i w)‖
⊢ ↑B < ↑B + ↑B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ

Tactic:
← mem_nthRoots h,

Goal state after:
n : ℕ
h : 0 < n
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
⊢ ζ ∈ nthRoots n 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).IsRoot ζ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
hn : Squarefree (X ^ n - 1)
⊢ False

Tactic:
rw [← this, Squarefree] at hn

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
hn : ∀ (x : K[X]), x * x ∣ (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) → IsUnit x
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : 0 = m.totient
⊢ 0 = m

Tactic:
eq_comm,

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : m.totient = 0
⊢ 0 = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
m : ℕ
hnm : natDegree 1 = (cyclotomic m R).natDegree
⊢ 0 = m

Tactic:
rwa [natDegree_one, natDegree_cyclotomic, eq_comm, Nat.totient_eq_zero, eq_comm] at hnm

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

Goal state before:
pp: 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
i : Fin p
⊢ α i = P.coeff ↑i

Tactic:
simp [P, ← Fin.ext_iff]

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

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : ¬p ∣ n
R : Type u_1
inst✝ : CommRing R
hnpos : n > 0
this : NeZero n
⊢ ((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ * cyclotomic n ℤ).natDegree

Tactic:
rw [natDegree_expand, natDegree_cyclotomic,
      natDegree_mul (cyclotomic_ne_zero _ ℤ) (cyclotomic_ne_zero _ ℤ), natDegree_cyclotomic,
      natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul ((Nat.Prime.coprime_iff_not_dvd hp).2 hdiv), Nat.totient_prime hp,
      mul_comm (p - 1), ← Nat.mul_succ, Nat.sub_one, Nat.succ_pred_eq_of_pos hp.pos]

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

Goal state before:
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)

Tactic:
eq_comm,

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 : ∑ 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
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ (IsPrimitiveRoot.powerBasis K hζ).gen ∈ K[ζ - 1]

Tactic:
powerBasis_gen,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ ζ ∈ K[ζ - 1]
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ p ^ a.succ * m = p * p ^ a * m

Tactic:
pow_succ'

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
⊢ p * p ^ a * m = p * p ^ a * m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ eval 1 (cyclotomic n ℤ) = 1 ∨ eval 1 (cyclotomic n ℤ) = -1

Tactic:
rw [← Int.natAbs_eq_natAbs_iff, Int.natAbs_one, Nat.eq_one_iff_not_exists_prime_dvd]

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
⊢ ∀ (p : ℕ), Nat.Prime p → ¬p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : ∏ j ∈ n.divisors.erase 1, eval 1 (cyclotomic j ℤ) = ↑n
⊢ False

Tactic:
eq_comm,

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : ↑n = ∏ j ∈ n.divisors.erase 1, eval 1 (cyclotomic j ℤ)
⊢ False
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
⊢ ¬0 = ζ.arg

Tactic:
eq_comm,

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
⊢ ¬ζ.arg = 0
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
hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯
⊢ (q - 1) ^ φ n < eval q (cyclotomic n ℝ)

Tactic:
by
    simp only [← Units.val_lt_val, Units.val_pow_eq_pow_val, Units.val_mk0, ← NNReal.coe_lt_coe,
      hq'.le, coe_nnnorm, NNReal.coe_pow, Real.coe_toNNReal', sub_nonneg, sup_of_le_left] at this
    convert! this
    rw [eq_comm]
    simp [cyclotomic_nonneg n hq'.le]

Goal state after:
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
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
⊢ ∃ r, IsPrimitiveRoot r n

Tactic:
obtain ⟨r, hr1, hr2⟩ := h n hn1 hn2
    exact ⟨⟨r, subset_adjoin ⟨n, hn1, hn2, hr1⟩⟩, Subtype.val_injective hr1,
      fun l hl ↦ hr2 l congr($hl.1)⟩

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

Goal state before:
pp: case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ q + 1 = max (q + 1) 0

Tactic:
eq_comm,

Goal state after:
case e'_4
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
hex : ∃ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ < q + 1
this✝ : ¬eval (↑q) (cyclotomic n ℂ) = 0
this : ‖eval (↑q) (cyclotomic n ℂ)‖ < max (q + 1) 0 ^ φ n
⊢ max (q + 1) 0 = q + 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B

Tactic:
rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂

Goal state after:
case pos
S✝ : Set ℕ
n : ℕ
S : Set ℕ
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension S A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ ↑(adjoin A ((cyclotomic n A).rootSet B))

Tactic:
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2

Goal state after:
case refine_2
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : IsDomain B
ζ : B
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left✝ : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ ↑(adjoin A ((cyclotomic n A).rootSet B))
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 = ↑d * (↑a₀ * p + ↑N₀ * q)
⊢ IsCoprime ↑a₀ ↑N₀

Tactic:
eq_comm,

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 * (↑a₀ * p + ↑N₀ * q) = ↑d
⊢ IsCoprime ↑a₀ ↑N₀
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 : (↑u).val.Coprime m
⊢ IsCoprime (↑m) n

Tactic:
rw [hu, Nat.coprime_iff_gcd_eq_one, ← Int.gcd_natCast_natCast,
      val_intCast, Int.gcd_emod] at h_coprime

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: 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:
rw [← Subgroup.orderOf_mk]
      exact Monoid.order_dvd_exponent ζ'

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
⊢ Finite (G →* Mˣ)

Tactic:
let S := rootsOfUnity (Monoid.exponent G) M

Goal state after:
G : Type u_1
M : Type u_2
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : CommMonoid M
inst✝ : HasEnoughRootsOfUnity M (Monoid.exponent G)
S : Subgroup Mˣ := rootsOfUnity (Monoid.exponent G) M
⊢ Finite (G →* Mˣ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((cyclotomic n K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
let := Classical.decEq L

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ adjoin K ((cyclotomic n K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
y : (ZMod n)ˣ
⊢ a₁✝ ↑y = a₂✝ ↑y

Tactic:
obtain ⟨z, rfl⟩ := ZMod.unitsMap_surjective hm y

Goal state after:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)
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
ζ : Rˣ
hζ₁ : ζ ∈ rootsOfUnity n R
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ ℤ[μ]

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁

Goal state after:
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
ζ : Rˣ
hζ₁ : ↑ζ ^ n = ↑1
hζ₂ : ↑ζ = χ a
⊢ χ a ∈ ℤ[μ]
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑↑p = 1
⊢ ((changeLevel ⋯) ψ).primitiveCharacter ↑↑p = 1

Tactic:
rw [primitiveCharacter_changeLevel_apply, primitiveCharacter_apply_of_isCoprime, hψ]

Goal state after:
case refine_1.ha
R : Type u_1
inst✝² : CommMonoidWithZero R
n : ℕ
inst✝¹ : NeZero n
inst✝ : Nontrivial R
p : ℕ
hp : Fact (Nat.Prime p)
this : NeZero (n / p ^ n.factorization p)
hcop : p.Coprime (n / p ^ n.factorization p)
ψ : DirichletCharacter R (n / p ^ n.factorization p)
hψ : ψ ↑↑p = 1
⊢ IsCoprime ↑p ↑(n / p ^ n.factorization p)
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 : ↑↑(↑u).val = ↑1
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1

Tactic:
eq_comm,

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 : ↑1 = ↑↑(↑u).val
this : (ZMod.castHom hd (ZMod d)) ↑u = ↑↑(↑u).val
⊢ ↑d ∣ ↑(↑u).val - 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ x, ∑ c, χ c * ψ (x * (c - 1)) = ↑(Fintype.card R)

Tactic:
Finset.sum_comm

Goal state after:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ ∑ y, ∑ x, χ y * ψ (x * (y - 1)) = ↑(Fintype.card R)
Module: Mathlib.Analysis.InnerProductSpace.NormPow

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖fderiv ℝ (fun x ↦ ‖f x‖ ^ p) x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖

Tactic:
rw [hf.fderiv_norm_rpow hp, norm_smul, norm_mul]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : F → E
hf : Differentiable ℝ f
x : F
p : ℝ
hp : 1 < p
⊢ ‖p‖ * ‖‖f x‖ ^ (p - 2)‖ * ‖(innerSL ℝ) (f x) ∘SL fderiv ℝ f x‖ ≤ p * ‖f x‖ ^ (p - 1) * ‖fderiv ℝ f x‖
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : 0 = χ (-1) * ↑(Fintype.card R)
hf : gaussSum χ ψ = 0
⊢ False

Tactic:
eq_comm,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : χ (-1) * ↑(Fintype.card R) = 0
hf : gaussSum χ ψ = 0
⊢ False
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(LocallyFiniteOrder.finsetIcc s t) = 2 ^ (#t - #s)

Tactic:
simp [h, card_sdiff_of_subset]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b : P
v : V
⊢ ⟪a -ᵥ b, v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b : P
v : V
⊢ ⟪-(b -ᵥ a), v⟫_𝕜 = 0 ↔ ⟪b -ᵥ a, v⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Affine

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
a b : P
⊢ ⟪v, a -ᵥ b⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0

Tactic:
← neg_vsub_eq_vsub_rev,

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
a b : P
⊢ ⟪v, -(b -ᵥ a)⟫_𝕜 = 0 ↔ ⟪v, b -ᵥ a⟫_𝕜 = 0
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case e'_2
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
FFp : Nat.Prime (ringChar FF)
this : Fact (Nat.Prime (ringChar FF))
hFF : ringChar FF ≠ 2
hu : IsUnit ↑(ringChar FF)
ψ₈ : PrimitiveAddChar (ZMod ↑8) F := primitiveZModChar 8 F ⋯
ψ₈char : AddChar (ZMod 8) FF := ψ₈.char
τ : FF := ψ₈char 1
τ_spec : τ ^ 4 = -1
χ : MulChar (ZMod 8) FF := χ₈.ringHomComp (Int.castRingHom FF)
hχ : χ (-1) = 1
hq : χ.IsQuadratic
h₁ : (fun a ↦ ↑(χ₈ a) * τ ^ ↑a) = fun a ↦ χ a * ψ₈char a
hg₁ : gaussSum χ ψ₈char = 2 * (τ - τ ^ 3)
hg : gaussSum χ ψ₈char ^ 2 = χ (-1) * ↑(Fintype.card (ZMod 8))
h : ↑8 ^ (Fintype.card F / 2) = χ ↑(Fintype.card F)
⊢ 2 ^ (Fintype.card F / 2) = 8 ^ (Fintype.card F / 2)

Tactic:
rw [(by norm_num : (8 : F) = 2 ^ 2 * 2), mul_pow,
      (FiniteField.isSquare_iff hF <| hp2 2).mp ⟨2, pow_two 2⟩, one_mul]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ ↑(assocIsometry 𝕜 E E E).symm.symm.toLinearEquiv ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)

Tactic:
← adjoint_toLinearMap_eq_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint ↑(assocIsometry 𝕜 E E E).symm.toLinearEquiv ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1))) =
    ↑(lidIsometry 𝕜 E).symm.toLinearEquiv

Tactic:
← adjoint_toLinearMap_eq_symm

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ adjoint ((↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) ∘ₗ LinearMap.rTensor E (toSpanSingleton 𝕜 E (e.symm 1))) =
    adjoint ↑(lidIsometry 𝕜 E).toLinearEquiv