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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'

Tactic:
pow_mul,

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup D
inst✝¹ : NormedSpace ℝ D
inst✝ : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F)) f
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * ((1 + ‖g x‖) ^ kg) ^ (k + l * n)
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case h't
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
hg : Integrable g μ
h'g : ContinuousAt g 0
I : Integrable φ μ
⊢ μ (closedBall 0 1) ≠ ∞

Tactic:
exact (isCompact_closedBall 0 1).measure_ne_top

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : IsTopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous[inst✝⁴, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ (L p.1) p.2
f g : V → E
hf : Integrable f μ
hg : Integrable g μ
⊢ fourierIntegral e μ L (f + g) = fourierIntegral e μ L f + fourierIntegral e μ L g

Tactic:
ext1 w
  dsimp only [Pi.add_apply, fourierIntegral]
  simp_rw [smul_add]
  rw [integral_add]
  · exact (fourierIntegral_convergent_iff he hL w).2 hf
  · exact (fourierIntegral_convergent_iff he hL w).2 hg

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

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x, -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L)
      (fun x ↦ ((fderiv ℝ (iteratedFDeriv ℝ n f) x) (m 0)) (Fin.tail m)) w =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ i, -(L (m i)) w) • fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w

Tactic:
rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)),
          ← fourierIntegral_continuousLinearMap_apply' J]

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (iteratedFDeriv ℝ n f) = fun w ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x, -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ ((fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ i, -(L (m i)) w) • fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L) f w
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s t : ℝ
ht : 0 < t
⊢ IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume ↔ s < -1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_of_lt h ht⟩
  contrapose! h
  intro H
  have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) :=
    H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl
  have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
    have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
    rw [← Real.rpow_neg_one x]
    exact Real.rpow_le_rpow_of_exponent_le x_one h
  exact not_integrableOn_Ioi_inv this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a ↦ ‖s * (↑(rexp (-a)) * ↑a ^ (s - 1))‖) (volume.restrict (Ioc 0 Y))

Tactic:
simp_rw [norm_mul]

Goal state after:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ HasFiniteIntegral (fun a ↦ ‖s‖ * (‖↑(rexp (-a))‖ * ‖↑a ^ (s - 1)‖)) (volume.restrict (Ioc 0 Y))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 Y → rexp (-x) * x ^ (s.re - 1) = ‖↑(rexp (-x))‖ * ‖↑x ^ (s - 1)‖

pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
· filter_upwards with x hx
    rw [Complex.norm_of_nonneg (exp_pos _).le, norm_cpow_eq_rpow_re_of_pos hx.1]
    simp

Goal state after:
case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      f 0 (Fin.cons x.1 (fun j ↦ cast ⋯ (x.2 j)) 0) *
        ∏ x_1,
          f x_1.succ
            (Fin.cons x.1 (fun j ↦ cast ⋯ (x.2 j)) x_1.succ) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)

Tactic:
Fin.cons_succ,

Goal state after:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
n : ℕ
n_ih :
  ∀ {E : Fin n → Type u_3} {mE : (i : Fin n) → MeasurableSpace (E i)} {μ : (i : Fin n) → Measure (E i)}
    [∀ (i : Fin n), SigmaFinite (μ i)] (f : (i : Fin n) → E i → 𝕜),
    ∫ (x : (i : Fin n) → E i), ∏ i, f i (x i) ∂Measure.pi μ = ∏ i, ∫ (x : E i), f i x ∂μ i
E : Fin (n + 1) → Type u_3
mE : (i : Fin (n + 1)) → MeasurableSpace (E i)
μ : (i : Fin (n + 1)) → Measure (E i)
inst✝ : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
f : (i : Fin (n + 1)) → E i → 𝕜
⊢ ∫ (x : E 0 × ((j : Fin n) → E (Fin.succAbove 0 j))),
      f 0 (Fin.cons x.1 (fun j ↦ cast ⋯ (x.2 j)) 0) *
        ∏ x_1, f x_1.succ (cast ⋯ (x.2 x_1)) ∂(μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)) =
    ∫ (x : E 0 × ((i : Fin n) → E i.succ)), f 0 x.1 * ∏ i, f i.succ (x.2 i) ∂(μ 0).prod (Measure.pi fun i ↦ μ i.succ)
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i ↦ polarCoord.source) =ᵐ[Measure.pi fun x ↦ volume] Set.univ

Tactic:
← Set.pi_univ

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
⊢ (Set.univ.pi fun i ↦ polarCoord.source) =ᵐ[Measure.pi fun x ↦ volume] Set.pi ?m.45 fun i ↦ Set.univ

ι : Type u_1
inst✝ : Fintype ι
⊢ Set ι
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case e_f.e_a.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
h'f : Integrable (𝓕 f) volume
v : V
A : Tendsto (fun c ↦ ∫ (w : V), cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫) • 𝓕 f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
B :
  Tendsto (fun c ↦ ∫ (w : V), 𝓕 (fun w ↦ cexp (-↑c⁻¹ * ↑‖w‖ ^ 2 + 2 * ↑π * I * ↑⟪v, w⟫)) w • f w) atTop (𝓝 (𝓕⁻ (𝓕 f) v))
c : ℝ
hc : 0 < c
w : V
⊢ -↑π ^ 2 * ↑‖v - w‖ ^ 2 / ↑c⁻¹ = -↑π ^ 2 * ↑c * ↑‖v - w‖ ^ 2

Tactic:
· simp; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ s = -↑(1 + m)

Tactic:
rw [hs]

Goal state after:
case hs
n✝ : ℕ
n_ih : ∀ {s : ℝ}, (∀ (m : ℕ), s ≠ -↑m) → -↑n✝ < s → Gamma s ≠ 0
s : ℝ
hs' : -↑(n✝ + 1) < s
m : ℕ
hs : s = -↑m - 1
⊢ -↑m - 1 = -↑(1 + m)
Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he✝ : Continuous ⇑e
hL✝ : Continuous fun p ↦ (L p.1) p.2
he : Continuous ⇑e
hL : Continuous fun p ↦ (L p.1) p.2
w : W
⊢ ∃ C, ∀ (x y : V), dist ↑(e ((L x) w)) ↑(e ((L y) w)) ≤ C

Tactic:
refine ⟨2, fun x y ↦ ?_⟩
    calc dist _ _
      ≤ (‖_‖ : ℝ) + ‖_‖ := dist_le_norm_add_norm _ _
    _ ≤ 1 + 1 := add_le_add (by simp) (by simp)
    _ = 2 := by ring

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ MemSobolev s p 0

Tactic:
by
  use 0
  rw [← Lp.toTemperedDistributionCLM_apply]
  simp only [map_zero]

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

Goal state before:
pp: 𝕜 : 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
ξ : E
⊢ ∫ (x : E), 𝐞 (-inner ℝ x ξ) • ∫ (y : E), (B (f₁ (x - y))) (f₂ y) =
    ∫ (x : E) (y : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y)

Tactic:
by
    congr
    ext x
    simp_rw [Circle.smul_def, integral_smul]

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

Goal state before:
pp: p m : ℕ+
pp : p.Prime
⊢ ↑m ∣ ↑p ↔ m = 1 ∨ m = p

Tactic:
Nat.dvd_prime pp

Goal state after:
p m : ℕ+
pp : p.Prime
⊢ ↑m = 1 ∨ ↑m = ↑p ↔ m = 1 ∨ m = p
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: n : ℕ
⊢ μ n = 0 ∨ μ n = 1 ∨ μ n = -1

Tactic:
simp only [moebius, coe_mk]

Goal state after:
n : ℕ
⊢ (if Squarefree n then (-1) ^ cardFactors n else 0) = 0 ∨
    (if Squarefree n then (-1) ^ cardFactors n else 0) = 1 ∨ (if Squarefree n then (-1) ^ cardFactors n else 0) = -1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: l : ℕ
hl : Squarefree l
⊢ (-1) ^ (2 * cardFactors l) = 1

Tactic:
pow_mul,

Goal state after:
l : ℕ
hl : Squarefree l
⊢ ((-1) ^ 2) ^ cardFactors l = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
rw [sum_eq_iff_sum_smul_moebius_eq]

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
⊢ (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
⊢ (∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
refine
      Iff.trans
        (Iff.trans (forall_congr' fun n => ?_)
          (@prod_eq_iff_prod_pow_moebius_eq_on Rˣ _
            (fun n => if h : 0 < n then Units.mk0 (f n) (hf n h) else 1)
            (fun n => if h : 0 < n then Units.mk0 (g n) (hg n h) else 1)
            s hs))
        (forall_congr' fun n => ?_) <;>
    refine imp_congr_right fun hn => ?_
  · rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors hx), Units.coeHom_apply, Units.val_mk0]
  · rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)),
      Units.coeHom_apply, Units.val_zpow_eq_zpow_val, Units.val_mk0]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ ζ ^ (k * i) = 1

Tactic:
pow_mul,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
⊢ (ζ ^ k) ^ i = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ ζ ^ (k * a) = 1

Tactic:
pow_mul,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i a : ℕ
hi : IsPrimitiveRoot (ζ ^ (i.gcd k * a)) k
ha : i = i.gcd k * a
b : ℕ
hb : k = b * i.gcd k
⊢ (ζ ^ k) ^ a = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1

Tactic:
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
    simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
      Polynomial.map_X] using Polynomial.map_dvd (Int.castRingHom R) this
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
  exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')

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

Goal state before:
pp: case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ ζ ^ (n * m) * a = a

Tactic:
pow_mul,

Goal state after:
case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ (ζ ^ n) ^ m * a = a
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 * volume.real A < 2 * ε

Tactic:
rw [div_mul_eq_mul_div, div_lt_iff₀ (NNReal.coe_pos.mpr hB_pos), mul_comm (2 : ℝ), mul_assoc,
    mul_lt_mul_iff_right₀ hε]

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)‖
⊢ volume.real A < 2 * ↑B
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2

Tactic:
refine le_trans ?_ hfg

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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ ≤ ∫ (x : V), ‖f x - g x‖
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
⊢ (IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)) →
    IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))

Tactic:
hind

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
⊢ IsPrimitiveRoot μ n✝ → (p * a).Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ x ^ (a * d) = 1

Tactic:
pow_mul,

Goal state after:
case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : n = a * d
hazero : 0 < a
⊢ (x ^ a) ^ d = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
⊢ nthRootsFinset n 1 = n.divisors.biUnion fun i ↦ primitiveRoots i R

Tactic:
ext x
  suffices x ^ n = 1 ↔ ∃ a, a ∣ n ∧ x ∈ primitiveRoots a R by
    simpa [Polynomial.mem_nthRootsFinset (NeZero.pos n), (NeZero.ne n)]
  constructor
  · intro H
    obtain ⟨k, hk, hx⟩ := exists_pos H (NeZero.ne n)
    exact ⟨k, hx.2 _ H, (mem_primitiveRoots hk).mpr hx⟩
  · rintro ⟨a, ⟨d, hd⟩, ha⟩
    have hazero : 0 < a := Nat.pos_of_ne_zero fun ha₀ ↦ by simp_all
    rw [mem_primitiveRoots hazero] at ha
    rw [hd, pow_mul, ha.pow_eq_one, one_pow]

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'
a : G
ha : a ≠ 1
inst : Fintype G := Fintype.ofFinite G
ζ : G'
hζ : IsPrimitiveRoot ζ (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
hζg : orderOf ζ ∣ orderOf g
⊢ ∃ φ, φ a ≠ 1

Tactic:
let φ := monoidHomOfForallMemZpowers hg hζg

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