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

Goal state before:
pp: case h₂
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : OpensMeasurableSpace E
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
p : ℝ≥0∞
μ : Measure E
hμ : μ.HasTemperateGrowth
k : ℕ
hk : eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-↑k)) p μ < ∞
f : 𝓢(E, F)
h_one_add : ∀ (x : E), 0 < 1 + ‖x‖
x : E
⊢ ‖(1 + ‖x‖) ^ k • f x‖ ≤ ↑(↑2 ^ k * (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f).toNNReal)

Tactic:
simpa [norm_smul, abs_of_nonneg (h_one_add x).le] using!
      one_add_le_sup_seminorm_apply (m := (k, 0)) (le_refl k) (le_refl 0) f x

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

Goal state before:
pp: case h'iφ
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 φ μ
⊢ ∀ᶠ (i : ℝ) in atTop, AEStronglyMeasurable (fun x ↦ i ^ finrank ℝ F * φ (i • x)) μ

pp: case hmg
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 φ μ
⊢ Integrable g μ

pp: case hcg
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 φ μ
⊢ Tendsto g (𝓝 0) (𝓝 (g 0))

Tactic:
· filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
    exact (I.comp_smul hc.ne').aestronglyMeasurable.const_mul _

Goal state after:
case hmg
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 φ μ
⊢ Integrable g μ

case hcg
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 φ μ
⊢ Tendsto g (𝓝 0) (𝓝 (g 0))
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ Integrable (⇑f) volume

Tactic:
by
  refine integrable_of_summable_norm_restrict (.of_nonneg_of_le
    (fun n : ℤ => mul_nonneg (norm_nonneg
      (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
        ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_
  · simp only [Compacts.coe_mk, le_add_iff_nonneg_right, zero_le_one, volume_real_Icc_of_le,
      add_sub_cancel_left, mul_one, norm_le _ (norm_nonneg _), ContinuousMap.restrict_apply]
    intro x
    have := ((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
        ⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩
    simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk,
      sub_add_cancel] using this
  · exact iUnion_Icc_intCast ℝ

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
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
i : ℕ
⊢ i ≤ n →
    ∀ j ≤ k,
      ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤
        ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖v‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f v‖

Tactic:
hi

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
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
I : ∀ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), Integrable (fun v ↦ ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖) μ
v : V
i : ℕ
hi : i ≤ n
⊢ ∀ j ≤ k,
    ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤
      ∑ i ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ‖v‖ ^ i.1 * ‖iteratedFDeriv ℝ i.2 f v‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: H : Type u_8
V : Type u_9
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : NormedSpace ℝ H
inst✝⁵ : FiniteDimensional ℝ H
inst✝⁴ : MeasurableSpace H
inst✝³ : BorelSpace H
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℂ V
f g : 𝓢(H, V)
μ : Measure H
inst✝ : μ.HasTemperateGrowth
⊢ inner ℂ (f.toLp 2 μ) (g.toLp 2 μ) = ∫ (x : H), inner ℂ (f x) (g x) ∂μ

Tactic:
apply integral_congr_ae
  have hf_ae := f.coeFn_toLp 2 μ
  have hg_ae := g.coeFn_toLp 2 μ
  filter_upwards [hf_ae, hg_ae] with _ hf hg
  rw [hf, 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
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
v : V
w : W
⊢ ((2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ) *
      ‖v‖ ^ n =
    ‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (2 * ↑k + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ

Tactic:
simp [mul_pow]
    ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: ⊢ Integrable (fun x ↦ (1 + x ^ 2)⁻¹) volume

Tactic:
suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]
  exact integrable_rpow_neg_one_add_norm_sq (by simp)

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

Goal state before:
pp: s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ↑(∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1))

Tactic:
conv_rhs => rw [this, ← _root_.integral_ofReal]

Goal state after:
s : ℝ
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x ↦ x * (b * x ^ (p - 1) + -1)) atTop atTop

Tactic:
apply tendsto_id.atTop_mul_atTop₀

Goal state after:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x ↦ b * x ^ (p - 1) + -1) atTop atTop
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
N : ℕ∞
n : ℕ
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedDeriv n f) volume
hn : ↑n ≤ N
x : ℝ
A : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) volume
⊢ ((fourierPowSMulRight (-innerSL ℝ) (𝓕 f) x n) fun x ↦ 1) = (2 * ↑π * I * ↑x) ^ n • 𝓕 f x

Tactic:
simp [← coe_smul, smul_smul, ← mul_pow, innerSL_apply_apply ℝ]

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
c : ℂ
hc : c ∈ {c | 0 < c.re}
⊢ (↑π / c) ^ 1 = (↑π / c) ^ (1 / 2 + 1 / 2)

Tactic:
norm_num

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹

Tactic:
norm_num

Goal state after:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (-1) = x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ x ^ (2 - 1) = x

Tactic:
norm_num

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 + 1 = -↑m
⊢ s = -↑(1 + m)

Tactic:
rw [← eq_sub_iff_add_eq] at 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
⊢ s = -↑(1 + m)
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case refine_1
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ mFourier 0 = 1

Tactic:
ext z

Goal state after:
case refine_1
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
z : UnitAddTorus d
⊢ (mFourier 0) z = 1 z
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case refine_2
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
⊢ mFourier (m + n) = mFourier m * mFourier n

Tactic:
ext z

Goal state after:
case refine_2
d : Type u_1
inst✝ : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx✝ : mFourier m ∈ Submonoid.closure (range mFourier)
n : d → ℤ
hy✝ : mFourier n ∈ Submonoid.closure (range mFourier)
z : UnitAddTorus d
⊢ (mFourier (m + n)) z = (mFourier m * mFourier n) z
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ (∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}, f fun i ↦ ↑(x i)) =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume

Tactic:
rw [← lintegral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]

Goal state after:
case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : ↑{f | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}), f fun i ↦ ↑(↑x i) ∂Measure.comap Subtype.val volume =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ ∀ (i j : d → ℤ), inner ℂ (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0

Tactic:
intro m n

Goal state after:
d : Type u_1
inst✝ : Fintype d
m n : d → ℤ
⊢ inner ℂ (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0
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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ 2 ≠ 0

Tactic:
norm_num

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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
⊢ 2 ≠ ∞

Tactic:
norm_num

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality

Goal state before:
pp: G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
ψ₁ ψ₂ : AddChar G R
inst✝ : Fintype G
⊢ ⟪⇑ψ₁, ⇑ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂

Tactic:
by
  rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module ℤ M
inst✝ : Module.Finite ℤ M
hM : IsTorsion ℤ M
⊢ Finite M

Tactic:
by
  rcases Module.equiv_directSum_of_isTorsion hM with ⟨ι, _, p, h, e, ⟨l⟩⟩
  have : ∀ i : ι, NeZero (p i ^ e i).natAbs := fun i =>
    ⟨Int.natAbs_ne_zero.mpr <| pow_ne_zero (e i) (h i).ne_zero⟩
  have : ∀ i : ι, _root_.Finite <| ℤ ⧸ Submodule.span ℤ {p i ^ e i} := fun i =>
    Finite.of_equiv _ (p i ^ e i).quotientSpanEquivZMod.symm.toEquiv
  have : _root_.Finite (⨁ i, ℤ ⧸ (Submodule.span ℤ {p i ^ e i} : Submodule ℤ ℤ)) :=
    Finite.of_equiv _ DFinsupp.equivFunOnFintype.symm
  exact Finite.of_equiv _ l.symm.toEquiv

Goal state after:
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
⊢ (complexBasis α) ψ = ⇑ψ

Tactic:
rw [coe_complexBasis]

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✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s s' : ℝ
h : s' ≤ s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ 0 < 2

Tactic:
norm_num

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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
⊢ (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v ↦ (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)

Tactic:
ext1 v

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 + i w) = (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by
  by_cases h0 : k = 0
  · subst k; simp_all only [pow_one, Nat.coprime_zero_right]
  rcases h.isUnit h0 with ⟨ζ, rfl⟩
  rw [← Units.val_pow_eq_pow_val]
  rw [coe_units_iff] at h ⊢
  refine
    { pow_eq_one := by rw [← pow_mul', pow_mul, h.pow_eq_one, one_pow]
      dvd_of_pow_eq_one := fun l hl ↦ h.dvd_of_pow_eq_one l ?_ }
  rw [← pow_one ζ, ← zpow_natCast ζ, ← hi.gcd_eq_one, Nat.gcd_eq_gcd_ab, zpow_add, mul_pow,
    ← zpow_natCast, ← zpow_mul, mul_right_comm]
  simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_natCast]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
⊢ i ∈ ↑(range n) → ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range n) → (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) x₂ → i = x₂

Tactic:
hi

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
ζ : M
hζ : IsPrimitiveRoot ζ n
i : ℕ
hi : i ∈ ↑(range n)
⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ ↑(range n) → (fun x ↦ ζ ^ x) i = (fun x ↦ ζ ^ x) x₂ → i = x₂
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
l : ℕ
hl : f ζ ^ l = 1
⊢ orderOf (f ζ) ∣ l

Tactic:
exact orderOf_dvd_of_pow_eq_one hl

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

Goal state before:
pp: case pos
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℕ
hi : (↑i).gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ ↑i) k

Tactic:
exact_mod_cast h.pow_of_coprime i hi

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

Goal state before:
pp: 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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Tactic:
rw [mul_comm] at hd

Goal state after:
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
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case left
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
i : ZMod k
⊢ (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
          ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
        i =
      0 →
    i = 0

Tactic:
hi

Goal state after:
case left
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
i : ZMod k
hi :
  (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
      i =
    0
⊢ i = 0
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)

Tactic:
sub_div,

Goal state after:
case e'_2.e'_5
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - ↑n / ↑n) * (2 * ↑Real.pi)
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i - ↑n) / ↑n * (2 * ↑Real.pi)

Tactic:
sub_div,

Goal state after:
case e'_2.e'_6
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ¬i * 2 ≤ n
⊢ (↑i / ↑n - 1) * (2 * ↑Real.pi) = (↑i / ↑n - ↑n / ↑n) * (2 * ↑Real.pi)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (cyclotomic 1 ℤ)

Tactic:
← int_cyclotomic_unique hspec

Goal state after:
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

Tactic:
by
  have integer : ∏ i ∈ Nat.divisors n, cyclotomic i ℤ = X ^ n - 1 := by
    apply map_injective (Int.castRingHom ℂ) Int.cast_injective
    simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
      Polynomial.map_one, Polynomial.map_sub]
    exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
  simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one,
    Polynomial.map_pow, Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer

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

Goal state before:
pp: n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
by
  suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
    simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
      Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this
  rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
    cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]

Goal state after: