mathlib-initiative/mathlib-tactics huggingface dataset:
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : Fin n → W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L)
      (fun x ↦ (fourierPowSMulRight L f x (n + 1)) (Fin.cons w' m)) w =
    (fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L)
        (fun x ↦ (fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) x) w') w)
      m

Tactic:
fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v ↦ ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : Fin n → W
⊢ fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L)
      (fun x ↦ (fourierPowSMulRight L f x (n + 1)) (Fin.cons w' m)) w =
    fourierIntegral 𝐞 μ (ContinuousLinearMap.toLinearMap₁₂ L)
      (fun x ↦ ((fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) x) w') m) w
Module: Mathlib.Analysis.Fourier.FourierTransform

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

Tactic:
calc
  ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν
    = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν := by
    congr with ξ
    apply (ContinuousLinearMap.integral_comp_commSL RCLike.conj_smul _ _).symm
    exact (fourierIntegral_convergent_iff he hL _).2 hf
  _ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
    integral_fourierIntegral_swap M.flip he hL hf hg
  _ = ∫ x, (∫ ξ, M (f x) (e (L.flip ξ x) • g ξ) ∂ν) ∂μ := by
    congr with x
    congr with ξ
    rw [← smul_one_smul ℂ _ (f x), ← smul_one_smul ℂ _ (g ξ)]
    simp only [map_smulₛₗ, ContinuousLinearMap.flip_apply, LinearMap.flip_apply, RingHom.id_apply,
      Circle.smul_def, smul_eq_mul, mul_one, ← Circle.coe_inv_eq_conj, AddChar.map_neg_eq_inv,
      inv_inv]
  _ = ∫ x, (∫ ξ, M (f x) (e (-(-L.flip ξ) x) • g ξ) ∂ν) ∂μ := by
    simp only [LinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, LinearMap.neg_apply,
      neg_neg]
  _ = ∫ x, M (f x) (∫ ξ, e (-(-L.flip ξ) x) • g ξ ∂ν) ∂μ := by
    congr with x
    apply ContinuousLinearMap.integral_comp_comm
    have hLflip : Continuous fun (p : W × V) => (-L.flip p.1) p.2 :=
      (continuous_neg.comp hL).comp continuous_swap
    exact (fourierIntegral_convergent_iff (L := -L.flip) he hLflip x).2 hg

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

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
⊢ False

Tactic:
have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) :=
    H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl

Goal state after:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.ImproperIntegrals

Goal state before:
pp: s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) volume

Tactic:
apply H'.mono' measurable_inv.aestronglyMeasurable

Goal state after:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (fun x ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi (max 1 t)), ‖a⁻¹‖ ≤ a ^ s
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x : V
⊢ 𝓕 f₁ x = 𝓕 f₂ x

Tactic:
apply integral_congr_ae
  filter_upwards [hf] with _ hf'
  rw [hf']

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
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
| (Measure.map Neg.neg μ).restrict (Iic 0)

Tactic:
measurableEmbedding_neg.restrict_map

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
| Measure.map Neg.neg (μ.restrict (Neg.neg ⁻¹' Iic 0))
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✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : SecondCountableTopology α
inst✝⁸ : MeasurableSpace α
μ : Measure α
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : AddCommGroup α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsOrderedAddMonoid α
inst✝³ : CompactIccSpace α
inst✝² : atTop.IsMeasurablyGenerated
inst✝¹ : MeasurableNeg α
inst✝ : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable f (Measure.map Neg.neg (μ.restrict (Ici 0)))
Module: Mathlib.Analysis.Fourier.FourierTransform

Goal state before:
pp: V : Type u_1
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f₁ f₂ : V → E
hf : f₁ =ᵐ[volume] f₂
x : V
⊢ 𝓕⁻ f₁ x = 𝓕⁻ f₂ x

Tactic:
apply integral_congr_ae
  filter_upwards [hf] with _ hf'
  rw [hf']

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

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = (starRingEnd ℂ) ↑(rexp (-x)) * (starRingEnd ℂ) (↑x ^ (s - 1))

Tactic:
conj_ofReal,

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * ↑x ^ ((starRingEnd ℂ) s - 1) = ↑(rexp (-x)) * (starRingEnd ℂ) (↑x ^ (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp ((starRingEnd ℂ) ↑(Real.log x) * (starRingEnd ℂ) (s - 1))

Tactic:
conj_ofReal,

Goal state after:
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(rexp (-x)) * cexp (↑(Real.log x) * ((starRingEnd ℂ) s - 1)) =
    ↑(rexp (-x)) * cexp (↑(Real.log x) * (starRingEnd ℂ) (s - 1))
Module: Mathlib.Analysis.SpecialFunctions.PolarCoord

Goal state before:
pp: ⊢ ContinuousOn (fun q ↦ (Complex.equivRealProd.symm q).arg) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})

Tactic:
have A : MapsTo Complex.equivRealProd.symm ({q : ℝ × ℝ | 0 < q.1} ∪ {q : ℝ × ℝ | q.2 ≠ 0})
        Complex.slitPlane := by
      rintro ⟨x, y⟩ hxy; simpa only using! hxy

Goal state after:
A : MapsTo (⇑Complex.equivRealProd.symm) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0}) Complex.slitPlane
⊢ ContinuousOn (fun q ↦ (Complex.equivRealProd.symm q).arg) ({q | 0 < q.1} ∪ {q | q.2 ≠ 0})
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
· simpa only [not_lt, integrable_exp_neg_mul_sq_iff] using hb

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ ‖↑x ^ s‖ * ‖↑(rexp (-x))‖ = x ^ s.re * rexp (-1 * x)

Tactic:
norm_cpow_eq_rpow_re_of_pos hx,

Goal state after:
s : ℂ
hs : 0 < s.re
this : (fun X ↦ s * s.partialGamma X - ↑X ^ s * ↑(rexp (-X))) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ s.re * ‖↑(rexp (-x))‖ = x ^ s.re * rexp (-1 * x)
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform

Goal state before:
pp: b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
⊢ ?m.420 * |c| ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))

Tactic:
conv_lhs => simp only [mul_comm _ |c|]

Goal state after:
b : ℂ
hb : 0 < b.re
c T : ℝ
hT : 0 ≤ T
vert_norm_bound :
  ∀ {T : ℝ},
    0 ≤ T →
      ∀ {c y : ℝ},
        |y| ≤ |c| → ‖cexp (-b * (↑T + ↑y * I) ^ 2)‖ ≤ rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
⊢ |c| * ?m.420 ≤ 2 * |c| * rexp (-(b.re * T ^ 2 - 2 * |b.im| * |c| * T - b.re * c ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case e'_3
⊢ ↑π ^ (1 / 2) = ↑π ^ (↑1 / ↑2)

Tactic:
ofReal_ofNat,

Goal state after:
case e'_3
⊢ ↑π ^ (1 / 2) = ↑π ^ (↑1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ Gamma s ≠ 0

Tactic:
suffices ∀ {n : ℕ}, -(n : ℝ) < s → Gamma s ≠ 0 by
    apply this
    swap
    · exact ⌊-s⌋₊ + 1
    rw [neg_lt, Nat.cast_add, Nat.cast_one]
    exact Nat.lt_floor_add_one _
  intro n
  induction n generalizing s with
  | zero =>
    intro hs
    refine (Gamma_pos_of_pos ?_).ne'
    rwa [Nat.cast_zero, neg_zero] at hs
  | succ _ n_ih =>
    intro hs'
    have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
    rw [Gamma_add_one, mul_ne_zero_iff] at this
    · exact this.2
    · simpa using hs 0

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

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

Tactic:
conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]
  rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub,
    mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]

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✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ (Δ f) u = f (Δ u)

Tactic:
by
  simp [laplacian_eq_sum (stdOrthonormalBasis ℝ E),
    SchwartzMap.laplacian_eq_sum (stdOrthonormalBasis ℝ E), map_neg, neg_neg]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Fintype α
⊢ Fintype.card (AddChar α ℂ) = Fintype.card α

Tactic:
by
  obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α
  classical
  have hn' i : NeZero (n i) := by have := hn i; exact ⟨by positivity⟩
  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n <| e a).compAddMonoidHom e)
  have hf : Injective f := circleEquivComplex.injective.comp
    ((compAddMonoidHom_injective_left _ e.surjective).comp <| mkZModAux_injective.comp <|
      DFunLike.coe_injective.comp <| e.injective.comp Additive.ofMul.injective)
  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)

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

Goal state before:
pp: a b m n : ℕ+
cop : m.Coprime n
am : a ∣ m
bn : b ∣ n
⊢ a = (b * a).gcd m

Tactic:
by rw [mul_comm]; apply Coprime.factor_eq_gcd_left cop am bn

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

Goal state before:
pp: l : ℕ
hl : Squarefree l
⊢ ((-1) ^ 2) ^ cardFactors l = 1

Tactic:
neg_one_sq,

Goal state after:
l : ℕ
hl : Squarefree l
⊢ 1 ^ cardFactors l = 1
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ↑x ^ n = 1

Tactic:
rw [← H, ← exp_nat_mul, exp_eq_one_iff]

Goal state after:
case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
i : ℕ
left✝ : i < n
H : cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x
⊢ ∃ n_1, ↑n * (2 * ↑π * I * (↑i / ↑n)) = ↑n_1 * (2 * ↑π * I)
Module: Mathlib.RingTheory.RootsOfUnity.Complex

Goal state before:
pp: ζ : ℂˣ
n : ℕ
inst✝ : NeZero n
hζ : ζ ∈ rootsOfUnity n ℂ
⊢ ‖↑ζ‖ = 1

Tactic:
by
  refine norm_eq_one_of_pow_eq_one ?_ <| NeZero.ne n
  norm_cast
  rw [_root_.mem_rootsOfUnity] at hζ
  rw [hζ, Units.val_one]

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi

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

Goal state before:
pp: case mpr
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
k : ℕ
inst✝ : NeZero k
ζ : R
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
exact h.pow_of_coprime i hi

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

Goal state before:
pp: case neg.h
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
e : α ^ n = a
hn : n > 0
hα : ¬α = 0
m : ℕ
left✝ : m < n
⊢ ζ ^ m * α ∈ nthRoots n a

Tactic:
rw [mem_nthRoots hn, mul_pow, e, ← pow_mul, mul_comm m,
      pow_mul, hζ.pow_eq_one, one_pow, one_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ (cyclotomic n R).IsRoot μ

Tactic:
rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h,
    roots_prod_X_sub_C, ← Finset.mem_def]
  rwa [← mem_primitiveRoots hpos] at h

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

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

Tactic:
cyclotomic_prime_pow_eq_geom_sum hn.out,

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

Goal state before:
pp: case inr.refine_2
p n : ℕ
hp : Nat.Prime p
hdiv : p ∣ n
R : Type u_1
inst✝ : CommRing R
hzero : n > 0
this : NeZero n
⊢ ((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ).natDegree

Tactic:
rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n,
      Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = eval 1 (∑ i ∈ range n, X ^ i)
⊢ False

Tactic:
eval_geom_sum,

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
h : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
hn' : n > 0
hn : 1 < n
p : ℕ
hp : Nat.Prime p
hpe : p ∣ (eval 1 (cyclotomic n ℤ)).natAbs
this✝ : Fact (Nat.Prime p)
this : eval 1 (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ range n, 1 ^ i
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
eq_self_sdiff_zero S,

Goal state after:
case neg
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension (S \ {0}) A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ (eval (↑0) (cyclotomic n ℤ)).natAbs ≠ 0

Tactic:
Int.natAbs_ne_zero,

Goal state after:
case inl
n : ℕ
hn' : 1 < n
hq : 0 ≠ 1
⊢ eval (↑0) (cyclotomic n ℤ) ≠ 0
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
n✝ : ℕ
hi : n✝ = n
hi' : n✝ ≠ 0
⊢ IsPrimitiveRoot (↑⟨ζ, ⋯⟩) n✝

Tactic:
Subtype.coe_mk,

Goal state after:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
ζ : B
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
n✝ : ℕ
hi : n✝ = n
hi' : n✝ ≠ 0
⊢ IsPrimitiveRoot ζ n✝
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_2.e_a
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)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝² : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
this : (p - 1) * (p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L) = (p - 1) * p ^ (k.succ - 1)
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s

Tactic:
replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this

Goal state after:
case refine_2.e_a
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)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this✝² : IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this✝¹ : FiniteDimensional K L
this✝ : IsGalois K L
H : (Algebra.norm K) η₁ = ↑(p ^ (k - s + 1)).minFac
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case neg
n m : ℕ
hm : NeZero m
h : n ∣ m
x : ℕ
hx : x.Coprime n
ps : Finset ℕ := {p ∈ m.primeFactors | ¬p ∣ x}
p : ℕ
pp : Nat.Prime p
hp : p ∣ x + ps.prod id * n
hpn : p ∣ m
hpx : ¬p ∣ x
⊢ False

Tactic:
have pps : p ∈ ps := Finset.mem_filter.mpr ⟨Nat.mem_primeFactors.mpr ⟨pp, hpn, hm.out⟩, hpx⟩
    have h := Nat.dvd_sub hp ((Finset.dvd_prod_of_mem id pps).mul_right n)
    rw [Nat.add_sub_cancel] at h
    contradiction

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

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ ((-1) ^ 2 * 2 ^ 2) ^ 2 ^ k₁ = ↑2 ^ (2 * 2 ^ k₁)

Tactic:
neg_one_sq,

Goal state after:
case pos
p : ℕ
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ (1 * 2 ^ 2) ^ 2 ^ k₁ = ↑2 ^ (2 * 2 ^ k₁)