mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case empty
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ι : Type u_2
f : ι → AddCircle T → E
hf : ∀ i ∈ ∅, Integrable (f i) haarAddCircle
x✝ : ℤ
⊢ fourierCoeff (∑ i ∈ ∅, f i) x✝ = (∑ i ∈ ∅, fourierCoeff (f i)) x✝

Tactic:
simp [fourierCoeff]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: case hcg
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : BorelSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst✝ : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : μ t ≠ ∞
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst✝⁴] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (fun i ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := ⋯
⊢ (fun x ↦ a) =ᶠ[𝓝[s] x₀] t.indicator fun x ↦ a

Tactic:
filter_upwards [h'ts] with x hx using by simp [hx]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * ‖iteratedDeriv n (⇑f) x‖ ≤ M
⊢ (SchwartzMap.seminorm 𝕜 k n) f ≤ M

Tactic:
refine seminorm_le_bound 𝕜 k n f hMp ?_
  simpa only [Real.norm_eq_abs, norm_iteratedFDeriv_eq_norm_iteratedDeriv]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    (∑ x ∈ Finset.range (m.1 + 1), ↑(m.1.choose x)) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f

Tactic:
Finset.sum_mul

Goal state after:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤
    ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m ↦ SchwartzMap.seminorm 𝕜 m.1 m.2) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case hbc
ι : 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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
⊢ ∑ i ∈ Finset.range (n + 1), ‖x‖ ^ k * (↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖) ≤
    (∑ _x ∈ Finset.range (n + 1), 1) *
      (↑(n.choose (n / 2)) * C * 2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f)

Tactic:
Finset.sum_mul

Goal state after:
case hbc
ι : 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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
⊢ ∑ i ∈ Finset.range (n + 1), ‖x‖ ^ k * (↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖) ≤
    ∑ i ∈ Finset.range (n + 1),
      1 * (↑(n.choose (n / 2)) * C * 2 ^ (l + k) * ((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E)) f)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
x : E
⊢ ((smulLeftCLM F (g₁ + g₂)) f) x = ((smulLeftCLM F g₁ + smulLeftCLM F g₂) f) x

Tactic:
simp [hg₁, hg₂, hg₁.add hg₂, add_smul]

Goal state after:
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAlgebra ℝ 𝕜
inst✝ : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
⊢ smulLeftCLM F (-g) = -smulLeftCLM F g

Tactic:
ext f x
  simp [hg, hg.neg, neg_smul]

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✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (v : V), ↑(e (-(L (v + v₀ - v₀)) w)) • f (v + v₀) ∂μ = ↑(e ((L v₀) w)) • ∫ (v : V), ↑(e (-(L v) w)) • f v ∂μ

Tactic:
rw [integral_add_right_eq_self fun v : V ↦ (e (-L (v - v₀) w) : ℂ) • f v, ← integral_smul]

Goal state after:
𝕜 : 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✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (x : V), ↑(e (-(L (x - v₀)) w)) • f x ∂μ = ∫ (a : V), ↑(e ((L v₀) w)) • ↑(e (-(L a) w)) • f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Asymptotics

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ IntegrableOn (fun i ↦ f (i, x)) s μ

Tactic:
have : IsFiniteMeasure (μ.restrict s) := ⟨Measure.restrict_apply_univ s ▸ hμ⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst✝¹ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝ : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ IntegrableOn (fun i ↦ f (i, x)) s μ
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
hf : Integrable f volume
hf' : Integrable (fun x ↦ x • f x) volume
w : ℝ
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume

Tactic:
simpa only [norm_smul] using! hf'.norm

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn (fun x ↦ x ^ s * rexp (-b * x ^ 2)) (Iio 0) volume

Tactic:
← (Measure.measurePreserving_neg (volume : Measure ℝ)).integrableOn_comp_preimage
      (Homeomorph.neg ℝ).measurableEmbedding

Goal state after:
b : ℝ
hb : 0 < b
s : ℝ
hs : -1 < s
⊢ IntegrableOn ((fun x ↦ x ^ s * rexp (-b * x ^ 2)) ∘ Neg.neg) (Neg.neg ⁻¹' Iio 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < (s + 1).re

Tactic:
add_re,

Goal state after:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ 0 < s.re + re 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s + 1).re < ↑n

Tactic:
add_re,

Goal state after:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s.re + re 1) < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s + 1).re < ↑n

Tactic:
add_re,

Goal state after:
s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s.re + re 1) < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
⊢ Gamma (s + 1) = s * Gamma s

Tactic:
have t1 : -s.re < n := by simpa only [sub_sub_cancel_left] using Nat.sub_one_lt_floor (1 - s.re)

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ Gamma (s + 1) = s * Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s + 1).re < ↑n

Tactic:
add_re,

Goal state after:
s : ℂ
h2 : s ≠ 0
n : ℕ := ⌊1 - s.re⌋₊
t1 : -s.re < ↑n
⊢ -(s.re + re 1) < ↑n
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)
x : ℝ
hx : 0 < x
⊢ ↑x ^ (a - 1) * cexp (-(↑r * ↑x)) = ↑(r⁻¹ * r) ^ (a - 1) * ↑x ^ (a - 1) * cexp (-(↑r * ↑x))

Tactic:
inv_mul_cancel₀ hr.ne',

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ rexp (-(b.re * x ^ 2))) volume

Tactic:
simp_rw [← neg_mul]

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
⊢ Integrable (fun x ↦ rexp (-b.re * x ^ 2)) volume
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
s : Set α
h : IsVanishingOn f s
s_open : IsOpen[inst✝²] s
⊢ s ⊆ (dsupport f)ᶜ

Tactic:
dsupport_compl_eq

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_6
V : Type u_10
inst✝³ : FunLike F α β
inst✝² : TopologicalSpace α
inst✝¹ : Zero β
inst✝ : Zero V
f : F → V
s : Set α
h : IsVanishingOn f s
s_open : IsOpen[inst✝²] s
⊢ s ⊆ ⋃₀ {a | IsVanishingOn f a ∧ IsOpen[inst✝²] a}
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d✝ : Type u_1
inst✝¹ : Fintype d✝
d : Type u_2
inst✝ : Fintype d
⊢ ∀ {a : C(UnitAddTorus d, ℂ)}, a ∈ (adjoin ℂ (range mFourier)).carrier → star a ∈ (adjoin ℂ (range mFourier)).carrier

Tactic:
change Algebra.adjoin ℂ (range mFourier) ≤ star (Algebra.adjoin ℂ (range mFourier))

Goal state after:
d✝ : Type u_1
inst✝¹ : Fintype d✝
d : Type u_2
inst✝ : Fintype d
⊢ adjoin ℂ (range mFourier) ≤ star (adjoin ℂ (range mFourier))
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
⊢ False

Tactic:
have h₀ := congr_fun ((complexBasis α).sum_repr f) 0

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
h₀ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case prime_pow
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ (μ * ↑ζ) (p ^ n) = 1 (p ^ n)

Tactic:
coe_mul_zeta_apply,

Goal state after:
case prime_pow
p n : ℕ
hp : Nat.Prime p
hn : 0 < n
⊢ ∑ i ∈ (p ^ n).divisors, μ i = 1 (p ^ n)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case inr
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
this : ∀ ⦃i j : ℕ⦄, i < k → j < k → ζ ^ i = ζ ^ j → i ≤ j → i = j
hij : ¬i ≤ j
⊢ i = j

Tactic:
exact (this hj hi H.symm (le_of_not_ge hij)).symm

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ cyclotomic' 2 R = X + 1

Tactic:
rw [cyclotomic']

Goal state after:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ ∈ primitiveRoots 2 R, (X - C μ) = X + 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (cyclotomic' n R).natDegree = n.totient

Tactic:
rw [cyclotomic']

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (cyclotomic' n R).roots = (primitiveRoots n R).val

Tactic:
rw [cyclotomic']

Goal state after:
n : ℕ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot (f ζ) k
hf : Injective ⇑f
⊢ ζ ^ k = 1

Tactic:
apply_fun f; rw [map_pow, map_one, h.pow_eq_one]

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

Goal state before:
pp: case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

pp: case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
· use 1
    simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]

Goal state after:
case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i ∈ range p, X ^ i

Tactic:
rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
    erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]

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

Goal state before:
pp: case inr
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ (algebraMap R[X] (RatFunc R)) (cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal, (algebraMap R[X] (RatFunc R)) (X ^ i.2 - 1) ^ μ i.1

Tactic:
rw [(prod_eq_iff_prod_pow_moebius_eq_of_nonzero (fun n hn => _) fun n hn => _).1 h n hpos]

Goal state after:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → (algebraMap R[X] (RatFunc R)) (cyclotomic n R) ≠ 0

n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hpos : n > 0
h :
  ∀ (n : ℕ),
    0 < n → ∏ i ∈ n.divisors, (algebraMap R[X] (RatFunc R)) (cyclotomic i R) = (algebraMap R[X] (RatFunc R)) (X ^ n - 1)
⊢ ∀ (n : ℕ), 0 < n → (algebraMap R[X] (RatFunc R)) (X ^ n - 1) ≠ 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ eval ζ (∏ i ∈ n.divisors, cyclotomic i R) = 0

Tactic:
apply eval_eq_zero_of_dvd_of_eval_eq_zero _ h

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
ζ : R
i : ℕ
hi : i ∈ n.divisors
h : (cyclotomic i R).IsRoot ζ
hn : n > 0
this : ζ ^ n - 1 = eval ζ (∏ i ∈ n.divisors, cyclotomic i R)
⊢ cyclotomic i R ∣ ∏ i ∈ n.divisors, cyclotomic i R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
this : ∀ b ∈ ↑(nthRootsFinset n 1), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n 1)), b = (algebraMap R K) a
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)

Tactic:
obtain ⟨x, hx, hx1⟩ := this _ ha

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ζ : R
n : ℕ
x✝ y : R
inst✝ : IsDomain R
hpos : 0 < n
h : IsPrimitiveRoot ζ n
K : Type u_1 := FractionRing R
h' : IsPrimitiveRoot ((algebraMap R K) ζ) n
a : K
ha : a ∈ ↑(nthRootsFinset n 1)
this : ∀ b ∈ ↑(nthRootsFinset n 1), ∃ a, ∃ (_ : a ∈ ↑(nthRootsFinset n 1)), b = (algebraMap R K) a
x : R
hx : x ∈ ↑(nthRootsFinset n 1)
hx1 : a = (algebraMap R K) x
⊢ a ∈ ⇑(algebraMap R K) '' ↑(nthRootsFinset n 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case h.inl.hb.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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hk : Odd n
⊢ 0 ≤ eval x (cyclotomic i R)

pp: case h.inl.hb.inr
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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)

Tactic:
· refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl
      · exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
      · exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk

Goal state after:
case h.inl.hb.inr
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
i : ℕ
hi : i ≠ 1 ∧ i ∣ n ∧ i < n
hx : 0 < x + 1
⊢ 0 ≤ eval x (cyclotomic i R)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ 0 < eval x (cyclotomic n R)

Tactic:
induction n using Nat.strong_induction_on with | _ n ih
  have hn' : 0 < n := pos_of_gt hn
  have hn'' : 1 < n := one_lt_two.trans hn
  have := prod_cyclotomic_eq_geom_sum hn' R
  apply_fun eval x at this
  rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons,
    eval_mul, eval_geom_sum] at this
  rcases lt_trichotomy 0 (∑ i ∈ Finset.range n, x ^ i) with (h | h | h)
  · apply pos_of_mul_pos_left
    · rwa [this]
    rw [eval_prod]
    refine Finset.prod_nonneg fun i hi => ?_
    simp only [Finset.mem_erase, mem_properDivisors] at hi
    rw [geom_sum_pos_iff hn'.ne'] at h
    rcases h with hk | hx
    · refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 ?_)).le <;> rintro rfl
      · exact hn'.ne' (zero_dvd_iff.mp hi.2.1)
      · exact not_odd_iff_even.2 (even_iff_two_dvd.mpr hi.2.1) hk
    · rcases eq_or_ne i 2 with (rfl | hk)
      · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using hx.le
      refine (ih _ hi.2.2 (Nat.two_lt_of_ne ?_ hi.1 hk)).le
      rintro rfl
      exact hn'.ne' <| zero_dvd_iff.mp hi.2.1
  · rw [eq_comm, geom_sum_eq_zero_iff_neg_one hn'.ne'] at h
    exact h.1.symm ▸ cyclotomic_neg_one_pos hn
  · apply pos_of_mul_neg_left
    · rwa [this]
    rw [geom_sum_neg_iff hn'.ne'] at h
    have h2 : 2 ∈ n.properDivisors.erase 1 := by
      rw [Finset.mem_erase, mem_properDivisors]
      exact ⟨by decide, even_iff_two_dvd.mp h.1, hn⟩
    rw [eval_prod, ← Finset.prod_erase_mul _ _ h2]
    apply mul_nonpos_of_nonneg_of_nonpos
    · refine Finset.prod_nonneg fun i hi => le_of_lt ?_
      simp only [Finset.mem_erase, mem_properDivisors] at hi
      refine ih _ hi.2.2.2 (Nat.two_lt_of_ne ?_ hi.2.1 hi.1)
      rintro rfl
      rw [zero_dvd_iff] at hi
      exact hn'.ne' hi.2.2.1
    · simpa only [eval_X, eval_one, cyclotomic_two, eval_add] using h.right.le

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

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

Tactic:
constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by lia)

Goal state after: