mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
apply this

Goal state after:
case a
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ -↑?n < s

case n
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
this : ∀ {n : ℕ}, -↑n < s → Gamma s ≠ 0
⊢ ℕ
Module: Mathlib.Analysis.Distribution.Support

Goal state before:
pp: E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ dsupport ⇑(TemperedDistribution.delta x) = {x}

Tactic:
by
  apply subset_antisymm
  · intro x' hx'
    rw [mem_dsupport_iff] at hx'
    exact hx' {x} (isVanishingOn_delta x) (T1Space.t1 x)
  rintro x rfl
  rw [mem_dsupport_iff_forall_exists_ne]
  intro s hx hs
  obtain ⟨u, h₁, h₂, h₃, -, h₄⟩ :=
    exists_contDiff_tsupport_subset (n := ⊤) ((IsOpen.mem_nhds_iff hs).mpr hx)
  have h₁' : tsupport (Complex.ofRealCLM ∘ u) ⊆ s := (tsupport_comp_subset rfl _).trans h₁
  have h₂' : HasCompactSupport (Complex.ofRealCLM ∘ u) := h₂.comp_left rfl
  use h₂'.toSchwartzMap (Complex.ofRealCLM.contDiff.comp h₃)
  exact ⟨h₁', by simp [h₄]⟩

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℂ F
inst✝² : CompleteSpace F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : ↥(Lp F 2 volume)
⊢ 𝓕⁻ (toTemperedDistribution (𝓕 (𝓕⁻ f))) = 𝓕⁻ (𝓕 (toTemperedDistribution (𝓕⁻ f)))

Tactic:
rw [fourier_toTemperedDistribution_eq]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : InnerProductSpace ℝ E
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace 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₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : NormedSpace 𝕜 F₃
inst✝¹ : SMulCommClass ℂ 𝕜 F₃
inst✝ : CompleteSpace F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
⊢ 𝓕 (((convolution B) f) g) = ((pairing B) (𝓕 f)) (𝓕 g)

Tactic:
simp [convolution]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹⁸ : RCLike 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : InnerProductSpace ℝ E
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : MeasurableSpace E
inst✝¹³ : BorelSpace 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₂
inst✝⁴ : NormedAddCommGroup F₃
inst✝³ : NormedSpace ℂ F₃
inst✝² : NormedSpace 𝕜 F₃
inst✝¹ : SMulCommClass ℂ 𝕜 F₃
inst✝ : CompleteSpace F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
⊢ 𝓕 (((convolution B) f) g) = ((pairing B) (𝓕 f)) (𝓕 g)

Tactic:
by simp [convolution]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = (ArithmeticFunction.prodPrimeFactors fun p ↦ (↑ζ + f) p) n

Tactic:
prodPrimeFactors_apply hn.ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, (1 + f p) = ∏ p ∈ n.primeFactors, (↑ζ + f) p
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 < B ∧ volume A ≤ ↑B

Tactic:
have hc : IsCompact A := by
      simpa only [Metric.closedBall, dist_eq_norm, sub_zero] using isCompact_closedBall (0 : V) _
    let B₀ := volume A
    replace hc : B₀ < ⊤ := hc.measure_lt_top
    refine ⟨B₀.toNNReal + 1, add_pos_of_nonneg_of_pos B₀.toNNReal.coe_nonneg one_pos, ?_⟩
    rw [ENNReal.coe_add, ENNReal.coe_one, ENNReal.coe_toNNReal hc.ne]
    exact le_self_add

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

Goal state before:
pp: 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_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖

Tactic:
rintro ⟨x, hx⟩

Goal state after:
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)
⊢ ‖(ContinuousMap.restrict (Icc (x✝ + R) (x✝ + S)) f) ⟨x, hx⟩‖ ≤
    ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a ↦ -a, continuous_toFun := ⋯ })‖
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

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

pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
· subst k; simp_all only [pow_one, Nat.coprime_zero_right]

Goal state after:
case neg
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
⊢ IsPrimitiveRoot (ζ ^ i) k
Module: Mathlib.Analysis.Fourier.PoissonSummation

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[cocompact ℝ] fun x ↦ |x| ^ (-b)
K : Compacts ℝ
⊢ (fun x ↦ ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight x))‖) =O[cocompact ℝ] fun x ↦ |x| ^ (-b)

Tactic:
obtain ⟨r, hr⟩ := K.isCompact.isBounded.subset_closedBall 0
  rw [closedBall_eq_Icc, zero_add, zero_sub] at hr
  have : ∀ x : ℝ,
      ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ := by
    intro x
    rw [ContinuousMap.norm_le _ (norm_nonneg _)]
    rintro ⟨y, hy⟩
    refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
    · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
    · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
  simp_rw [cocompact_eq_atBot_atTop, isBigO_sup] at hf ⊢
  constructor
  · refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)
    simp_rw [norm_norm]; exact this
  · refine (isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)
    simp_rw [norm_norm]; exact this

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

Goal state before:
pp: case right
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 R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ Function.Surjective
    ⇑(((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i ↦ Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)

Tactic:
rintro ⟨ξ, i, rfl⟩
        refine ⟨Int.castAddHom (ZMod k) i, ?_⟩
        rw [AddMonoidHom.liftOfRightInverse_comp_apply]
        rfl

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

Goal state before:
pp: case left
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
⊢ 0 + B * cyclotomic' k K = X ^ k - 1

pp: case right
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
⊢ degree 0 < B.degree

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

Goal state after:
case right
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
⊢ degree 0 < B.degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ ∃ x, (mapRingHom (Int.castRingHom K)) x = cyclotomic' k K

Tactic:
use Q₁

Goal state after:
case h
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ⋯
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left✝ : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := ⋯
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ (mapRingHom (Int.castRingHom K)) Q₁ = cyclotomic' k K
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

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

Tactic:
· simp only [hzero, cyclotomic, degree_one, monic_one, cyclotomic'_zero, dif_pos,
      Polynomial.map_one, and_self_iff]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic 0 ℤ).degree = ↑(Nat.totient 0)

Tactic:
simp only [cyclotomic, degree_one, dif_pos, Nat.totient_zero, CharP.cast_eq_zero]

Goal state after:
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:
by
  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.Polynomial.Cyclotomic.Basic

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

Tactic:
exact Finset.notMem_sdiff_of_notMem_left Nat.self_notMem_properDivisors

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

Goal state before:
pp: case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
⊢ ξ ∈ primitiveRoots k R → ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ

Tactic:
hξ

Goal state after:
case neg.refine_3
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
this : NeZero k
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ k.Coprime a) ∧ ζ ^ a = ξ
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1
hrw : ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = 1
⊢ (X - 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0 = -1

Tactic:
simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
y : S
hy : y ∈ K[x]
a✝ : ⟨y, hy⟩ ∈ ⊤
this : (∃ f, ⟨y, hy⟩ = (aeval ⟨x, ⋯⟩) f) → ⟨y, hy⟩ ∈ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
⊢ ⟨y, hy⟩ ∈ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)

Tactic:
apply this

Goal state after:
case hsp
K : Type u_1
S : Type u_2
inst✝² : Field K
inst✝¹ : CommRing S
inst✝ : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective ⇑(algebraMap (↥K[x]) S)
hx' : IsIntegral K ⟨x, ⋯⟩
y : S
hy : y ∈ K[x]
a✝ : ⟨y, hy⟩ ∈ ⊤
this : (∃ f, ⟨y, hy⟩ = (aeval ⟨x, ⋯⟩) f) → ⟨y, hy⟩ ∈ Submodule.span K (Set.range fun i ↦ ⟨x, ⋯⟩ ^ ↑i)
⊢ ∃ f, ⟨y, hy⟩ = (aeval ⟨x, ⋯⟩) f
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ B.gen ^ n = (aeval B.gen) Q

Tactic:
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly R B.gen)]

Goal state after:
S : Type u_2
inst✝⁶ : CommRing S
R : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Algebra R S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
i : Fin B.dim
a✝ : Nontrivial S
Q : R[X] := X ^ n %ₘ minpoly R B.gen
⊢ (aeval B.gen) (X ^ n %ₘ minpoly R B.gen + minpoly R B.gen * (X ^ n /ₘ minpoly R B.gen)) = (aeval B.gen) Q
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 6 ℤ * cyclotomic 2 ℤ = (X ^ 2 - X + 1) * cyclotomic 2 ℤ

Tactic:
rw [show 6 = 2 * 3 by rfl, ← cyclotomic_expand_eq_cyclotomic_mul Nat.prime_three (by norm_num1)]

Goal state after:
R : Type u_1
inst✝ : Ring R
⊢ (expand ℤ 3) (cyclotomic 2 ℤ) = (X ^ 2 - X + 1) * cyclotomic 2 ℤ
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: p n : ℕ
inst✝⁹ : NeZero n
A : Type w
B : Type z
K : Type u
L : Type v
C : Type w
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsCyclotomicExtension {n} A B
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ PowerBasis K L

Tactic:
by
  apply PowerBasis.ofAdjoinEqTop (((integral {n} K L).isIntegral ζ).sub isIntegral_one)
  exact PowerBasis.adjoin_eq_top_of_gen_mem_adjoin (hζ.powerBasis_gen_mem_adjoin_zeta_sub_one _)

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < eval x (cyclotomic 0 R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic 0 R))

Tactic:
simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]

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

Goal state before:
pp: case succ.succ.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
⊢ (1 < x → 0 < x + 1) ∧ (1 ≤ x → 0 ≤ x + 1)

Tactic:
constructor <;> intro <;> linarith

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 :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
x y : ℕ
hxy : (fun t ↦ p ^ (t + 1)) x = (fun t ↦ p ^ (t + 1)) y
⊢ x = y

Tactic:
apply Nat.succ_injective

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 :
  ↑n =
    (∏ x ∈ n.divisors.erase 1 \ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)) *
      ∏ x ∈ image (fun t ↦ p ^ (t + 1)) (range (padicValNat p n)), eval 1 (cyclotomic x ℤ)
x y : ℕ
hxy : (fun t ↦ p ^ (t + 1)) x = (fun t ↦ p ^ (t + 1)) y
⊢ x.succ = y.succ
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
this : {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} = {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}
b : B
h : b ∈ adjoin A {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
⊢ b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h

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

Goal state before:
pp: S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
⊢ ∀ (x : ↥(adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}

Tactic:
rintro ⟨x, hx⟩

Goal state after:
S : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n
x : B
hx : x ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
⊢ ⟨x, hx⟩ ∈ adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case pos.inr
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
h✝ : p ∣ ps.prod id * n
h : p ∣ n
⊢ False

Tactic:
· exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, pp, hpx, h⟩ hx

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

Goal state before:
pp: p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : Algebra (ZMod p) K
h : Nat.card K = p ^ n
⊢ IsSplittingField (ZMod p) K (X ^ p ^ n - X)

Tactic:
by
  have : Finite K := (Nat.card_pos_iff.mp (h ▸ pow_pos h_prime.1.pos n)).2
  have : Fintype K := Fintype.ofFinite K
  rw [← h, Nat.card_eq_fintype_card]
  exact FiniteField.isSplittingField_sub K (ZMod p)

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

Goal state before:
pp: case inl
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
⊢ ∃ a, (Algebra.norm K) a = 0

pp: case inr
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
k : K
ne : k ≠ 0
⊢ ∃ a, (Algebra.norm K) a = k

Tactic:
· exact ⟨0, Algebra.norm_zero ..⟩

Goal state after:
case inr
K : Type u_1
K' : Type u_2
inst✝³ : Field K
inst✝² : Field K'
inst✝¹ : Algebra K K'
inst✝ : Finite K'
k : K
ne : k ≠ 0
⊢ ∃ a, (Algebra.norm K) a = k
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
x : CyclotomicField n K
hx : x ∈ adjoin A {b | b ^ n = 1}
y : CyclotomicField n K
hy : y ∈ {b | b ^ n = 1}
⊢ ⟨y, ⋯⟩ ^ n = 1

Tactic:
rwa [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0

Tactic:
exact map_nonunit _ h

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

Goal state before:
pp: N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ (fun Φ k ↦ (↑N)⁻¹ • auxDFT Φ (-k)) (auxDFT Φ) = Φ

Tactic:
simp only [auxDFT_auxDFT, neg_neg, ← mul_smul, inv_mul_cancel₀ (NeZero.ne _), one_smul]

Goal state after:
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(Iic s) = 2 ^ #s

Tactic:
by rw [Iic_eq_powerset, card_powerset]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ f.closure.inverse.graph = f.inverse.graph.topologicalClosure

Tactic:
inverse_graph hf,

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ f.closure.inverse.graph = (Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph).topologicalClosure