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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
⊢ ∃ c, IsBigOWith c atTop (fun x ↦ x ^ (-↑k)) fun x ↦ x ^ s

Tactic:
Asymptotics.IsBigOWith

Goal state after:
E : Type u_5
F : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : 𝓢(E, F)
inst✝ : ProperSpace E
s : ℝ
k : ℕ := ⌈-s⌉₊
hk : -↑k ≤ s
⊢ ∃ c, ∀ᶠ (x : ℝ) in atTop, ‖x ^ (-↑k)‖ ≤ c * ‖x ^ s‖
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖m‖ * (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
move_mul [‖m‖]

Goal state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ * ‖m‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f * ‖m‖
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 → 𝕜
f : 𝓢(E, F)
⊢ tsupport ⇑((smulLeftCLM F g) f) ⊆ tsupport ⇑f ∩ tsupport g

Tactic:
by
  by_cases hg : g.HasTemperateGrowth
  · simpa [smulLeftCLM_apply hg] using
      ⟨tsupport_smul_subset_right g f, tsupport_smul_subset_left g f⟩
  · simp [smulLeftCLM, hg, FunLike.coe_zero]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁷ : TopologicalSpace α
inst✝⁶ : BorelSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝³ : CompleteSpace E
inst✝² : MetrizableSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
hs : IsCompact s
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ closure[inst✝⁷] (interior s)
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
this : x₀ ∈ s
u : Set α
u_open : IsOpen[inst✝⁷] u
x₀_u : x₀ ∈ u
⊢ μ (u ∩ interior s) ≤ μ (u ∩ s)

Tactic:
gcongr; apply interior_subset

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

Goal state before:
pp: 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✝ : SecondCountableTopologyEither E F
f : 𝓢(E, F)
μ : Measure E
⊢ MemLp ⇑f ∞ μ

Tactic:
by
  rcases f.decay 0 0 with ⟨C, _, hC⟩
  refine memLp_top_of_bound f.continuous.aestronglyMeasurable C (ae_of_all μ fun x ↦ ?_)
  simpa using hC x

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

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ s.re < -1 + 1

Tactic:
neg_add_cancel

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ s.re < 0
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x ↦ s * ↑x ^ (s - 1)) (Ioi t) volume
⊢ IntegrableOn (deriv fun x ↦ ↑x ^ s) (Ioi t) volume

Tactic:
refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (fun x ↦ s * ↑x ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ (fun x ↦ s * ↑x ^ (s - 1)) x = deriv (fun x ↦ ↑x ^ s) x
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ s.re < -1 + 1

Tactic:
neg_add_cancel

Goal state after:
s : ℂ
t : ℝ
ht : 0 < t
hs✝ : s.re ≤ 0
hs : s.re < 0
⊢ s.re < 0
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
⊢ HasFDerivAt (fun x i ↦ ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p

Tactic:
have := Fintype.ofFinite ι
  rw [fderivPiPolarCoordSymm, hasFDerivAt_pi]
  exact fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

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

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ (∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2)) * ∫ (θ : ℝ) in Ioo (-π) π, 1 = ↑π / b

Tactic:
simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply,
        univ_inter, real_smul, mul_one, integral_mul_cexp_neg_mul_sq hb]

Goal state after:
b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * ↑(volume.real (Ioo (-π) π)) = ↑π / b
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T = I₂ T + I * ∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2) - cexp (-b * (↑T - ↑x * I) ^ 2)

Tactic:
intervalIntegral.integral_sub

Goal state after:
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ I₁ T =
    I₂ T + I * ((∫ (x : ℝ) in 0..c, cexp (-b * (↑T + ↑x * I) ^ 2)) - ∫ (x : ℝ) in 0..c, cexp (-b * (↑T - ↑x * I) ^ 2))

case hf
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x ↦ cexp (-b * (↑T + ↑x * I) ^ 2)) volume 0 c

case hg
b : ℂ
hb : 0 < b.re
c : ℝ
I₁ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
HI₁ : I₁ = fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * (↑x + ↑c * I) ^ 2)
I₂ : ℝ → ℂ := fun T ↦ ∫ (x : ℝ) in -T..T, cexp (-b * ↑x ^ 2)
I₄ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (↑T + ↑y * I) ^ 2)
I₅ : ℝ → ℂ := fun T ↦ ∫ (y : ℝ) in 0..c, cexp (-b * (-↑T + ↑y * I) ^ 2)
T : ℝ
C : I₂ T - I₁ T + I * I₄ T = I * I₅ T
⊢ IntervalIntegrable (fun x ↦ cexp (-b * (↑T - ↑x * I) ^ 2)) volume 0 c
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))

Tactic:
have h (x : ℝ) : cexp (b * x ^ 2 + c * x + d) =
      cexp (- -b * (x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b)) := by
    simp_rw [← Complex.exp_add]
    congr 1
    field

Goal state after:
b : ℂ
hb : b.re < 0
c d : ℂ
hb' : b ≠ 0
h : ∀ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = cexp (- -b * (↑x + c / (2 * b)) ^ 2) * cexp (d - c ^ 2 / (4 * b))
⊢ ∫ (x : ℝ), cexp (b * ↑x ^ 2 + c * ↑x + d) = (↑π / -b) ^ (1 / 2) * cexp (d - c ^ 2 / (4 * b))
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: 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
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext v
  exact hf.fourierInv_fourier_eq h'f h.continuousAt

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

Goal state before:
pp: case hp.hg
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ Continuous fun y ↦ toTemperedDistribution (𝓕 y)

Tactic:
· exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

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

Goal state before:
pp: case a
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
⊢ ‖mFourier n‖ ≤ 1

Tactic:
refine (ContinuousMap.norm_le _ zero_le_one).mpr fun i ↦ ?_
    simp only [mFourier, fourier_apply, ContinuousMap.coe_mk, norm_prod, Circle.norm_coe,
      Finset.prod_const_one, le_rfl]

Goal state after:
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✝¹² : NormedAddCommGroup F₁
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedAddCommGroup F₃
inst✝⁹ : InnerProductSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
inst✝⁷ : MeasurableSpace E
inst✝⁶ : BorelSpace E
inst✝⁵ : NormedSpace ℂ F₃
inst✝⁴ : CompleteSpace F₁
inst✝³ : CompleteSpace F₂
inst✝² : CompleteSpace F₃
inst✝¹ : NormedSpace ℂ F₁
inst✝ : NormedSpace ℂ F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ ∫ (y : E), (∫ (x : E), B (𝐞 (-inner ℝ x ξ) • f₁ x)) (𝐞 (-inner ℝ y ξ) • f₂ y) =
    (B (∫ (x : E), 𝐞 (-inner ℝ x ξ) • f₁ x)) (∫ (y : E), 𝐞 (-inner ℝ y ξ) • f₂ y)

Tactic:
rw [← integral_comp_comm _ (by simpa using hf₂), ← integral_comp_comm _ (by simpa using hf₁)]

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁷ : RCLike 𝕜
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : InnerProductSpace ℝ E
inst✝¹⁴ : FiniteDimensional ℝ E
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
inst✝¹¹ : NormedAddCommGroup F₁
inst✝¹⁰ : NormedSpace ℂ F₁
inst✝⁹ : NormedSpace 𝕜 F₁
inst✝⁸ : SMulCommClass ℂ 𝕜 F₁
inst✝⁷ : NormedAddCommGroup F₂
inst✝⁶ : NormedSpace ℂ F₂
inst✝⁵ : NormedSpace 𝕜 F₂
inst✝⁴ : SMulCommClass ℂ 𝕜 F₂
inst✝³ : NormedAddCommGroup F₃
inst✝² : NormedSpace ℂ F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : SMulCommClass ℂ 𝕜 F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
⊢ ∀ (x y : 𝓢(E, F₁)),
    fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 (x + y)) ∘SL fourierCLM 𝕜 𝓢(E, F₂) =
      fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 x) ∘SL fourierCLM 𝕜 𝓢(E, F₂) +
        fourierInvCLM 𝕜 𝓢(E, F₃) ∘SL (pairing B) (𝓕 y) ∘SL fourierCLM 𝕜 𝓢(E, F₂)

Tactic:
by simp [FourierTransform.fourier_add]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ (∃ ψ, ψ a ≠ 1) ↔ a ≠ 0

Tactic:
refine ⟨?_, fun ha ↦ ?_⟩
  · rintro ⟨ψ, hψ⟩ rfl
    exact hψ ψ.map_zero_eq_one
  classical
  by_contra! h
  let f : α → ℂ := fun b ↦ if a = b then 1 else 0
  have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
  have h₁ := congr_fun ((complexBasis α).sum_repr f) a
  simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
    map_zero_eq_one, if_pos rfl, if_neg ha, f] at h₀ h₁
  exact one_ne_zero (h₁.symm.trans h₀)

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

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ (if k = 1 then -1 else 0) = 0

Tactic:
if_neg

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ 0 = 0

case hnc
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Nat.Prime (p ^ k)
⊢ ¬k = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else f x, map_zero' := ⋯ }
g' : ArithmeticFunction R := { toFun := fun x ↦ if x = 0 then 0 else g x, map_zero' := ⋯ }
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
trans (ζ : ArithmeticFunction ℤ) • f' = g'

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔ ↑ζ • f' = g'

R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ↑ζ • f' = g' ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l

Tactic:
have : 0 ≤ -l := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le

Goal state after:
case neg
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℤ
h0 : ¬0 ≤ l
this : 0 ≤ -l
⊢ ζ ^ l = 1 ↔ ↑k ∣ l
Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma

Goal state before:
pp: E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hf1 :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf2 : HasCompactSupport f
ε : ℝ
hε : ε > 0
R : ℝ
hR_bd : ∀ (x : V), R ≤ ‖x‖ → f x = 0
A : Set V := {v | ‖v‖ ≤ R + 1}
mA : MeasurableSet A
B : ℝ≥0
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ R ≤ ‖v‖

Tactic:
· exact (le_add_of_nonneg_right zero_le_one).trans hv.le

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

Goal state before:
pp: case neg.convert_2.left
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : ↑n < ↑i * 2
⊢ -↑n < (↑i - ↑n) * 2

Tactic:
linear_combination h₂

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

Goal state before:
pp: n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)

Tactic:
apply _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))

Goal state after:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := ⋯
hfrob : map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) ((expand ℤ p) Q)
⊢ minpoly ℤ μ ∣ (expand ℤ p) Q
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
⊢ IsIntegral K ⟨x, ⋯⟩

Tactic:
apply (isIntegral_algebraMap_iff hST).mp

Goal state after:
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
⊢ IsIntegral K ((algebraMap (↥K[x]) S) ⟨x, ⋯⟩)
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr 1) i)

Tactic:
← pow_zero B.gen,

Goal state after:
case refine_1
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
⊢ IsIntegral R ((B.basis.repr (B.gen ^ 0)) i)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
have hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
    cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by lia) hirr

Goal state after:
p : ℕ
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K)
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ (↑q).arg ≠ (-ζ).arg

Tactic:
rw [Complex.arg_ofReal_of_nonneg hq.le, Ne, eq_comm]

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
hfor : ∀ ζ' ∈ primitiveRoots n ℂ, ‖↑q - ζ'‖ ≤ q + 1
ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)
hζ : IsPrimitiveRoot ζ n
⊢ ¬(-ζ).arg = 0
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a : R
⊢ ∀ ⦃a₂ : R⦄, ψ.mulShift a = ψ.mulShift a₂ → a = a₂

Tactic:
b

Goal state after:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
⊢ ψ.mulShift a = ψ.mulShift b → a = b
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
val✝ : Infinite K
⊢ (X ^ Nat.card K - X).Splits

Tactic:
rw [← Polynomial.splits_neg_iff]
    simpa [Nat.card_eq_zero_of_infinite, pow_zero, neg_sub] using Splits.X_sub_C (1 : K)

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a, ψ a = 0

Tactic:
by
  rcases ne_one_iff.1 hψ with ⟨b, hb⟩
  have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a :=
    Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl
  simp_rw [map_add_eq_mul] at h₁
  have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
  rw [← Finset.mul_sum, h₂] at h₁
  exact eq_zero_of_mul_eq_self_left hb h₁

Goal state after:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : CommRing R
inst✝² : Fintype R
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ gaussSum χ 1 = 0

Tactic:
simpa [gaussSum] using MulChar.sum_eq_zero_of_ne_one hχ

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ (auxDFT fun j ↦ Φ (-j)) = fun k ↦ auxDFT Φ (-k)

Tactic:
by
  ext1 k; simpa only [auxDFT] using
    Fintype.sum_equiv (Equiv.neg _) _ _ (fun j ↦ by rw [Equiv.neg_apply, neg_mul_neg])

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: case hpq
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ 1 - k * p + ∑ i ∈ s, p = 1

pp: case h₂.hq
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ 1 - k * p

pp: case h₂.hp
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ ∀ i ∈ s, 0 ≤ p

Tactic:
· simp only [sum_const, nsmul_eq_mul]
                ring

Goal state after:
case h₂.hq
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ 0 ≤ 1 - k * p

case h₂.hp
ι : Type u_1
A : ι → Type u_2
inst✝² : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝¹ : DecidableEq ι
p : ℝ
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : ↑(#s) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : A i → (a : ι) → A a := ⋯
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ⋯
hk' : 0 ≤ 1 - k * p
⊢ ∀ i ∈ s, 0 ≤ p
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ x * y * z = x * (y * z)

Tactic:
AlgebraOfCoalgebra.mul_def,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : Coalgebra 𝕜 E
x y z : E
⊢ (adjoint comul) ((adjoint comul) (x ⊗ₜ[𝕜] y) ⊗ₜ[𝕜] z) = (adjoint comul) (x ⊗ₜ[𝕜] (adjoint comul) (y ⊗ₜ[𝕜] z))