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

Goal state before:
pp: case neg
𝕜 : 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
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : ¬CompleteSpace G
⊢ ∫ (ξ : W), (M (fourierIntegral e μ L f ξ)) (g ξ) ∂ν = ∫ (x : V), (M (f x)) (fourierIntegral e ν (-L.flip) g x) ∂μ

Tactic:
simp [integral, hG]

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
F : Type u_5
G : Type u_6
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℂ E
inst✝¹⁵ : NormedAddCommGroup F
inst✝¹⁴ : NormedSpace ℂ F
inst✝¹³ : NormedAddCommGroup G
inst✝¹² : NormedSpace ℂ G
inst✝¹¹ : TopologicalSpace 𝕜
inst✝¹⁰ : IsTopologicalRing 𝕜
inst✝⁹ : TopologicalSpace V
inst✝⁸ : BorelSpace V
inst✝⁷ : TopologicalSpace W
inst✝⁶ : MeasurableSpace W
inst✝⁵ : BorelSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
ν : Measure W
inst✝⁴ : SigmaFinite μ
inst✝³ : SigmaFinite ν
inst✝² : SecondCountableTopologyEither W V
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : V → E
g : W → F
M : E →L⋆[ℂ] F →L[ℂ] G
he : Continuous[inst✝¹¹, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝¹¹] fun p ↦ (L p.1) p.2
hf : Integrable f μ
hg : Integrable g ν
hG : CompleteSpace G
⊢ ∫ (ξ : W), (M.flip (g ξ)) (∫ (x : V), e (-(L x) ξ) • f x ∂μ) ∂ν =
    ∫ (ξ : W), ∫ (x : V), (M.flip (g ξ)) (e (-(L x) ξ) • f x) ∂μ ∂ν

Tactic:
by
    congr with ξ
    apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
⊢ ∫ (x : ℝ) in Iic 0, f |x| = ∫ (x : ℝ) in Iic 0, f (-x)

Tactic:
refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_)

Goal state after:
f : ℝ → ℝ
eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x
hf : IntegrableOn (fun x ↦ f |x|) (Ioi 0) volume
int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) volume
x✝ : ℝ
hx : x✝ ∈ Iic 0
⊢ f |x✝| = f (-x✝)
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℝ
ha : a < 0
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, rexp (a * x) = -rexp (a * c) / a

Tactic:
Real.exp,

Goal state after:
a : ℝ
ha : a < 0
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, (Complex.exp ↑(a * x)).re = -(Complex.exp ↑(a * c)).re / a
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun x ↦ -log⁻¹ x) (x⁻¹ / log x ^ 2) x

Tactic:
intro t

Goal state after:
c : ℝ
hc : 1 < c
t : ℝ
⊢ t ∈ Ici c → HasDerivAt (fun x ↦ -log⁻¹ x) (t⁻¹ / log t ^ 2) t
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ioi c, 0 ≤ x⁻¹ / log x ^ 2

Tactic:
intro t

Goal state after:
c : ℝ
hc : 1 < c
t : ℝ
⊢ t ∈ Ioi c → 0 ≤ t⁻¹ / log t ^ 2
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: case convert_1
c : ℝ
hc : 1 < c
⊢ ∀ x ∈ Ici c, HasDerivAt (fun t ↦ -(log t)⁻¹) (x⁻¹ / log x ^ 2) x

Tactic:
intro t

Goal state after:
case convert_1
c : ℝ
hc : 1 < c
t : ℝ
⊢ t ∈ Ici c → HasDerivAt (fun t ↦ -(log t)⁻¹) (t⁻¹ / log t ^ 2) t
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| r

Tactic:
← sqrt_sq (le_of_lt hr),

Goal state after:
r θ : ℝ
hr : r ∈ Ioi 0
hθ : θ ∈ Ioo (-π) π
| √(r ^ 2)
Module: Mathlib.MeasureTheory.Integral.Pi

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
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 → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
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 → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)

Tactic:
rw [← this.integrable_comp_emb (MeasurableEquiv.measurableEmbedding _)]

Goal state after:
case succ
𝕜 : Type u_1
inst✝¹ : NormedCommRing 𝕜
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 → 𝕜},
    (∀ (i : Fin n), Integrable (f i) (μ i)) → Integrable (fun x ↦ ∏ i, f i (x i)) (Measure.pi μ)
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 → 𝕜
hf : ∀ (i : Fin (n + 1)), Integrable (f i) (μ i)
this :
  MeasurePreserving (⇑(MeasurableEquiv.piFinSuccAbove E 0).symm) ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
    (Measure.pi μ)
⊢ Integrable ((fun x ↦ ∏ i, f i (x i)) ∘ ⇑(MeasurableEquiv.piFinSuccAbove E 0).symm)
    ((μ 0).prod (Measure.pi fun j ↦ μ (Fin.succAbove 0 j)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -(((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0)
⊢ s ≠ 0

Tactic:
contrapose! hs

Goal state after:
s : ℂ
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun x ↦ ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x
cont : Continuous ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s)
der_ible : IntervalIntegrable (fun x ↦ -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X
int_eval :
  (∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) =
    -(((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) X - ((ofReal ∘ fun y ↦ rexp (-y)) * fun x ↦ ↑x ^ s) 0)
hs : s = 0
⊢ s.re ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
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]

Goal state after:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: case e'_6
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
v : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))
⊢ ((fun v ↦ cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫)) ∘ ⇑e) v = cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪e.symm w, v⟫)

Tactic:
simp only [neg_mul, Function.comp_apply, LinearIsometryEquiv.norm_map,
    LinearIsometryEquiv.symm_symm,
    LinearIsometryEquiv.inner_map_eq_flip]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
⊢ 𝓢(V, E) →L[𝕜] 𝓢(V, E)

Tactic:
refine mkCLM ((𝓕 : (V → E) → (V → E)) ·) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
⊢ ∀ (f g : 𝓢(V, E)) (x : V), 𝓕 (⇑(f + g)) x = 𝓕 (⇑f) x + 𝓕 (⇑g) x

case refine_2
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
⊢ ∀ (a : 𝕜) (f : 𝓢(V, E)) (x : V), 𝓕 (⇑(a • f)) x = (RingHom.id 𝕜) a • 𝓕 (⇑f) x

case refine_3
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
⊢ ∀ (f : 𝓢(V, E)), ContDiff ℝ (↑⊤) (𝓕 ⇑f)

case refine_4
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
⊢ ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(V, E)) (x : V),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (𝓕 ⇑f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 V E)) f
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f g : 𝓢(V, E)
⊢ ∀ (x : V), 𝓕 (⇑(f + g)) x = 𝓕 (⇑f) x + 𝓕 (⇑g) x

Tactic:
simp [fourier_eq, integral_add ((fourierIntegral_convergent_iff _).mpr f.integrable)
      ((fourierIntegral_convergent_iff _).mpr g.integrable)]

Goal state after:
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
x : α
⊢ x ∈ dsupport f ↔ ∀ (s : Set α), IsVanishingOn f sᶜ → IsClosed[inst✝²] s → x ∈ s

Tactic:
by
  simp [dsupport]

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
f : 𝓢'(E, F)
⊢ MemSobolev 0 2 f ↔ ∃ f', 𝓕 f = Lp.toTemperedDistribution f'

Tactic:
simp [memSobolev_iff_exists_smulLeftCLM_fourier]

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

Goal state before:
pp: case intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
have : Unique (Fin Nat.zero →₀ ℤ) :=
      { uniq := by subsingleton }

Goal state after:
case intro.zero
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
f : G ≃+ (Fin 0 →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
this : Unique (Fin Nat.zero →₀ ℤ)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))
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)
hf : MemSobolev s 2 f
m x : E
⊢ ‖↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))‖ ≤ ‖m‖

Tactic:
apply le_of_sq_le_sq _ (by positivity)

Goal state after:
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)
hf : MemSobolev s 2 f
m x : E
⊢ ‖↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))‖ ^ 2 ≤ ‖m‖ ^ 2
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: ⊢ μ.IsMultiplicative

Tactic:
IsMultiplicative.iff_ne_zero

Goal state after:
⊢ μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → μ (m * n) = μ m * μ n
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

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

Tactic:
rw [pmul_apply, intCoe_apply, ArithmeticFunction.moebius_apply_prime
        (prime_of_mem_primeFactorsList (List.mem_toFinset.mp hp))]

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : f.IsMultiplicative
n : ℕ
hn : Squarefree n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - f p = 1 + ↑(-1) * f p
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}
this : A = Metric.closedBall 0 (R + 1)
⊢ MeasurableSet (Metric.closedBall 0 (R + 1))

Tactic:
exact Metric.isClosed_closedBall.measurableSet

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
f g : ℕ → R
hf : ∀ (n : ℕ), 0 < n → f n ≠ 0
hg : ∀ (n : ℕ), 0 < n → g n ≠ 0
n : ℕ
hn : n > 0
⊢ (∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
      if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
· 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.Complex

Goal state before:
pp: case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑(↑(2 • n) / ↑q.den)) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))

Tactic:
Int.nsmul_eq_mul

Goal state after:
case e'_3
q : ℚ
h : Even q.num
n : ℤ
hn : q.num = 2 • n
⊢ cexp (↑π * I * ↑(↑(↑2 * n) / ↑q.den)) = cexp (2 * ↑π * I * ↑(↑n / ↑q.den))
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ orderOf ζ > 0

Tactic:
rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
Module: Mathlib.RingTheory.RootsOfUnity.Minpoly

Goal state before:
pp: case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
⊢ minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))

Tactic:
let : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed

Goal state after:
case inr
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed
⊢ minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case pos
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

pp: case neg
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : ¬n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

Tactic:
· simp only [hzero, cyclotomic, dif_pos, Polynomial.map_one]

Goal state after:
case neg
n : ℕ
R : Type u_1
inst✝ : Ring R
hzero : ¬n = 0
⊢ map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (nthRoots n 1).card = n

Tactic:
rw [card_nthRoots h, if_pos ⟨ζ, h.pow_eq_one⟩]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
rw [hzero] at heq

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : -1 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

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

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:
· simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]
    constructor <;> intro <;> linarith

Goal state after:
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))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case f
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
x✝ : L →ₐ[K] E
| x✝ (ζ - 1)

Tactic:
rw [← neg_sub, map_neg, map_sub, map_one, neg_eq_neg_one_mul]

Goal state after:
case f
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝¹ : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝ : FiniteDimensional K L := finiteDimensional {n} K L
this : IsGalois K L := isGalois {n} K L
x✝ : L →ₐ[K] E
| -1 * (1 - x✝ ζ)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ ∏ x, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))

Tactic:
Hprod,

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝ : IsCyclotomicExtension {n} K L
h : 2 < n
hirr : Irreducible (cyclotomic n K)
this✝² : NeZero ↑n
E : Type v := AlgebraicClosure L
z : E
hz : (cyclotomic n E).IsRoot z
this✝¹ : FiniteDimensional K L := finiteDimensional {n} K L
this✝ : IsGalois K L := isGalois {n} K L
Hprod : ∏ σ, (1 - σ ζ) = eval 1 (cyclotomic' n E)
this : NeZero ↑n
⊢ eval 1 (cyclotomic' n E) = (algebraMap K E) ↑(eval 1 (cyclotomic n ℤ))
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
⊢ (Algebra.norm K) (ζ - 1) = 2

Tactic:
have : 2 < 2 ^ k := by
    nth_rw 1 [← pow_one 2]
    exact Nat.pow_lt_pow_right one_lt_two (lt_of_lt_of_le one_lt_two hk)

Goal state after:
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ k)
hk : 2 ≤ k
H : IsCyclotomicExtension {2 ^ k} K L
hirr : Irreducible (cyclotomic (2 ^ k) K)
this : 2 < 2 ^ k
⊢ (Algebra.norm K) (ζ - 1) = 2
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
⊢ K ≃+* K'

Tactic:
have hpp' : p = p' := by
    by_contra hne
    simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne

Goal state after:
p✝ : ℕ
inst✝⁴ : Fact (Nat.Prime p✝)
n✝ : ℕ
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Fintype K
inst✝ : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ ↑n
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ ↑n'
hpp' : p = p'
⊢ K ≃+* K'