mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ↑(1 / r) * ∫ (x : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑x ^ (a - 1) * cexp (-↑x) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
ofReal_div,

Goal state after:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ↑1 / ↑r * ∫ (x : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑x ^ (a - 1) * cexp (-↑x) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_3
b : ℝ
hb : 0 < b
⊢ ↑((π / b) ^ (1 / 2) / 2) = ↑(π / b) ^ (1 / 2) / 2

Tactic:
ofReal_div,

Goal state after:
case e'_3
b : ℝ
hb : 0 < b
⊢ ↑((π / b) ^ (1 / 2)) / ↑2 = ↑(π / b) ^ (1 / 2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_3
⊢ ↑π ^ (1 / 2) = ↑π ^ ↑(1 / 2)

Tactic:
ofReal_div,

Goal state after:
case e'_3
⊢ ↑π ^ (1 / 2) = ↑π ^ (↑1 / ↑2)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2) * (π ^ (↑2 * (↑(finrank ℝ V) / 2)) * (‖x‖ ^ ↑2) ^ (↑(finrank ℝ V) / 2))

Tactic:
← rpow_mul (norm_nonneg _),

Goal state after:
case e_a
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
hf : Integrable f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ := fun w ↦ π ^ (↑(finrank ℝ V) / 2) * rexp (-π ^ 2 * ‖w‖ ^ 2)
A : Tendsto (fun w ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop
B :
  Tendsto
    (fun x ↦
      π ^ (-↑(finrank ℝ V) / 2) * ((fun x ↦ x ^ (↑(finrank ℝ V) / 2) * rexp (-1 * x)) ∘ fun w ↦ π ^ 2 * ‖w‖ ^ 2) x)
    (cobounded V) (𝓝 0)
x : V
⊢ ‖x‖ ^ ↑(finrank ℝ V) * π ^ (↑(finrank ℝ V) / 2) =
    π ^ (-↑(finrank ℝ V) / 2) * (π ^ (↑2 * (↑(finrank ℝ V) / 2)) * ‖x‖ ^ (↑2 * (↑(finrank ℝ V) / 2)))
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: case e_f
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ x : E
⊢ 𝐞 (-inner ℝ x ξ) • ∫ (y : E), (B (f₁ (x - y))) (f₂ y) = ∫ (y : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y)

Tactic:
Circle.smul_def,

Goal state after:
case e_f
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ x : E
⊢ ↑(𝐞 (-inner ℝ x ξ)) • ∫ (y : E), (B (f₁ (x - y))) (f₂ y) = ∫ (y : E), ↑(𝐞 (-inner ℝ x ξ)) • (B (f₁ (x - y))) (f₂ y)
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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ 𝐞 (-⟪v, w⟫) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w) = -(𝐞 (-(⟪v, w⟫ + 1 / 2)) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w))

Tactic:
Circle.smul_def,

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ ↑(𝐞 (-⟪v, w⟫)) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w) = -(↑(𝐞 (-(⟪v, w⟫ + 1 / 2))) • f (v + (1 / (2 * ‖w‖ ^ 2)) • w))
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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
⊢ cexp (2 * ↑π * -↑⟪v, w⟫ * I) * 1 = -(cexp (2 * ↑π * -↑⟪v, w⟫ * I) * cexp (2 * ↑π * -(1 / 2) * I) * 1)

Tactic:
have H : exp (- (π * I)) = (-1)⁻¹ := by rw [exp_neg, exp_pi_mul_I]

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
H : cexp (-(↑π * I)) = (-1)⁻¹
⊢ cexp (2 * ↑π * -↑⟪v, w⟫ * I) * 1 = -(cexp (2 * ↑π * -↑⟪v, w⟫ * I) * cexp (2 * ↑π * -(1 / 2) * I) * 1)
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: n : ℕ+
⊢ n.gcd 1 = 1

Tactic:
rw [gcd_comm]
  apply one_gcd

Goal state after:
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 x : ℝ
hx : max 0 (-2 * R) < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
rw [max_lt_iff] at hx

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 x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
n : ℕ
h : Squarefree n
⊢ |μ n| = 1

pp: case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0

Tactic:
· exact abs_moebius_eq_one_of_squarefree h

Goal state after:
case neg
n : ℕ
h : ¬Squarefree n
⊢ |μ n| = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + ((↑μ).pmul f) p) = ∑ d ∈ n.divisors, ↑(μ d) * f d

Tactic:
rw [(isMultiplicative_moebius.intCast.pmul hf).prodPrimeFactors_one_add_of_squarefree hn]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∑ d ∈ n.divisors, ((↑μ).pmul f) d = ∑ d ∈ n.divisors, ↑(μ d) * f d
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ↑ζ • f' = g'

Tactic:
rw [ArithmeticFunction.ext_iff]
    apply forall_congr'
    intro n
    cases n with
    | zero => simp
    | succ n =>
      rw [coe_zeta_smul_apply]
      simp only [forall_prop_of_true, succ_pos', f', g', coe_mk, succ_ne_zero, ite_false]
      rw [sum_congr rfl fun x hx => if_neg (pos_of_mem_divisors hx).ne']

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⁻¹
⊢ 2⁻¹ * ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))‖ < ε

Tactic:
inv_mul_eq_div,

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⁻¹
⊢ ‖∫ (v : V), 𝐞 (-⟪v, w⟫) • (f v - f (v + i w))‖ / 2 < ε
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[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ y + x ≤ x + r

Tactic:
by linarith [(hr hy).2]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (nthRoots n 1).card = (X ^ n - C 1).natDegree

Tactic:
IsPrimitiveRoot.card_nthRoots_one h,

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ n = (X ^ n - C 1).natDegree
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1

Tactic:
mem_primitiveRoots zero_lt_one,

Goal state after:
case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : IsPrimitiveRoot x 1
⊢ x = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Additive.ofMul ⟨(fun x ↦ ζ ^ x) 0, ⋯⟩ = 0

Tactic:
by simp only [zpow_zero]; rfl

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

Goal state before:
pp: case refine_3
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (X ^ n - 1)

Tactic:
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
      exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)

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
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
⊢ Tendsto (fun w ↦ ∫ (v : V), 𝐞 (-w v) • f v ∂μ.addHaarScalarFactor volume • volume) (cocompact (StrongDual ℝ V)) (𝓝 0)

Tactic:
simp_rw [integral_smul_nnreal_measure]

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
⊢ Tendsto (fun w ↦ μ.addHaarScalarFactor volume • ∫ (v : V), 𝐞 (-w v) • f v ∂volume) (cocompact (StrongDual ℝ V)) (𝓝 0)
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μ : (cyclotomic n K).IsRoot μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
key : i < n
⊢ False

Tactic:
have key' : i ∣ n := hio.trans hμn

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : (cyclotomic n K).IsRoot μ
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : (cyclotomic i K).IsRoot μ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case zero
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
⊢ cyclotomic (p ^ (0 + 1)) R = ∑ i ∈ range p, (X ^ p ^ 0) ^ i

Tactic:
have := Fact.mk hp; simp [cyclotomic_prime]

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

Goal state before:
pp: G : Type u_7
G' : Type u_8
inst✝³ : Group G
inst✝² : IsCyclic G
inst✝¹ : Finite G
inst✝ : CommGroup G'
hG' : ∃ ζ, IsPrimitiveRoot ζ (Nat.card G)
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
by
  let inst : Fintype G := Fintype.ofFinite _
  obtain ⟨ζ, hζ⟩ := hG'
  -- pick a generator `g` of `G`
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  have hζg : orderOf ζ ∣ orderOf g := by
    rw [← hζ.eq_orderOf, orderOf_eq_card_of_forall_mem_zpowers hg, Nat.card_eq_fintype_card]
  -- use the homomorphism `φ` given by `g ↦ ζ`
  let φ := monoidHomOfForallMemZpowers hg hζg
  have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by
    rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg]
  use φ
  contrapose ha
  specialize hg a
  rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg
  obtain ⟨k, hk⟩ := hg
  rw [← hk, map_pow] at ha
  obtain ⟨l, rfl⟩ := (hφg.pow_eq_one_iff_dvd k).mp ha
  rw [← hk, pow_mul, Nat.card_eq_fintype_card, pow_card_eq_one, one_pow]

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

Goal state before:
pp: case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
⊢ cyclotomic (n * p) ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)

Tactic:
have hprim := Complex.isPrimitiveRoot_exp _ hpos.ne.symm

Goal state after:
case inr.refine_1
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ cyclotomic (n * p) ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1.inl
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r n✝

pp: case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝

Tactic:
· obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'
      refine ⟨algebraMap B C b, ?_⟩
      exact hb.map_of_injective h

Goal state after:
case refine_1.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
n✝ : ℕ
hn' : n✝ ≠ 0
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r n✝
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 :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), eval 1 (cyclotomic (p ^ (x + 1)) ℤ)
⊢ False

Tactic:
eval_one_cyclotomic_prime_pow,

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 =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ range (padicValNat p n), ↑p
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (-1) ^ φ n = 1

Tactic:
exact (totient_even <| h1.lt_of_ne hn.symm).neg_one_pow

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

Goal state before:
pp: case refine_2.inl
S : Set ℕ
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
inst✝ : NeZero m
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ
hy : m * z ∈ S
hy' : m * z ≠ 0
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

Tactic:
exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩

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

Goal state before:
pp: 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
h : ζ.re ≤ 0 ∧ (-ζ).im = 0
⊢ False

Tactic:
Complex.neg_im,

Goal state after:
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
h : ζ.re ≤ 0 ∧ -ζ.im = 0
⊢ 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
x : CyclotomicField 0 K
⊢ x ∈ adjoin K {b | ∃ n ∈ {0}, n ≠ 0 ∧ b ^ n = 1}

Tactic:
have finrank : Module.finrank K (CyclotomicField 0 K) = 1 := by
      have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1
      let e : K ≃ₗ[K] (CyclotomicField 0 K) :=
        (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 0 K)).toLinearEquiv
      simp [← LinearEquiv.finrank_eq e, finrank_self]
    simp [Subalgebra.bot_eq_top_iff_finrank_eq_one.mpr finrank]

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

Goal state before:
pp: case refine_1
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}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ⟨y, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
refine subset_adjoin ?_
      simp only [mem_singleton_iff, exists_eq_left, mem_ofPred_eq]
      exact ⟨NeZero.ne n, by rwa [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
inst✝ : NeZero m
hm : n ∣ m
⊢ ((changeLevel hm) χ).conductor = χ.conductor

Tactic:
have : NeZero n := ⟨by aesop⟩
  have h : (changeLevel hm χ).conductor ∣ χ.conductor := by
    refine conductor_dvd_of_mem_conductorSet _
      ⟨χ.conductor_dvd_level.trans hm, χ.primitiveCharacter, ?_⟩
    rw [changeLevel_trans _ χ.conductor_dvd_level, changeLevel_primitiveCharacter]
  refine h.antisymm <| conductor_dvd_of_mem_conductorSet _
    ⟨h.trans χ.conductor_dvd_level, (changeLevel hm χ).primitiveCharacter, ?_⟩
  apply changeLevel_injective hm
  rw [← changeLevel_trans, changeLevel_primitiveCharacter]

Goal state after:
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ (∃ a, a ::ₘ s = t) → s ⋖ t

Tactic:
by rintro ⟨a, rfl⟩; exact covBy_cons _ _

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
⊢ d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))

Tactic:
induction n using Nat.case_strong_induction_on with
    | hz => simpa [u, ε_pos.le] using! hu 0
    | hi n IH =>
      have A : d (u (n + 1)) x ≤ 2 * ε := by
        rw [dist_comm]
        let r := range (n + 1) -- range (n+1) = {0, ..., n}
        calc
          d (u 0) (u (n + 1)) ≤ ∑ i ∈ r, d (u i) (u <| i + 1) := dist_le_range_sum_dist u (n + 1)
          _ ≤ ∑ i ∈ r, ε / 2 ^ i :=
            (sum_le_sum fun i i_in => (IH i <| Nat.lt_succ_iff.mp <| Finset.mem_range.mp i_in).1)
          _ = (∑ i ∈ r, (1 / 2 : ℝ) ^ i) * ε := by
            rw [Finset.sum_mul]
            simp
            field_simp
          _ ≤ 2 * ε := by gcongr; apply sum_geometric_two_le
      have B : 2 ^ (n + 1) * ϕ x ≤ ϕ (u (n + 1)) := by
        refine @geom_le (ϕ ∘ u) _ zero_le_two (n + 1) fun m hm => ?_
        exact (IH _ <| Nat.lt_add_one_iff.1 hm).2.le
      exact hu (n + 1) ⟨A, B⟩

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
⊢ 0 ≤ 1 - k * p

Tactic:
linarith only [hp]

Goal state after: