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

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ (fourier (-n)) ↑z✝ = (starRingEnd ℂ) ((fourier n) ↑z✝)

Tactic:
fourier_apply,

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(-n • ↑z✝).toCircle = (starRingEnd ℂ) ↑(n • ↑z✝).toCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ (fourier (-n)) ↑z✝ = (starRingEnd ℂ) ((fourier n) ↑z✝)

Tactic:
simp_rw [fourier_apply, toCircle]

Goal state after:
case H
T : ℝ
n : ℤ
z✝ : ℝ
⊢ ↑(⋯.lift (-n • ↑z✝)) = (starRingEnd ℂ) ↑(⋯.lift (n • ↑z✝))
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
m n : ℤ
x : AddCircle T
⊢ (fourier (m + n)) x = (fourier m) x * (fourier n) x

Tactic:
fourier_apply,

Goal state after:
T : ℝ
m n : ℤ
x : AddCircle T
⊢ ↑((m + n) • x).toCircle = ↑(m • x).toCircle * ↑(n • x).toCircle
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ (fourier n) (x + ↑(T / 2 / ↑n)) = -(fourier n) x

Tactic:
fourier_apply,

Goal state after:
T : ℝ
n : ℤ
hn : n ≠ 0
hT : 0 < T
x : AddCircle T
⊢ ↑(n • (x + ↑(T / 2 / ↑n))).toCircle = -(fourier n) x
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪b i, b j⟫ = if i = j then 1 else 0

Tactic:
rw [← b.repr.inner_map_map (b i) (b j), b.repr_self, b.repr_self, lp.inner_single_left,
    lp.single_apply, Pi.single_apply]

Goal state after:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
i j : ι
⊢ ⟪1, if i = j then 1 else 0⟫ = if i = j then 1 else 0
Module: Mathlib.Analysis.Fourier.AddCircle

Goal state before:
pp: case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
⊢ ‖(fourier n) t‖ ≤ 1

Tactic:
fourier_apply,

Goal state after:
case hφ2
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : AddCircle T → E
hf : Integrable f haarAddCircle
n : ℤ
t : AddCircle T
⊢ ‖↑(n • t).toCircle‖ ≤ 1
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i ↦ ((innerSL 𝕜) (b i)) x • b i) x

Tactic:
by
    simpa only [innerSL_apply_apply, ← b.repr_apply_apply] using b.hasSum_repr x

Goal state after:
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:
rw [← norm_toNNReal, Real.toNNReal_le_iff_le_coe]

Goal state after:
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)
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: 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 φ μ
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun x ↦ c ^ finrank ℝ F * φ (c • x)) μ

Tactic:
exact (I.comp_smul hc.ne').aestronglyMeasurable.const_mul _

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : Integrable g μ
⊢ Integrable f μ

Tactic:
rewrite [← integrableAtFilter_top] at *
  exact hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
  exact ⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩

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

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
⊢ ‖{ toFun := fourierTransform, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖

Tactic:
by
      rw [one_mul, BoundedContinuousFunction.norm_le (by positivity)]
      intro x
      rw [LinearMap.coe_mk, AddHom.coe_mk, Lp.fourierTransform_apply, Real.fourier_eq]
      apply (norm_integral_le_integral_norm _).trans
      simp_rw [Circle.norm_smul]
      exact (L1.norm_eq_integral_norm f).symm.le

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

Goal state before:
pp: p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
⊢ IntegrableOn (fun x ↦ (b ^ (-p⁻¹)) ^ s * (x ^ s * rexp (-x ^ p))) (Ioi 0) volume

Tactic:
refine Integrable.const_mul ?_ _

Goal state after:
p s b : ℝ
hs : -1 < s
hp : 0 < p
hb : 0 < b
hib : 0 < b ^ (-p⁻¹)
⊢ Integrable (fun x ↦ x ^ s * rexp (-x ^ p)) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p

Tactic:
rw [← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb
    measurableEquivRealProd.symm.measurableEmbedding, ← lintegral_comp_polarCoord_symm]

Goal state after:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
⊢ (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target, (∏ i, (p i).1) • f fun i ↦ ↑polarCoord.symm (p i)) =
    ∫ (x : ι → ℝ × ℝ) in Set.univ.pi fun x ↦ polarCoord.target,
      |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
refine setIntegral_congr_fun measurableSet_pi_polarCoord_target fun x hx ↦ ?_

Goal state after:
case e'_2
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : (ι → ℝ × ℝ) → E
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, (x i).1) • f fun i ↦ ↑polarCoord.symm (x i)) =
    |(fderivPiPolarCoordSymm x).det| • f fun i ↦ ↑polarCoord.symm (x i)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
rcases n with - | n
  · simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]
    rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]
    rintro rfl
    rw [zero_re] at h1
    exact h1.false
  · dsimp only [GammaAux]
    have : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1) := by
      have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
      rw [GammaAux_recurrence1 (s + 1) n hh1]
    rw [this]

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
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ ∫ (x : ℝ), ↑(rexp (-1 * x ^ 2)) = (↑π / 1) ^ (1 / 2)

Tactic:
integral_ofReal,

Goal state after:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ ↑(∫ (x : ℝ), rexp (-1 * x ^ 2)) = (↑π / 1) ^ (1 / 2)
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: case h'φ
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)
⊢ π ^ (↑(finrank ℝ V) / 2) * π ^ ((↑1 - ↑2) * (↑(finrank ℝ V) / 2)) = 1

Tactic:
← rpow_add pi_pos

Goal state after:
case h'φ
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)
⊢ π ^ (↑(finrank ℝ V) / 2 + (↑1 - ↑2) * (↑(finrank ℝ V) / 2)) = 1
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
m : E
f : 𝓢(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ inner ℝ x m) f

Tactic:
fourierMultiplierCLM_apply,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : NormedSpace ℂ F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
m : E
f : 𝓢(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • 𝓕⁻ ((smulLeftCLM F fun x ↦ inner ℝ x m) (𝓕 f))
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
m : E
f : 𝓢'(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • (fourierMultiplierCLM F fun x ↦ ↑(inner ℝ x m)) f

Tactic:
fourierMultiplierCLM_apply,

Goal state after:
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
m : E
f : 𝓢'(E, F)
⊢ ∂_{m} f = (2 * ↑π * Complex.I) • 𝓕⁻ ((smulLeftCLM F fun x ↦ ↑(inner ℝ x m)) (𝓕 f))
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℂ E
V : Type u_3
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace ℝ V
inst✝⁸ : FiniteDimensional ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℂ G
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : 𝓢(V, E)
g : 𝓢(V, F)
M : E →L[ℂ] F →L[ℂ] G
⊢ ∫ (ξ : V), (M ((𝓕 f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((𝓕 g) x)

Tactic:
simpa using! VectorFourier.integral_bilin_fourierIntegral_eq_flip M (L := innerₗ V)
    continuous_fourierChar continuous_inner f.integrable g.integrable

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
x : E
hf : ↑↑(f.toLp p μ) x = f x
⊢ g x • ↑↑(f.toLp p μ) x = g x • f x

Tactic:
rw [hf]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst✝ : SecondCountableTopology E
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ toTemperedDistribution (f.toLp p μ) = (toTemperedDistributionCLM E F μ) f

Tactic:
ext g
  simp only [Lp.toTemperedDistribution_apply, toTemperedDistributionCLM_apply_apply]
  apply integral_congr_ae
  filter_upwards [f.coeFn_toLp p μ] with x hf
  rw [hf]

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

Goal state before:
pp: case h
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
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
hvv' : v ≠ v'
w : W
hw : (char he hL w) v ≠ (char he hL w) v'
⊢ (∃ a ∈ charPoly he hL, ⇑((toContinuousMapStarₐ ℂ) a) = ⇑(char he hL w)) ∧ ¬(char he hL w) v = (char he hL w) v'

Tactic:
exact ⟨⟨char he hL w, char_mem_charPoly w, rfl⟩, hw⟩

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

Tactic:
convert! integral_sub_right_eq_self _ y (μ := volume)

Goal state after:
case e'_2.e'_7
𝕜 : 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
ξ y x✝ : E
⊢ 𝐞 (-inner ℝ x✝ ξ) • (B (f₁ (x✝ - y))) (f₂ y) = 𝐞 (-inner ℝ (y + (x✝ - y)) ξ) • (B (f₁ (x✝ - y))) (f₂ y)
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this : Integrable (fun ξ ↦ (B ((𝓕 f) ξ)) ((𝓕 g) ξ)) volume
x✝ : E
⊢ (𝓕 (((convolution B) f) g)) x✝ = (B ((𝓕 f) x✝)) ((𝓕 g) x✝)

Tactic:
fourier_convolution,

Goal state after:
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
this : Integrable (fun ξ ↦ (B ((𝓕 f) ξ)) ((𝓕 g) ξ)) volume
x✝ : E
⊢ (((pairing B) (𝓕 f)) (𝓕 g)) x✝ = (B ((𝓕 f) x✝)) ((𝓕 g) x✝)
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R ↑n) A ≤ B
this : A.toAddSubgroup.FG
⊢ B.toAddSubgroup.IsFiniteRelIndex A.toAddSubgroup

Tactic:
have := isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg this hn

Goal state after:
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : Module.Finite ℤ R
A B : Submodule R K
n : ℕ
hn : n ≠ 0
hfg : A.FG
h : map (LinearMap.mulLeft R ↑n) A ≤ B
this✝ : A.toAddSubgroup.FG
this : (AddSubgroup.map (nsmulAddMonoidHom n) A.toAddSubgroup).IsFiniteRelIndex A.toAddSubgroup
⊢ B.toAddSubgroup.IsFiniteRelIndex A.toAddSubgroup
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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 : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 ((fourierMultiplierCLM F g) f)) =
    (smulLeftCLM F ⇑g') ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f))

Tactic:
fourierMultiplierCLM_apply,

Goal state after:
case h
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 : ℝ
f : 𝓢'(E, F)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
f' : ↥(Lp F 2 volume)
hf : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
C : ℝ
hC : ∀ (x : E), ‖g x‖ ≤ C
g' : E →ᵇ ℂ := BoundedContinuousFunction.ofNormedAddCommGroup g ⋯ C hC
⊢ (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 (𝓕⁻ ((smulLeftCLM F g) (𝓕 f)))) =
    (smulLeftCLM F ⇑g') ((smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f))
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := ⋯
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ Summable fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight ↑n))‖

Tactic:
convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1

Goal state after:
f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ (fun n ↦ ‖ContinuousMap.restrict (Icc 0 1) ((e * f).comp (ContinuousMap.addRight ↑n))‖) = fun n ↦
    ‖ContinuousMap.restrict (↑{ carrier := Icc 0 1, isCompact' := ⋯ }) (f.comp (ContinuousMap.addRight ↑n))‖
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ ↑1 = 1

Tactic:
intCoe_one

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ 1 = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ ζ' : M
k' : ℕ
hζ : IsPrimitiveRoot ζ k
hζ' : IsPrimitiveRoot ζ' k'
hk : k ≠ 0
hk' : k' ≠ 0
⊢ IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')

Tactic:
by
  convert! IsPrimitiveRoot.orderOf _
  convert!
    ((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf])
        (by simpa [← hζ'.eq_orderOf])).symm using 2
  all_goals simp [hζ.eq_orderOf, hζ'.eq_orderOf]

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

Tactic:
injective_iff_map_eq_zero

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
⊢ ∀ (a : ZMod k),
    (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
            ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
          a =
        0 →
      a = 0
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
h : n ≠ 0
i : ℕ
⊢ (map (Int.castRingHom ℤ) ⋯.choose).coeff i = ⋯.choose.coeff i

Tactic:
simp only [coeff_map, Int.cast_id, eq_intCast]

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

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ ξ : R
h : IsPrimitiveRoot ζ k
hξ : ξ ^ k = 1
⊢ ∃ i < k, ζ ^ i = ξ

Tactic:
lift ζ to Rˣ using h.isUnit NeZero.out

Goal state after:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ξ : R
hξ : ξ ^ k = 1
ζ : Rˣ
h : IsPrimitiveRoot (↑ζ) k
⊢ ∃ i < k, ↑ζ ^ i = ξ