mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Tuple.Sort

Goal state before:
pp: n : ℕ
α : Type u_1
j : Fin n
f : Fin n → α
inst✝¹ : Preorder α
a : α
inst✝ : DecidableLT α
h_sorted : Antitone f
⊢ ∀ (i j : Fin n), j ≤ i → a < f i → a < f j

Tactic:
grind [Antitone]

Goal state after:
Module: Mathlib.Analysis.Matrix.Spectrum

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
this : hA.eigenvalues₀ = hB.eigenvalues₀
⊢ hA.eigenvalues = hB.eigenvalues

Tactic:
unfold eigenvalues

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A B : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : A.charpoly = B.charpoly
this : hA.eigenvalues₀ = hB.eigenvalues₀
⊢ (fun i ↦ hA.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)) = fun i ↦
    hB.eigenvalues₀ ((Fintype.equivOfCardEq ⋯).symm i)
Module: Mathlib.Analysis.Matrix.PosDef

Goal state before:
pp: m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
⊢ ∀ (x y z : n → 𝕜), M *ᵥ z ⬝ᵥ star (x + y) = M *ᵥ z ⬝ᵥ star x + M *ᵥ z ⬝ᵥ star y

Tactic:
by simp only [star_add, dotProduct_add, forall_const]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
μ : 𝕜
hμ : μ ≠ 0
hT : IsCompactOperator ⇑((↑T).restrict ⋯)
⊢ FiniteDimensional 𝕜 ↥(eigenspace (↑T) μ)

Tactic:
restrict_eigenspace,

Goal state after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
μ : 𝕜
hμ : μ ≠ 0
hT : IsCompactOperator ⇑(μ • LinearMap.id)
⊢ FiniteDimensional 𝕜 ↥(eigenspace (↑T) μ)
Module: Mathlib.Analysis.Matrix.Order

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).PosSemidef

Tactic:
posSemidef_iff_dotProduct_mulVec

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
ι : Type u_3
A B : Matrix ι ι 𝕜
hA : A.PosSemidef
hB : B.PosSemidef
x : ι →₀ 𝕜
hAs : (A.submatrix Subtype.val Subtype.val).PosSemidef
hBs : (B.submatrix Subtype.val Subtype.val).PosSemidef
⊢ (A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val).IsHermitian ∧
    ∀ (x_1 : ↥x.support → 𝕜),
      0 ≤ star x_1 ⬝ᵥ A.submatrix Subtype.val Subtype.val ⊙ B.submatrix Subtype.val Subtype.val *ᵥ x_1
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
F : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ eLpNorm (fun x ↦ ‖↑↑f x‖ ^ 2) 1 μ < ∞

Tactic:
by
  have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp
  rw [eLpNorm_norm_rpow f zero_lt_two, one_mul, h_two]
  exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.eLpNorm_ne_top f)

Goal state after:
Module: Mathlib.MeasureTheory.Function.ContinuousMapDense

Goal state before:
pp: α : Type u_1
inst✝⁸ : TopologicalSpace α
inst✝⁷ : NormalSpace α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : BorelSpace α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝³ : NormedSpace ℝ E
inst✝² : R1Space α
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : μ.Regular
hp : p ≠ ∞
f : α → E
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
H :
  ∃ g,
    eLpNorm (f - g) p μ ≤ ε ∧
      Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ ∧ HasCompactSupport g
⊢ ∃ g,
    HasCompactSupport g ∧
      eLpNorm (f - g) p μ ≤ ε ∧ Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g ∧ MemLp g p μ

Tactic:
rcases H with ⟨g, hg, g_cont, g_mem, g_support⟩
    exact ⟨g, g_support, hg, g_cont, g_mem⟩

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
⊢ ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)

Tactic:
intro b

Goal state after:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
K : Submodule 𝕜 E
hK : CompleteSpace ↥K
b : Bool
⊢ CompleteSpace ↥(bif b then K else Kᗮ)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: case h₂
ι : 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✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedAddCommGroup D
inst✝⁵ : NormedSpace ℝ D
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth : ∀ N ≤ n, ∀ (x : D), ‖iteratedFDeriv ℝ N g x‖ ≤ C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  ‖iteratedFDeriv ℝ n (fun y ↦ ((ContinuousLinearMap.bilinearRestrictScalars ℝ B) (f y)) (g y)) x‖ ≤
    ‖ContinuousLinearMap.bilinearRestrictScalars ℝ B‖ *
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv ℝ i (⇑f) x‖ * ‖iteratedFDeriv ℝ (n - i) g x‖
this : ∑ _x ∈ Finset.range (n + 1), 1 = ↑n + 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ n.choose i ≤ n.choose (n / 2)

Tactic:
exact i.choose_le_middle n

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
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : IsTopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : FirstCountableTopology W
he : Continuous[inst✝⁵, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (L p.1) p.2
f : V → E
hf : Integrable f μ
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)

Tactic:
apply continuous_of_dominated
  · exact fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1
  · exact fun w ↦ ae_of_all _ fun v ↦ le_of_eq (Circle.norm_smul _ _)
  · exact hf.norm
  · filter_upwards with v
    fun_prop

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
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : IsTopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : AddChar 𝕜 𝕊
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : FirstCountableTopology W
he : Continuous[inst✝⁵, _] ⇑e
hL : Continuous[instTopologicalSpaceProd, inst✝⁵] fun p ↦ (L p.1) p.2
f : V → E
hf : Integrable f μ
⊢ Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (fourierIntegral e μ L f)

Tactic:
by
  apply continuous_of_dominated
  · exact fun w ↦ ((fourierIntegral_convergent_iff he hL w).2 hf).1
  · exact fun w ↦ ae_of_all _ fun v ↦ le_of_eq (Circle.norm_smul _ _)
  · exact hf.norm
  · filter_upwards with v
    fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
m : ℕ
⊢ ↑m ≤ N → Integrable (iteratedFDeriv ℝ m fun v ↦ fourierPowSMulRight L f v k) μ

Tactic:
hm

Goal state after:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ
k n : ℕ
hk : ↑k ≤ K
hn : ↑n ≤ N
w : W
m : ℕ
hm : ↑m ≤ N
⊢ Integrable (iteratedFDeriv ℝ m fun v ↦ fourierPowSMulRight L f v k) μ
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: c y : ℝ
x✝ : y ∈ Iic 0
⊢ rexp c - rexp (id y) ≤ rexp c

Tactic:
sub_le_self_iff

Goal state after:
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ rexp (id y)
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 *

Goal state after:
α : 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 : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1) volume

Tactic:
← integrableOn_Icc_iff_integrableOn_Ioc

Goal state after:
case left
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Icc 0 1) volume
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ HasFDerivAt (fun x i ↦ ↑polarCoord.symm (x i))
    (ContinuousLinearMap.pi fun i ↦ fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i) p

Tactic:
hasFDerivAt_pi

Goal state after:
ι : Type u_1
inst✝ : Finite ι
p : ι → ℝ × ℝ
this : Fintype ι
⊢ ∀ (i : ι), HasFDerivAt (fun x ↦ ↑polarCoord.symm (x i)) (fderivPolarCoordSymm (p i) ∘SL ContinuousLinearMap.proj i) p
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℂ
hb : 0 < b.re
⊢ ∀ {b : ℂ}, 0 < b.re → b ≠ 0

Tactic:
intro b

Goal state after:
b✝ : ℂ
hb : 0 < b✝.re
b : ℂ
⊢ 0 < b.re → b ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑0

Tactic:
by norm_cast; linarith

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

Goal state before:
pp: case a
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
| ↑1 / 2

Tactic:
← ofReal_ofNat,

Goal state after:
case a
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
| ↑1 / ↑2
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: b : ℝ
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ 2) = √(π / b) / 2

Tactic:
rcases le_or_gt b 0 with (hb | hb)
  · rw [integral_undef, sqrt_eq_zero_of_nonpos, zero_div]
    · exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb
    · rwa [← IntegrableOn, integrableOn_Ioi_exp_neg_mul_sq_iff, not_lt]
  rw [← RCLike.ofReal_inj (K := ℂ), ← integral_ofReal, ← RCLike.algebraMap_eq_ofReal,
    coe_algebraMap]
  convert! integral_gaussian_complex_Ioi (by rwa [ofReal_re] : 0 < (b : ℂ).re)
  · simp
  · rw [sqrt_eq_rpow, ← ofReal_div, ofReal_div, ofReal_cpow]
    · simp
    · exact (div_pos pi_pos hb).le

Goal state after:
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 → ℝ := ⋯
⊢ ∫ (x : V), φ x = 1

Tactic:
rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]

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) * (π / π ^ 2) ^ (↑(finrank ℝ V) / 2) = 1
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
s : ℝ
f : 𝓢'(E, F)
⊢ 𝓕 ((besselPotential E F s) f) = (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f)

Tactic:
by
  simp [besselPotential, fourierMultiplierCLM]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i ↦ ‖mFourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : UnitAddTorus d), ‖↑↑f t‖ ^ 2)

Tactic:
by
  simpa only [← RCLike.inner_apply', inner_self_eq_norm_sq, ← integral_re
    (L2.integrable_inner f f)] using RCLike.hasSum_re ℂ (hasSum_prod_mFourierCoeff f f)

Goal state after:
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : ι → 𝕜
a : 𝕜
⊢ ⟪f, const ι a⟫_[𝕜] = a * ∑ i, (starRingEnd 𝕜) (f i)

Tactic:
by simp [wInner_one_eq_sum, mul_sum]

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

Goal state before:
pp: case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₂ * ψ₁⁻¹ ≠ 1
⊢ 𝔼 i, inner R (ψ₁ i) (ψ₂ i) = 0

Tactic:
RCLike.inner_apply,

Goal state after:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₂ * ψ₁⁻¹ ≠ 1
⊢ 𝔼 i, ψ₂ i * (starRingEnd R) (ψ₁ i) = 0
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))

Tactic:
obtain ⟨ι, inst, n, h₁, h₂⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' (Additive G)

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Finite G
ι : Type
inst : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (Additive G ≃+ ⨁ (i : ι), ZMod (n i))
⊢ ∃ ι x n, (∀ (i : ι), 1 < n i) ∧ Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
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(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
this : ∀ (x : ℝ), ‖e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ⨆ x, ‖(e * g) ↑x‖ = ⨆ x, ‖g ↑x‖

Tactic:
mul_apply,

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 := ⋯ }
this : ∀ (x : ℝ), ‖e x‖ = 1
K : Compacts ℝ
g : C(ℝ, ℂ)
⊢ ⨆ x, ‖e ↑x * g ↑x‖ = ⨆ x, ‖g ↑x‖
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) ↔ ∀ (x : ℕ), (↑ζ • f') x = g' x

Tactic:
apply forall_congr'

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ∀ (a : ℕ), a > 0 → ∑ i ∈ a.divisors, f i = g a ↔ (↑ζ • f') a = g' a
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' := ⋯ }
⊢ (∀ (x : ℕ), (μ • g') x = f' x) ↔ ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n

Tactic:
apply forall_congr'

Goal state after:
R : Type u_1
inst✝ : AddCommGroup R
f g : ℕ → R
f' : ArithmeticFunction R := ⋯
g' : ArithmeticFunction R := ⋯
⊢ ∀ (a : ℕ), (μ • g') a = f' a ↔ a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
⊢ (∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
apply forall_congr'

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
⊢ ∀ (a : ℕ),
    a > 0 → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
Module: Mathlib.NumberTheory.ArithmeticFunction.Moebius

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ (∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔
    ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n

Tactic:
apply forall_congr'

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
f g : ℕ → R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
⊢ ∀ (a : ℕ),
    a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔
      a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x

Tactic:
· convert! congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
    -- This `have` unfolds the function composition in `Equiv.summable_iff`.

    -- This `have` unfolds the function composition in `Equiv.summable_iff`.
    have : Summable fun (c : ℤ) => f.comp (ContinuousMap.addRight (Equiv.addRight 1 c • p)) :=
      (Equiv.addRight (1 : ℤ)).summable_iff.mpr h
    simp_rw [← tsum_apply h, ← tsum_apply this]
    simp [Equiv.coe_addRight, comp_apply, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
⊢ (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) (x + p) =
    (∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p))) x
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 + i w‖

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:
· rw [← sub_neg_eq_add]
      refine le_trans ?_ (norm_sub_norm_le _ _)
      rw [le_sub_iff_add_le, norm_neg]
      refine le_trans ?_ hv.le
      rw [add_le_add_iff_left, hw'_nm, ← div_div]
      refine (div_le_one <| norm_pos_iff.mpr hw_ne).mpr ?_
      refine le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| ?_) hw_bd
      exact (mul_pos (zero_lt_two' ℝ) hδ1).le

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
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‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d R ∣ ∑ i ∈ range n, X ^ i

Tactic:
suffices cyclotomic d ℤ ∣ ∑ i ∈ Finset.range n, X ^ i by
    simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
      map_dvd (Int.castRingHom R) this
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← prod_cyclotomic_eq_geom_sum hn]
  apply Finset.dvd_prod_of_mem
  simp [hd, hdn, hn.ne']

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
n : ℕ
inst✝ : NeZero n
x : R
⊢ (∃ a, a ∣ n ∧ x ∈ primitiveRoots a R) → x ^ n = 1

Tactic:
· rintro ⟨a, ⟨d, hd⟩, ha⟩
    have hazero : 0 < a := Nat.pos_of_ne_zero fun ha₀ ↦ by simp_all
    rw [mem_primitiveRoots hazero] at ha
    rw [hd, pow_mul, ha.pow_eq_one, one_pow]

Goal state after: