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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
n₁ n₂ : ℕ∞
K₁ K₂ : Compacts E
H : ¬(n₂ ≤ n₁ ∧ K₁ ≤ K₂)
⊢ monoCLM 𝕜 = 0

Tactic:
by
  ext; simp [H]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: A : Type u_2
inst✝⁹ : NonUnitalNormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : CStarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ ‖abs a‖ = ‖a‖

Tactic:
by
  rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, sq, ← CStarRing.norm_star_mul_self,
    (abs_nonneg _).star_eq, CFC.abs_mul_abs, CStarRing.norm_star_mul_self]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
F' : Type u_4
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedSpace ℝ 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'
n n₁ n₂ k✝ : ℕ∞
K K₁ K₂ : Compacts E
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
G : Type u_8
inst✝⁹ : NormedAlgebra ℝ 𝕜
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace 𝕜 F₁
inst✝⁶ : NormedSpace ℝ F₁
inst✝⁵ : NormedAddCommGroup F₂
inst✝⁴ : NormedSpace 𝕜 F₂
inst✝³ : NormedSpace ℝ F₂
inst✝² : NormedAddCommGroup F₃
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℝ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
g : E → F₂
hg : ContDiff ℝ (↑n) g
k : ℕ
hk : ↑k ≤ n
hcont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun x ↦
    (Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖
C₀ : ℝ
hC₀ : ∀ x ∈ ↑K, ‖(Finset.range (k + 1)).sup' ⋯ fun i ↦ ‖iteratedFDeriv ℝ i g x‖‖ ≤ C₀
hgC₀ : ∀ i ≤ k, ∀ x ∈ K, ‖iteratedFDeriv ℝ i g x‖ ≤ ‖C₀‖
φ : 𝓓^{n}_{K}(E, F₁)
x : E
hx : x ∈ K
⊢ ‖iteratedFDeriv ℝ k (fun y ↦ (B (φ y)) (g y)) x‖ ≤
    ‖B‖ * ∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * ‖iteratedFDeriv ℝ i (⇑φ) x‖ * ‖iteratedFDeriv ℝ (k - i) g x‖

Tactic:
by
          simpa using (B.bilinearRestrictScalars ℝ).norm_iteratedFDeriv_le_of_bilinear
            φ.contDiff hg x (mod_cast hk)

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Bases

Goal state before:
pp: case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ ↑(b.proj A) x ∈ Submodule.span 𝕜 (↑b '' ↑A)

Tactic:
rw [ContinuousLinearMap.coe_coe, proj_apply]

Goal state after:
case a
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
β : Type u_3
L : SummationFilter β
b : GeneralSchauderBasis β 𝕜 X L
A : Finset β
x : X
⊢ ∑ i ∈ A, (b.coord i) x • ↑b i ∈ Submodule.span 𝕜 (↑b '' ↑A)
Module: Mathlib.Analysis.InnerProductSpace.l2Space

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : (span 𝕜 (Set.range v))ᗮ = ⊥
⊢ ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure

Tactic:
by rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i ↦ ↑(fourierBasis.repr f) i • fourierBasis i) f

Tactic:
exact HilbertBasis.hasSum_repr fourierBasis f

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

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ inner ℂ (fourierLp 2 m) (fourierLp 2 n) = Pi.single n 1 m

Tactic:
(orthonormal_fourier (hT := hT)).2 hmn

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
n m : ℤ
hmn : m ≠ n
⊢ 0 = Pi.single n 1 m
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
⊢ ContDiff ℝ ∞ fun x ↦ 0

Tactic:
by exact contDiff_const

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

Goal state before:
pp: case e_6
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 F
f : 𝓢(E, F)
a b x : E
⊢ x - b - a = x - (a + b)

Tactic:
exact (sub_add_eq_sub_sub_swap x a b).symm

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter f l μ

Tactic:
by
  obtain ⟨C, hC⟩ := hf.bound
  obtain ⟨s, hsl, hsm, hfg, hf, hg⟩ :=
    (hC.smallSets.and <| hfm.eventually.and hg.eventually).exists_measurable_mem_of_smallSets
  refine ⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩
  refine (ae_restrict_mem hsm).mono fun x hx ↦ ?_
  exact (hfg x hx).trans (le_abs_self _)

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

Goal state before:
pp: V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ ‖𝓕 (↑↑f) x‖ ≤ ‖f‖

Tactic:
rw [Real.fourier_eq]

Goal state after:
V : Type u_1
W : Type u_2
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : InnerProductSpace ℝ V
inst✝⁷ : MeasurableSpace V
inst✝⁶ : BorelSpace V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : InnerProductSpace ℝ W
inst✝³ : MeasurableSpace W
inst✝² : BorelSpace W
inst✝¹ : FiniteDimensional ℝ W
inst✝ : FiniteDimensional ℝ V
f : ↥(Lp E 1 volume)
x : V
⊢ ‖∫ (v : V), 𝐞 (-⟪v, x⟫) • ↑↑f v‖ ≤ ‖f‖
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ × ℝ) → ℝ≥0∞
x : ι → ℝ × ℝ
hx : x ∈ Set.univ.pi fun x ↦ polarCoord.target
⊢ ((∏ i, ENNReal.ofReal (x i).1) * f fun i ↦ ↑polarCoord.symm (x i)) =
    ENNReal.ofReal |(fderivPiPolarCoordSymm x).det| * f fun i ↦ ↑polarCoord.symm (x i)

Tactic:
simp_rw [det_fderivPiPolarCoordSymm, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦
    abs_nonneg _), abs_fst_of_mem_pi_polarCoord_target hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case zero
s : ℂ
⊢ ∀ (s : ℂ), ((starRingEnd ℂ) s).GammaIntegral = (starRingEnd ℂ) s.GammaIntegral

Tactic:
exact GammaIntegral_conj

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

Goal state before:
pp: V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢(V, F)
x : V
⊢ ∫ (v : V), ‖𝐞 (-inner ℝ v x) • f v‖ = ‖f.toLp 1 volume‖

Tactic:
by simp [norm_toLp_one]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (x : UnitAddTorus d), f x = ∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}, f fun i ↦ ↑(x i)

Tactic:
convert! lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm

Goal state after:
case e'_2.e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
e_2✝ : MeasureSpace.pi.toMeasurableSpace = MeasurableSpace.pi
⊢ volume = Measure.map (⇑(measurableEquivPiIoc a).symm) (Measure.comap Subtype.val volume)

case e'_3
d : Type u_1
inst✝ : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ (∫⁻ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}, f fun i ↦ ↑(x i)) =
    ∫⁻ (a_1 : { x // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f ((measurableEquivPiIoc a).symm a_1) ∂Measure.comap Subtype.val volume
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f g : ι → 𝕜
⊢ ⟪f, g⟫_[𝕜] = ⟪toLp 2 f, toLp 2 g⟫_𝕜

Tactic:
by
  simp [PiLp.inner_apply, wInner]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f g : PiLp 2 fun _i ↦ 𝕜
⊢ ⟪f, g⟫_𝕜 = ⟪f.ofLp, g.ofLp⟫_[𝕜]

Tactic:
by
  simp [PiLp.inner_apply, wInner]

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

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

pp: case h'f
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Integrable (𝓕 (⇑f ⋆[B, volume] ⇑g)) volume

Tactic:
· exact f.integrable.integrable_convolution B g.integrable

Goal state after:
case h'f
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : InnerProductSpace ℝ E
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedAddCommGroup F₁
inst✝⁷ : NormedSpace ℂ F₁
inst✝⁶ : NormedAddCommGroup F₂
inst✝⁵ : NormedSpace ℂ F₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : CompleteSpace F₃
inst✝¹ : CompleteSpace F₁
inst✝ : CompleteSpace F₂
B : F₁ →L[ℂ] F₂ →L[ℂ] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
x : E
⊢ Integrable (𝓕 (⇑f ⋆[B, volume] ⇑g)) volume
Module: Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ ∑ ψ, ψ a = if a = 0 then ↑(Fintype.card α) else 0

Tactic:
by
  simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

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 (s - 1) 2 (∂_{m} f)

Tactic:
SubNegMonoid.sub_eq_add_neg s 1,

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 + -1) 2 (∂_{m} f)
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: f : C(ℝ, ℂ)
hf : ∀ (K : Compacts ℝ), Summable fun n ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖
m : ℤ
e : C(ℝ, ℂ) := (fourier (-m)).comp { toFun := QuotientAddGroup.mk, continuous_toFun := ⋯ }
neK : ∀ (K : Compacts ℝ) (g : C(ℝ, ℂ)), ‖ContinuousMap.restrict (↑K) (e * g)‖ = ‖ContinuousMap.restrict (↑K) g‖
eadd : ∀ (n : ℤ), e.comp (ContinuousMap.addRight ↑n) = e
⊢ ∑' (n : ℤ), ∫ (x : ℝ) in 0..1, ((e * f).comp (ContinuousMap.addRight ↑n)) x = ∫ (x : ℝ), e x * f x

Tactic:
by
      suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq
      apply integrable_of_summable_norm_Icc
      convert! hf ⟨Icc 0 1, isCompact_Icc⟩ using 1
      simp_rw [mul_comp] at eadd ⊢
      simp_rw [eadd]
      exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _

Goal state after:
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n k : ℕ+
⊢ k.Coprime m → m.gcd (k * n) = m.gcd n

Tactic:
intro h; iterate 2 rw [gcd_comm]; symm
  apply Coprime.gcd_mul_left_cancel _ h

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

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ = ‖(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) (-x)‖

Tactic:
ContinuousMap.comp_apply,

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x ↦ |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ }) =O[atTop] fun x ↦ |x| ^ (-b)
h2 :
  ((fun x ↦ ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x ↦ |x| ^ (-b)
this : (fun x ↦ |x| ^ (-b)) ∘ Neg.neg = fun x ↦ |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ = ‖f ({ toFun := fun a ↦ -a, continuous_toFun := ⋯ } (-x))‖
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖(f.comp (ContinuousMap.addRight x)) y‖ = ‖f (y + x)‖

Tactic:
ContinuousMap.comp_apply,

Goal state after:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : ↑K ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ ↑K
⊢ ‖f ((ContinuousMap.addRight x) y)‖ = ‖f (y + x)‖
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case pos.convert_2.refine_2
n : ℕ
hn : n ≠ 0
i : ℕ
h : i < n
hin : i.Coprime n
h₂ : i * 2 ≤ n * 1
⊢ Real.pi * (↑i * 2 / ↑n) ≤ Real.pi

Tactic:
exact mul_le_of_le_one_right Real.pi_pos.le
      ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁷ : CommMonoid M
inst✝⁶ : CommMonoid N
inst✝⁵ : DivisionCommMonoid G
k l : ℕ
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
μ : S
n : ℕ
hμ : IsPrimitiveRoot μ n
inst✝² : CommRing R
inst✝¹ : Algebra R S
inst✝ : NeZero n
μ' : ↥(rootsOfUnity n S) := hμ.toRootsOfUnity
⊢ orderOf μ' = orderOf μ

Tactic:
rw [← hμ.val_toRootsOfUnity_coe, orderOf_units, Subgroup.orderOf_coe]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
h : (cyclotomic n R).roots = 0
⊢ (cyclotomic n R).roots.Nodup

pp: case inr
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ (cyclotomic n R).roots
⊢ (cyclotomic n R).roots.Nodup

Tactic:
· exact h.symm ▸ Multiset.nodup_zero

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
ζ : R
hζ : ζ ∈ (cyclotomic n R).roots
⊢ (cyclotomic n R).roots.Nodup
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ X ^ (p ^ k * p) - 1 = X ^ p ^ (k + 1) - 1

Tactic:
pow_succ,

Goal state after:
R : Type u_1
inst✝ : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ X ^ (p ^ k * p) - 1 = X ^ (p ^ k * p) - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
hpos : 0 < n * p
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑(n * p))) (n * p)
⊢ n = n * p / p

Tactic:
rw [Nat.mul_div_cancel _ hp.pos]

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

Goal state before:
pp: case inr.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + k).succ) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
pow_succ,

Goal state after:
case inr.succ
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hm : m > 0
k : ℕ
hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)
hmn : m ≤ m + (k + 1)
h : Irreducible (cyclotomic (p ^ (m + k) * p) R)
this : m + k ≠ 0
⊢ Irreducible (cyclotomic (p ^ m) R)
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: S T : Set ℕ
A : Type u
B : Type v
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ⇑(algebraMap B C)
⊢ IsCyclotomicExtension (S ∪ T) A C

Tactic:
refine ⟨fun hn => ?_, fun x => ?_⟩
  · intro hn'
    rcases hn with hn | hn
    · obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'
      refine ⟨algebraMap B C b, ?_⟩
      exact hb.map_of_injective h
    · exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn hn'
  · refine adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
      (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
      (fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy)
      fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy
    let f := IsScalarTower.toAlgHom A B C
    have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}).map f :=
      ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩
    rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb
    refine adjoin_mono (fun y hy => ?_) hb
    obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy
    exact ⟨n, ⟨mem_union_left T hn.1, hn.2.1, by rw [← h₁, ← map_pow, hn.2.2, map_one]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : ¬n = 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
replace h1 : 2 ≤ n := (two_le_iff n).mpr ⟨NeZero.ne _, h1⟩

Goal state after:
case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (Algebra.norm K) ζ = 1
Module: Mathlib.FieldTheory.Finite.Trace

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Finite L
inst✝ : Algebra K L
x : L
⊢ (algebraMap K L) ((Algebra.norm K) x) = ∏ i ∈ Finset.range (Module.finrank K L), x ^ Nat.card K ^ i

Tactic:
have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
  have := ofFinite K
  rw [Algebra.norm_eq_prod_automorphisms, Finset.prod_range]
  exact Eq.symm <| prod_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <|
    fun i ↦ by rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
coe_int_mul_inv_eq_one h

Goal state after:
n : ℕ
x : ℤ
h : IsCoprime x ↑n
⊢ 1 = 1
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
m : ℤ
h : IsCoprime m ↑n
⊢ ↑m * (↑m)⁻¹ = 1

Tactic:
coe_int_mul_inv_eq_one h

Goal state after:
n : ℕ
inst✝ : NeZero n
m : ℤ
h : IsCoprime m ↑n
⊢ 1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ∑ x, ψ (x * b) = ↑(Fintype.card R)

Tactic:
simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]
    rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ⁻¹ * χ = 1

Tactic:
by
  ext x
  rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]
  simp only [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]
  rw [one_apply_coe]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ (n + 1)) ↑a = χ ↑a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n * χ) ↑a = χ ↑a ^ (n + 1)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n * χ) ↑a = χ ↑a ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : (χ ^ n) ↑a = χ ↑a ^ n
⊢ (χ ^ n * χ) ↑a = χ ↑a ^ n * χ ↑a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x : (↥T)ˣ
⊢ (domRestrict T 1) ↑x = 1 ↑x

Tactic:
domRestrict_apply,

Goal state after:
R : Type u_1
inst✝⁴ : CommMonoid R
R' : Type u_2
inst✝³ : CommMonoidWithZero R'
S : Type u_3
inst✝² : SetLike S R
inst✝¹ : SubmonoidClass S R
T : S
R'' : Type u_4
inst✝ : CommMonoidWithZero R''
x : (↥T)ˣ
⊢ (if IsUnit ↑x then 1 ↑↑x else 0) = 1 ↑x