mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℝ), f |x| = (∫ (x : ℝ) in Iic 0, f |x|) + ∫ (x : ℝ) in Ioi 0, f |x|

Tactic:
← setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,

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 : ℝ), f |x| = ∫ (x : ℝ) in Iic 0 ∪ Ioi 0, f |x|
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: a : ℂ
ha : a.re < 0
c : ℝ
⊢ IntegrableOn (fun x ↦ Complex.exp (a * ↑x)) (Ioi c) volume

Tactic:
by
  refine (integrable_norm_iff ?_).mp ?_
  · apply Continuous.aestronglyMeasurable
    fun_prop
  · simpa [Complex.norm_exp] using!
      (integrableOn_Ioi_comp_mul_left_iff (fun x => exp (-x)) c (a := -a.re) (by simpa)).mpr <|
        integrableOn_exp_neg_Ioi _

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

Goal state before:
pp: b : ℂ
c T : ℝ
⊢ rexp (-(b * (↑T + ↑c * I) ^ 2).re) = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))

Tactic:
← re_add_im b

Goal state after:
b : ℂ
c T : ℝ
⊢ rexp (-((↑b.re + ↑b.im * I) * (↑T + ↑c * I) ^ 2).re) =
    rexp (-((↑b.re + ↑b.im * I).re * T ^ 2 - 2 * (↑b.re + ↑b.im * I).im * c * T - (↑b.re + ↑b.im * I).re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case inl
b : ℝ
hb : b ≤ 0
⊢ 0 = √(π / b)

pp: case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume

Tactic:
sqrt_eq_zero_of_nonpos

Goal state after:
case inl
b : ℝ
hb : b ≤ 0
⊢ 0 = 0

case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x ↦ rexp (-b * x ^ 2)) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

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

Tactic:
have t2 : -(s + 1).re < n := by rw [add_re, one_re]; linarith

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

Goal state before:
pp: case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1) / s)

Tactic:
div_eq_mul_inv _ s,

Goal state after:
case succ
s✝ : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (GammaAux n s)
s : ℂ
⊢ GammaAux n ((starRingEnd ℂ) s + 1) / (starRingEnd ℂ) s = (starRingEnd ℂ) (GammaAux n (s + 1) * s⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)
⊢ ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * (↑r * ↑t) ^ (a - 1) * cexp (-(↑r * ↑t)) =
    1 / ↑r * ∫ (t : ℝ) in Ioi 0, (1 / ↑r) ^ (a - 1) * ↑t ^ (a - 1) * cexp (-↑t)

Tactic:
by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]

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
f : 𝓢(V, E)
x : V
⊢ fderiv ℝ (𝓕 ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) ⇑f) x

Tactic:
rw [fderiv_fourier f.integrable]

Goal state after:
𝕜 : 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)
x : V
⊢ Integrable (fun v ↦ ‖v‖ * ‖f v‖) volume
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ ((TemperedDistribution.smulLeftCLM F g) f) u = 0

Tactic:
apply hf ((SchwartzMap.smulLeftCLM ℂ g) u)

Goal state after:
E : Type u_5
F : Type u_6
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
s : Set E
hf : IsVanishingOn (⇑f) s
g : E → ℂ
hg : Function.HasTemperateGrowth g
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ tsupport ⇑((SchwartzMap.smulLeftCLM ℂ g) u) ⊆ s
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℂ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul ℂ F
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
⊢ smulLeftCLM F (g₁ + g₂) = smulLeftCLM F g₁ + smulLeftCLM F g₂

Tactic:
ext f u
  simp [SchwartzMap.smulLeftCLM_add hg₁ hg₂]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
⊢ Orthonormal ℂ (mFourierLp 2)

Tactic:
by
  rw [orthonormal_iff_ite]
  intro m n
  simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]
  split_ifs with h
  · simpa only [h, add_neg_cancel, mFourier_zero, probReal_univ, one_smul] using!
      integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)
  rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod]
  obtain ⟨i, hi⟩ := Function.ne_iff.mp h
  apply Finset.prod_eq_zero (Finset.mem_univ i)
  simpa only [eq_false_intro hi, if_false, ContinuousMap.inner_toLp, ← fourier_neg,
    ← fourier_add] using! (orthonormal_iff_ite.mp <| orthonormal_fourier) (m i) (n i)

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(E, F)
g : 𝓢(E, ℂ)
⊢ (𝓕 ((toTemperedDistributionCLM E F volume) f)) g = ((toTemperedDistributionCLM E F volume) (𝓕 f)) g

Tactic:
simpa using integral_fourier_smul_eq g f

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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
m : E
⊢ MemSobolev (-1 + s) 2 (∂_{m} f)

Tactic:
← memSobolev_besselPotential_iff,

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 : E
⊢ MemSobolev s 2 ((besselPotential E F (-1)) (∂_{m} f))
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 : ℝ
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
⊢ MemSobolev (-2 + s) 2 (Δ f)

Tactic:
← memSobolev_besselPotential_iff,

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
⊢ MemSobolev s 2 ((besselPotential E F (-2)) (Δ f))
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ 1) = -1

Tactic:
pow_one,

Goal state after:
case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ p = -1
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.PrimitiveRoots

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

Tactic:
refine ⟨fun hi ↦ ?_, h.pow_of_coprime i⟩

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
h0 : 0 < k
i : ℕ
hi : IsPrimitiveRoot (ζ ^ i) k
⊢ i.Coprime k
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < k
⊢ ζ ^ l ≠ 1

Tactic:
h.eq_orderOf

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
hk : 0 < k
h : IsPrimitiveRoot ζ k
l : ℕ
hl' : 0 < l
hl : l < orderOf ζ
⊢ ζ ^ l ≠ 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ k
⊢ IsPrimitiveRoot (ζ ^ p) (k / p)

Tactic:
h.eq_orderOf

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
p : ℕ
hp : p ≠ 0
hdiv : p ∣ orderOf ζ
⊢ IsPrimitiveRoot (ζ ^ p) (orderOf ζ / p)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

Tactic:
cyclotomic'

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

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

Tactic:
cyclotomic'

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

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

Tactic:
cyclotomic'

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

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

Tactic:
h.eq_orderOf

Goal state after:
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 ζ k
hf : Injective ⇑f
⊢ ∀ (l : ℕ), f ζ ^ l = 1 → orderOf ζ ∣ l
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 : ℕ), ζ ^ l = 1 → k ∣ l

Tactic:
h.eq_orderOf

Goal state after:
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 : ℕ), ζ ^ l = 1 → orderOf (f ζ) ∣ l
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ∉ d.divisors

pp: case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0

Tactic:
· exact fun hk => h.2.not_ge <| Nat.divisor_le hk

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ n ≠ 0
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ orderOf ζ = n

Tactic:
h.eq_orderOf

Goal state after:
R : Type u_4
inst✝² : CommRing R
ζ : Rˣ
inst✝¹ : IsDomain R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ orderOf ζ = orderOf ζ
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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • f v) - ∫ (v : V), 𝐞 (-⟪v, w⟫) • g v‖ ≤ ∫ (x : V), ‖f x - g x‖

Tactic:
simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
      ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
      ← smul_sub, ← Pi.sub_apply]

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
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
w : V
hI : ‖(∫ (v : V), 𝐞 (-⟪v, w⟫) • g v) - 0‖ < ε / 2
⊢ ‖∫ (a : V), 𝐞 (-⟪a, w⟫) • (f - g) a ∂volume‖ ≤ ∫ (x : V), ‖(f - g) x‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
| h.choose % n

Tactic:
2

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
f : S ≃ₐ[R] S
h : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
| n
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ a.Coprime p

Tactic:
by
  apply Nat.Coprime.symm
  rw [hprime.1.coprime_iff_not_dvd]
  intro h
  replace h := (ZMod.natCast_eq_zero_iff a p).2 h
  rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot
  by_cases hone : n = 1
  · simp only [hone, cyclotomic_one, zero_sub, coeff_one_zero, coeff_X_zero, neg_eq_zero,
      one_ne_zero, coeff_sub] at hroot
  rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt
    (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot
  exact one_ne_zero hroot

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

Goal state before:
pp: R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p ^ 1 * m) R = cyclotomic m R ^ (p ^ 1 - p ^ (1 - 1))

Tactic:
pow_one,

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
x✝ : 0 < 1
⊢ cyclotomic (p * m) R = cyclotomic m R ^ (p - p ^ (1 - 1))
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : CommRing K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1

Tactic:
rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_natCast, h]

Goal state after:
case h
K : Type u_1
inst✝¹ : CommRing K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * (0 * X ^ (q - 1) - 1) = 1
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ 2 * n = orderOf (-ζ)

Tactic:
rw [neg_eq_neg_one_mul, (Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime]

Goal state after:
n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ 2 * n = orderOf (-1) * orderOf ζ

n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ (orderOf (-1)).Coprime (orderOf ζ)
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
⊢ Function.Injective ψ.mulShift

Tactic:
by
  intro a b h
  apply_fun fun x => x * mulShift ψ (-b) at h
  simp only [mulShift_mul, mulShift_zero, add_neg_cancel] at h
  simpa [← sub_eq_add_neg, sub_eq_zero] using (hψ · h)

Goal state after:
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ X ^ p ^ 1 = X ^ Fintype.card (ZMod p)

Tactic:
pow_one,

Goal state after:
p✝ : ℕ
inst✝ : Fact (Nat.Prime p✝)
n✝ p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
⊢ X ^ p = X ^ Fintype.card (ZMod p)
Module: Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ n ∣ Monoid.exponent ↥(rootsOfUnity n M)

Tactic:
h.eq_orderOf

Goal state after:
case refine_2
M : Type u_1
inst✝² : CommMonoid M
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity M n
ζ : M
h : IsPrimitiveRoot ζ n
⊢ orderOf ζ ∣ Monoid.exponent ↥(rootsOfUnity n M)
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: n : ℕ
hn : n % 2 = 1
help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)

Tactic:
exact help _ (Nat.mod_lt n (by lia)) <| (Nat.mod_mod_of_dvd n (by lia : 2 ∣ 4)).trans hn

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n) * χ ^ 1 = χ

Tactic:
pow_one,

Goal state after:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n) * χ = χ
Module: Mathlib.NumberTheory.DirichletCharacter.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
⊢ χ ∈ annihilator R H ↔ ∀ x ∈ Submonoid.closure H, χ ↑x = 1

Tactic:
simp only [annihilator, MonoidHom.mem_ker, MulChar.domRestrictHom_apply,
    MulChar.domRestrict_eq_one_iff]

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
H : Set (ZMod n)ˣ
χ : DirichletCharacter R n
⊢ (∀ (x : (↥(Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)))ˣ), χ ↑↑x = 1) ↔
    ∀ x ∈ Submonoid.closure H, χ ↑x = 1
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ ^ 1 = χ (↑p ^ 0) * gaussSum χ ψ

Tactic:
pow_one,

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
p : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
⊢ gaussSum χ ψ = χ (↑p ^ 0) * gaussSum χ ψ
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) = χ (↑p ^ n)

Tactic:
apply mul_right_cancel₀ this

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ.IsQuadratic
ψ : AddChar R R'
p n : ℕ
fp : Fact (Nat.Prime p)
hch : CharP R' p
hp : IsUnit ↑p
hp' : p ≠ 2
hg : gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
this : gaussSum χ ψ ≠ 0
⊢ (gaussSum χ ψ ^ 2) ^ (p ^ n / 2) * gaussSum χ ψ = χ (↑p ^ n) * gaussSum χ ψ
Module: Mathlib.Analysis.Fourier.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ f : ZMod N → ℂ
hf : Function.Odd f
⊢ Function.Odd (𝓕 f)

Tactic:
simp only [Function.Odd, ← congr_fun (dft_comp_neg f), funext hf, ← Pi.neg_apply, map_neg,
      implies_true]

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

Goal state before:
pp: case hxy.e'_6.a
ι : 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 := update x i
hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t)
hF₀ : Measurable fun t ↦ f (X t)
k : ℝ := ↑(#s)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ Disjoint {j} {i}

Tactic:
· rw [Finset.disjoint_singleton]
                  exact fun h ↦ hi (h ▸ hj)

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
S : E →ₗ[𝕜] F
⊢ (S ∘ₗ LinearMap.adjoint S).IsPositive

Tactic:
by
  simpa using! LinearMap.isPositive_one.conj_adjoint S

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace ℂ E'
T : E' →L[ℂ] E'
⊢ T.IsPositive ↔ ∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ

Tactic:
simp [← isPositive_toLinearMap_iff, LinearMap.isPositive_iff_complex]

Goal state after: