mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
| star a * a

Tactic:
rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]

Goal state after:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NonUnitalRing A
inst✝¹⁴ : TopologicalSpace A
inst✝¹³ : Module 𝕜 A
inst✝¹² : StarRing A
inst✝¹¹ : PartialOrder A
inst✝¹⁰ : StarOrderedRing A
inst✝⁹ : IsScalarTower 𝕜 A A
inst✝⁸ : SMulCommClass 𝕜 A A
inst✝⁷ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝⁶ : Module ℝ A
inst✝⁵ : SMulCommClass ℝ A A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : IsTopologicalRing A
inst✝¹ : T2Space A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
| cfcₙ (fun x ↦ star x * x) a
Module: Mathlib.MeasureTheory.Function.L2Space

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal

pp: case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖↑↑f x‖ ^ 2

pp: case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x ↦ ‖↑↑f x‖ ^ 2) μ

Tactic:
rotate_left

Goal state after:
case hf
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ 0 ≤ᵐ[μ] fun x ↦ ‖↑↑f x‖ ^ 2

case hfm
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ AEStronglyMeasurable (fun x ↦ ‖↑↑f x‖ ^ 2) μ

α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ).toReal = (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ).toReal
Module: Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

Goal state before:
pp: case pos
𝕜 : 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
i : ℕ
f : 𝓓^{n₁}_{K₁}(E, F)
H : n₂ ≤ n₁ ∧ K₁ ≤ K₂
⊢ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₂ K₂ i) ((monoLM 𝕜) f) ≤ (ContDiffMapSupportedIn.seminorm 𝕜 E F n₁ K₁ i) f

Tactic:
simp (discharger := positivity) only [ContDiffMapSupportedIn.seminorm_le_iff, monoLM_apply, H,
      and_self, ↓reduceIte]
    intro hik _ _
    exact norm_iteratedFDeriv_apply_le_seminorm _ (hik.trans (mod_cast H.1))

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

Goal state before:
pp: 𝕜 : 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 = ∑ i ∈ A, (b.coord i) x • ↑b i

Tactic:
by
  simp [proj, _root_.sum_apply, ContinuousLinearMap.smulRight_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
X : Type u_2
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
P : ℕ → X →L[𝕜] X
hrank : ∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n
hcomp : ∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x
n : ℕ
U : Submodule 𝕜 X := (↑(succSub P n)).range
V : Submodule 𝕜 X := (↑(P n)).range
W : Submodule 𝕜 X := (↑(P (n + 1))).range
hV : V ≤ W
hUW : U ≤ W
hW : W = U ⊔ V
x : X
x✝ : x ∈ U ⊓ V
y : X
hy : ↑(succSub P n) y = x
z : X
hz : ↑(P n) z = x
⊢ x ∈ ⊥

Tactic:
simp only [Submodule.mem_bot]
    calc x = (P n) x := by rw [← hz, ContinuousLinearMap.coe_coe, hcomp, min_self]
         _ = 0       := by rw [← hy, ContinuousLinearMap.coe_coe]; simp [succSub, map_sub, hcomp]

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

Goal state before:
pp: case e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪x, ⟪b i, y⟫ • b i⟫

Tactic:
inner_smul_right,

Goal state after:
case e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ ⟪x, b i⟫ * ⟪b i, y⟫ = ⟪b i, y⟫ * ⟪x, b i⟫
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
inst✝⁹ : NormedField 𝕜
inst✝⁸ : NormedField 𝕜'
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SMulCommClass ℝ 𝕜 E
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
A : 𝓢(D, E) → F → G
hadd : ∀ (f g : 𝓢(D, E)) (x : F), A (f + g) x = A f x + A g x
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)) (x : F), A (a • f) x = σ a • A f x
hsmooth : ∀ (f : 𝓢(D, E)), ContDiff ℝ ∞ (A f)
hbound :
  ∀ (n : ℕ × ℕ),
    ∃ s C,
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : F),
          ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
f : 𝓢(D, E)
k n : ℕ
s : Finset (ℕ × ℕ)
C : ℝ
left✝ : 0 ≤ C
h :
  ∀ (f : 𝓢(D, E)) (x : F),
    ‖x‖ ^ (k, n).1 * ‖iteratedFDeriv ℝ (k, n).2 (A f) x‖ ≤ C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f
⊢ ∃ C, ∀ (x : F), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (A f) x‖ ≤ C

Tactic:
exact ⟨C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f, h f⟩

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
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v ↦ ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) volume
k n : ℕ
hk : ↑k ≤ K
hn✝ : ↑n ≤ N
w : V
Z :
  ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ n *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
hn : n ≠ 0
hw : w ≠ 0
⊢ 0 < ‖w‖

Tactic:
simp [hw]

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

Goal state before:
pp: s : ℝ
⊢ (fun x ↦ rexp (-x) * x ^ s) =o[atTop] fun x ↦ rexp (-(1 / 2) * x)

Tactic:
by
  refine isLittleO_of_tendsto (fun x hx => ?_) ?_
  · exfalso; exact (exp_pos (-(1 / 2) * x)).ne' hx
  have : (fun x : ℝ => exp (-x) * x ^ s / exp (-(1 / 2) * x)) =
      (fun x : ℝ => exp (1 / 2 * x) / x ^ s)⁻¹ := by
    ext1 x
    simp [field, ← exp_nsmul, exp_neg]
  rw [this]
  exact (tendsto_exp_mul_div_rpow_atTop s (1 / 2) one_half_pos).inv_tendsto_atTop

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

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

Tactic:
← Ioc_union_Ioi_eq_Ioi (@zero_le_one ℝ _ _ _ _),

Goal state after:
s : ℝ
h : 0 < s
⊢ IntegrableOn (fun x ↦ rexp (-x) * x ^ (s - 1)) (Ioc 0 1 ∪ Ioi 1) volume
Module: Mathlib.Analysis.Fourier.Inversion

Goal state before:
pp: V : Type u_1
E : Type u_2
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace ℝ V
inst✝⁴ : MeasurableSpace V
inst✝³ : BorelSpace V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : V → E
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
| ‖f v‖

Tactic:
← one_mul (‖f v‖)

Goal state after:
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
hf : Integrable f volume
c : ℝ
hc : 0 ≤ c
v : V
| 1 * ‖f v‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : 0 < s
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)

Tactic:
have : (Function.support fun x : ℝ => exp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0 := by
    rw [inter_eq_right]
    intro x hx
    rw [Function.mem_support]
    exact mul_ne_zero (exp_pos _).ne' (rpow_pos_of_pos hx _).ne'

Goal state after:
s : ℝ
hs : 0 < s
this : (Function.support fun x ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0
⊢ 0 < ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
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:
enter [1, 2, x]

Goal state after:
b : ℂ
hb : 0 < b.re
t : ℂ
x : ℝ
| cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2)
Module: Mathlib.Analysis.Distribution.FourierMultiplier

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : NormedSpace ℂ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℂ 𝕜 F
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F g₁) ((fourierMultiplierCLM F g₂) f) = (fourierMultiplierCLM F (g₁ * g₂)) f

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smulLeftCLM_apply hg₁ hg₂]

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : NormedSpace ℂ F
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ (fourierMultiplierCLM F g₂) ((fourierMultiplierCLM F g₁) f) = (fourierMultiplierCLM F (g₁ * g₂)) f

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smulLeftCLM_apply hg₁ hg₂]

Goal state after:
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
m : E
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ (∂_{m} f) u = 0

Tactic:
simp only [TemperedDistribution.lineDerivOp_apply_apply, map_neg, neg_eq_zero]

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
m : E
u : 𝓢(E, ℂ)
hu : tsupport ⇑u ⊆ s
⊢ f (∂_{m} u) = 0
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:
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:
simp [PiLp.inner_apply, wInner]

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
n✝ : ℕ
a✝ b✝ : α
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite α
ψ : AddChar α ℂ
a b : α
⊢ ⟨ψ (a + b), ⋯⟩ = ⟨ψ a, ⋯⟩ * ⟨ψ b, ⋯⟩

Tactic:
by ext : 1; simp [map_add_eq_mul]

Goal state after:
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
⊢ (fun i ↦
      ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (e * f.comp (ContinuousMap.addRight ↑i))‖) =
    fun n ↦ ‖ContinuousMap.restrict (↑{ carrier := uIcc 0 1, isCompact' := ⋯ }) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
exact funext fun n => neK _ _

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

Goal state before:
pp: m n : ℕ+
⊢ m.Coprime n → n.Coprime m

Tactic:
by
  unfold Coprime
  rw [gcd_comm]
  simp

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

Goal state before:
pp: K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

Tactic:
rw [← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons]

Goal state after:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x ∈ n.properDivisors, cyclotomic' x K) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧
    (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

Tactic:
rw [int_cyclotomic_rw hzero]

Goal state after:
case neg
n : ℕ
hzero : ¬n = 0
⊢ map (Int.castRingHom ℂ) ⋯.choose = cyclotomic' n ℂ ∧ ⋯.choose.degree = (cyclotomic' n ℂ).degree ∧ ⋯.choose.Monic
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

Tactic:
Nat.mem_properDivisors

Goal state after:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∣ n ∧ d < n
⊢ (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

Tactic:
← Finset.sdiff_union_of_subset (Nat.divisors_subset_properDivisors (ne_of_lt hpos).symm
    (Nat.mem_properDivisors.1 hm).1 (ne_of_lt (Nat.mem_properDivisors.1 hm).2)),

Goal state after:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
hpos : 0 < n
hdiff : m ≠ n
hm : m ∈ n.properDivisors
⊢ X ^ m - 1 ∣ ∏ i ∈ n.properDivisors \ m.divisors ∪ m.divisors, cyclotomic i R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1
heq : -1 = -(cyclotomic n R).coeff 0
hzero : (X ^ n - 1).coeff 0 = -1
⊢ (cyclotomic n R).coeff 0 = 1

Tactic:
exact neg_inj.mp (Eq.symm heq)

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
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ cyclotomic m R ^ ((p ^ a.succ - p ^ a) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 1))

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
R : Type u_1
p m : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Ring R
inst✝ : CharP R p
hm : ¬p ∣ m
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ cyclotomic m R ^ (p ^ a.succ * p - p ^ a * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 1))
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
a : ℕ
x✝ : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ cyclotomic m R ^ ((p ^ a.succ - p ^ (a.succ - 1)) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))

Tactic:
simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
      rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]

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

Goal state before:
pp: case refine_1
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∨ s ∈ {n}
hs' : s ≠ 0
⊢ ∃ r, IsPrimitiveRoot r s

Tactic:
mem_singleton_iff

Goal state after:
case refine_1
n : ℕ
inst✝³ : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∨ s = n
hs' : s ≠ 0
⊢ ∃ r, IsPrimitiveRoot r s
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (aeval 0) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
rw [← coeff_zero_eq_aeval_zero']

Goal state after:
case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ((X ^ (n✝ + 1) ^ n - X).coeff 0) = 0
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : ↑(castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d

Tactic:
MonoidHom.coe_coe

Goal state after:
case inr
N : ℕ
a : ZMod N
hN : N ≠ 0
this : NeZero N
d : ℕ := a.val.gcd N
hd : d ≠ 0
a₀ : ℕ
ha₀ : a.val = d * a₀
N₀ : ℕ
hN₀ : N = d * N₀
hu₀ : IsUnit ↑a₀
u : (ZMod N)ˣ
hu : (castHom ⋯ (ZMod N₀)) ↑u = ↑a₀
⊢ ∃ u, IsUnit u ∧ a = u * ↑d
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ ∃ d, d ∣ N ∧ d < N ∧ e.mulShift ↑d = 1

Tactic:
refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩

Goal state after:
case refine_1
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ d ≠ N

case refine_2
N : ℕ
inst✝¹ : NeZero N
R : Type u_1
inst✝ : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * ↑d ≠ 0
hb : e.mulShift (u * ↑d) = 1
⊢ e.mulShift ↑d = 1
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:
nth_rewrite 1 [h.eq_orderOf]
    rw [← (h.isUnit NeZero.out).unit_spec, orderOf_units]
    let ζ' : rootsOfUnity n M := ⟨(h.isUnit NeZero.out).unit, ?_⟩
    · rw [← Subgroup.orderOf_mk]
      exact Monoid.order_dvd_exponent ζ'
    simp only [mem_rootsOfUnity]
    rw [← Units.val_inj, Units.val_pow_eq_pow_val, IsUnit.unit_spec, h.pow_eq_one, Units.val_one]

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

Goal state before:
pp: S : Set ℕ
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
⊢ IsGalois K L

Tactic:
rw [isGalois_iff]
  use isSeparable S K L
  obtain ⟨i⟩ := nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)
  rw [i.transfer_normal, IntermediateField.normal_iff_forall_map_le]
  intro f x hx
  rw [← IntermediateField.mem_toSubalgebra, IntermediateField.toSubalgebra_map,
    Subalgebra.mem_map] at hx
  obtain ⟨y, hy, rfl⟩ := hx
  rw [IntermediateField.mem_toSubalgebra] at hy
  induction hy using IntermediateField.adjoin_induction with
  | mem x hx =>
    obtain ⟨n, hn, h1, h2⟩ := hx
    apply IntermediateField.subset_adjoin
    use n, hn, h1
    rw [← map_pow, ← map_one f, h2]
  | algebraMap x =>
    convert! IntermediateField.algebraMap_mem _ x
    exact AlgHom.commutes _ x
  | add x y hx hy ihx ihy =>
    rw [map_add]
    exact add_mem ihx ihy
  | mul x y hx hy ihx ihy =>
    rw [map_mul]
    exact mul_mem ihx ihy
  | inv x hx ihx =>
    rw [map_inv₀]
    exact inv_mem ihx

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

Goal state before:
pp: n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
a : ℕ
han : a ∈ {n}
x✝ : a ≠ 0
⊢ ∃ r, IsPrimitiveRoot r a

Tactic:
mem_singleton_iff

Goal state after:
n : ℕ
inst✝¹⁰ : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑n
a : ℕ
han : a = n
x✝ : a ≠ 0
⊢ ∃ r, IsPrimitiveRoot r a
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : IsUnit a
⊢ χ a = χ' a

Tactic:
exact h ha.unit

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : Fintype M
inst✝¹ : DecidableEq M
R : Type u_2
inst✝ : CommMonoidWithZero R
inst_cyc : IsCyclic Mˣ
χ : MulChar M R
⊢ χ.toUnitHom (Classical.choose ⋯) ∈ rootsOfUnity (Fintype.card Mˣ) R

Tactic:
simp only [toUnitHom_eq, mem_rootsOfUnity, ← map_pow, pow_card_eq_one, map_one]

Goal state after: