mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.PeakFunction

Goal state before:
pp: α : Type u_1
E : Type u_2
hm : MeasurableSpace α
μ : Measure α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : BorelSpace α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
g : α → E
x₀ : α
s : Set α
inst✝² : CompleteSpace E
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
hs : IsCompact s
hμ : ∀ (u : Set α), IsOpen[inst✝⁶] u → x₀ ∈ u → 0 < μ (u ∩ s)
c : α → ℝ
hc : ContinuousOn c s
h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀
hnc : ∀ x ∈ s, 0 ≤ c x
hnc₀ : 0 < c x₀
h₀ : x₀ ∈ s
hmg : IntegrableOn g s μ
hcg : ContinuousWithinAt g s x₀
φ : ℕ → α → ℝ := fun n x ↦ (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ * c x ^ n
hnφ : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ φ n x
I : ∀ (n : ℕ), IntegrableOn (fun x ↦ c x ^ n) s μ
J : ∀ (n : ℕ), 0 ≤ᵐ[μ.restrict s] fun x ↦ c x ^ n
P : ∀ (n : ℕ), 0 < ∫ (x : α) in s, c x ^ n ∂μ
hiφ : ∀ (n : ℕ), ∫ (x : α) in s, φ n x ∂μ = 1
u : Set α
u_open : IsOpen[inst✝⁶] u
x₀u : x₀ ∈ u
t : ℝ
t_pos : 0 ≤ t
tx₀ : t < c x₀
ht : ∀ x ∈ s \ u, c x ≤ t
t' : ℝ
tt' : t < t'
t'x₀ : t' < c x₀
t'_pos : 0 < t'
v : Set α
v_open : IsOpen[inst✝⁶] v
x₀_v : x₀ ∈ v
hv : v ∩ s ⊆ c ⁻¹' Ioi t'
M : ∀ (n : ℕ), ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n
N : Tendsto (fun n ↦ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 0)
ε : ℝ
εpos : ε > 0
n : ℕ
hn : (μ.real (v ∩ s))⁻¹ * (t / t') ^ n < ε
x : α
hx : x ∈ s \ u
⊢ φ n x < ε

Tactic:
exact (M n x hx).trans_lt hn

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (v : V), ↑(e (-(L (v + v₀ - v₀)) w)) • f (v + v₀) ∂μ = ↑(e ((L v₀) w)) • ∫ (v : V), ↑(e (-(L v) w)) • f v ∂μ

Tactic:
integral_add_right_eq_self fun v : V ↦ (e (-L (v - v₀) w) : ℂ) • f v,

Goal state after:
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst✝ : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (x : V), ↑(e (-(L (x - v₀)) w)) • f x ∂μ = ↑(e ((L v₀) w)) • ∫ (v : V), ↑(e (-(L v) w)) • f v ∂μ
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✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ * (‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖) ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f

Tactic:
le_seminorm 𝕜 k n f x

Goal state after:
ι : 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✝⁷ : RCLike 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace ℝ G
inst✝³ : NormedSpace 𝕜 G
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace ℝ H
inst✝ : NormedSpace 𝕜 H
L : F →L[𝕜] G
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f ≤ ‖L‖ * (SchwartzMap.seminorm 𝕜 k n) f
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Integral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x

Tactic:
have := MeasurableEmbedding.setIntegral_map (μ := volume) A f (Ici (-c))

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x ↦ -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x ↦ -x) volume = ∫ (x : ℝ) in (fun x ↦ -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
Module: Mathlib.Analysis.Fourier.FourierTransformDeriv

Goal state before:
pp: case inl
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 : ℕ
hk : ↑k ≤ K
w : V
hn : ↑0 ≤ N
Z :
  ‖w‖ ^ 0 * (‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
    ‖w‖ ^ 0 *
      ((2 * (π * ‖innerSL ℝ‖)) ^ k *
        ((2 * ↑k + 2) ^ 0 *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖))
⊢ ‖w‖ ^ 0 * ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤
    (2 * π) ^ k * (2 * ↑k + 2) ^ 0 *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (0 + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖

Tactic:
simp only [pow_zero, one_mul, mul_one, zero_add, Finset.range_one, Finset.product_singleton,
      Finset.sum_map, Function.Embedding.coeFn_mk, norm_iteratedFDeriv_zero] at Z ⊢

Goal state after:
case inl
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 : ℕ
hk : ↑k ≤ K
w : V
hn : ↑0 ≤ N
Z : ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * (π * ‖innerSL ℝ‖)) ^ k * ∑ x ∈ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ x * ‖f v‖
⊢ ‖iteratedFDeriv ℝ k (𝓕 f) w‖ ≤ (2 * π) ^ k * ∑ x ∈ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ x * ‖f v‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: case right
s : ℂ
hs : 0 < s.re
Y : ℝ
hY : 0 ≤ Y
this : (fun x ↦ ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x ↦ s * (↑(rexp (-x)) * ↑x ^ (s - 1))
⊢ MeasurableSet (Ioc 0 Y)

Tactic:
· exact measurableSet_Ioc

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

Goal state before:
pp: ι : Type u_2
inst✝² : Fintype ι
X : ι → Type u_3
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : ∀ (i : ι), IsFiniteMeasure (μ i)
i : ι
f : X i → E
hf : Integrable f (μ i)
⊢ Integrable f (map (fun x ↦ x i) (Measure.pi μ))

Tactic:
classical
  rw [Measure.pi_map_eval]
  exact hf.smul_measure <| ENNReal.prod_ne_top (by finiteness)

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

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ 0 < (↑b).re

Tactic:
ofReal_re

Goal state after:
b : ℝ
hb : 0 < b
⊢ 0 < b
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

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

Tactic:
have : ∀ x : ℝ, cexp (-(1 : ℂ) * (x : ℂ) ^ 2) = exp (-(1 : ℝ) * x ^ 2) := by
      intro x
      simp only [ofReal_exp, neg_mul, one_mul, ofReal_neg, ofReal_pow]

Goal state after:
b : ℂ
hb : 0 < b.re
nv : ∀ {b : ℂ}, 0 < b.re → b ≠ 0
this : ∀ (x : ℝ), cexp (-1 * ↑x ^ 2) = ↑(rexp (-1 * x ^ 2))
⊢ ∫ (x : ℝ), cexp (-1 * ↑x ^ 2) = (↑π / 1) ^ (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 < (↑a).re

Tactic:
ofReal_re

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ 0 < a
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral

Goal state before:
pp: case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ Gamma (↑(k + 1) + 1 + 1 / 2) = ↑(2 * (k + 1) + 1)‼ * √π / 2 ^ (k + 1 + 1)

Tactic:
rw [add_right_comm, Gamma_add_one (by positivity), Nat.cast_add, Nat.cast_one, ih, Nat.mul_add]

Goal state after:
case succ
k : ℕ
ih : Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)
⊢ (↑k + 1 + 1 / 2) * (↑(2 * k + 1)‼ * √π / 2 ^ (k + 1)) = ↑(2 * k + 2 * 1 + 1)‼ * √π / 2 ^ (k + 1 + 1)
Module: Mathlib.Analysis.Distribution.SchwartzSpace.Fourier

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
⊢ 𝓕 ((fderivCLM 𝕜 V E) f) = (2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)

Tactic:
ext x m

Goal state after:
𝕜 : Type u_1
inst✝⁹ : RCLike 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : 𝓢(V, E)
x m : V
⊢ ((𝓕 ((fderivCLM 𝕜 V E) f)) x) m = (((2 * ↑π * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (𝓕 f)) x) m
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✝ : NormedSpace ℂ F
f : 𝓢'(E, F)
x✝ : 𝓢(E, ℂ)
⊢ ((besselPotential E F 0) f) x✝ = ((ContinuousLinearMap.id ℂ 𝓢'(E, F)) f) x✝

Tactic:
simp [besselPotential]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : CompleteSpace F
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ✝ : Measure E
hμ : μ✝.HasTemperateGrowth
μ : Measure E
inst✝ : μ.HasTemperateGrowth
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ Continuous toTemperedDistribution

Tactic:
apply PointwiseConvergenceCLM.continuous_of_continuous_eval
    intro g
    have : Fact (1 ≤ (1 - p⁻¹)⁻¹) := by simp [fact_iff]
    have hpq : ENNReal.HolderConjugate p (1 - p⁻¹)⁻¹ :=
      ENNReal.HolderConjugate.inv_one_sub_inv' hp.out
    exact (((lsmul ℂ ℂ (E := F)).flip.lpPairing μ p (1 - p⁻¹)⁻¹).flip (g.toLp (1 - p⁻¹)⁻¹ μ)).cont

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

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
hvv' : v ≠ v'
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).toSubalgebra, f v ≠ f v'

Tactic:
obtain ⟨w, hw⟩ : ∃ w, char he hL w v ≠ char he hL w v' := by
    contrapose! hvv'
    exact ext_of_char_eq he he' hL hL' hvv'

Goal state after:
V : Type u_1
W : Type u_2
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module ℝ V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module ℝ W
inst✝ : TopologicalSpace W
e : AddChar ℝ Circle
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
he : Continuous ⇑e
he' : e ≠ 1
hL : Continuous fun p ↦ (L p.1) p.2
hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0
v v' : V
hvv' : v ≠ v'
w : W
hw : (char he hL w) v ≠ (char he hL w) v'
⊢ ∃ f ∈ (fun f ↦ ⇑f) '' ↑(StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL)).toSubalgebra, f v ≠ f v'
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
⊢ ∫ (x : ℝ) in 0..1, e x * (∑' (n : ℤ), f.comp (ContinuousMap.addRight ↑n)) x =
    ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), (e * f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
coe_mul,

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

Goal state before:
pp: case h
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
w : V
hw : w ≠ 0
⊢ ¬‖w‖ = 0

Tactic:
norm_eq_zero

Goal state after:
case h
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
w : V
hw : w ≠ 0
⊢ ¬w = 0
Module: Mathlib.Data.PNat.Prime

Goal state before:
pp: m n : ℕ+
⊢ (↑m).Coprime ↑n ↔ m.Coprime n

Tactic:
by
  unfold Nat.Coprime Coprime
  rw [← coe_inj]
  simp

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

Goal state before:
pp: R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h : ζ ∈ primitiveRoots k R
hk : k = 0
⊢ IsPrimitiveRoot ζ k

Tactic:
by simp [hk] at h

Goal state after:
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

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

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

Goal state before:
pp: case neg
M : Type u_1
inst✝ : CommMonoid M
k i : ℕ
hi : i.Coprime k
h0 : ¬k = 0
ζ : Mˣ
h : IsPrimitiveRoot ζ k
l : ℕ
hl : (ζ ^ i) ^ l = 1
⊢ ζ ^ (↑i * ↑l * i.gcdA k) * (ζ ^ (↑k * i.gcdB k)) ^ l = 1

Tactic:
simp only [zpow_mul, hl, h.pow_eq_one, one_zpow, one_pow, one_mul, zpow_natCast]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ f ζ ^ k = 1

Tactic:
← map_pow,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
⊢ f (ζ ^ k) = 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f ζ ^ l = 1
⊢ orderOf ζ ∣ l

Tactic:
← map_pow,

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
k : ℕ
ζ : M
f : F
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
h : IsPrimitiveRoot ζ k
hf : Injective ⇑f
l : ℕ
hl : f (ζ ^ l) = 1
⊢ orderOf ζ ∣ l
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: case refine_1.refine_2
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
ζ₁ ζ₂ : R
k₁ k₂ : ℕ
hζ₁ : IsPrimitiveRoot ζ₁ k₁
hζ₂ : IsPrimitiveRoot ζ₂ k₂
hk₁ : k₁ ≠ 0
hk₂ : k₂ ≠ 0
ζ : R
hζ : IsPrimitiveRoot ζ (k₁.lcm k₂)
this : NeZero (k₁.lcm k₂)
⊢ ζ₂ ∈ ↑S[ζ]

Tactic:
obtain ⟨_, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one <|
        (hζ₂.pow_eq_one_iff_dvd _).mpr <| k₁.dvd_lcm_right k₂
      exact Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton S _) _

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
hind : IsPrimitiveRoot μ n✝ → a.Coprime n✝ → minpoly ℤ μ = minpoly ℤ (μ ^ a)
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))

Tactic:
clear hind

Goal state after:
case refine_3
K : Type u_1
inst✝² : CommRing K
μ : K
inst✝¹ : IsDomain K
inst✝ : CharZero K
m n✝ a p : ℕ
a✝ : a ≠ 0
hprime : Prime p
h : IsPrimitiveRoot μ n✝
hcop : (p * a).Coprime n✝
⊢ minpoly ℤ (μ ^ a) = minpoly ℤ (μ ^ (p * a))
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ P = cyclotomic n R

Tactic:
rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
a✝ : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1
prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
⊢ (fun n ↦ cyclotomic n R) n = (fun n ↦ cyclotomic n R) m → n = m

Tactic:
hnm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hnm : (fun n ↦ cyclotomic n R) n = (fun n ↦ cyclotomic n R) m
⊢ n = m
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : (cyclotomic n ℂ).IsRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m

Tactic:
hnm

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n m : ℕ
hzero : n ≠ 0
this : NeZero n
hnm : cyclotomic n ℂ = cyclotomic m ℂ
hprim : IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
hroot : (cyclotomic m ℂ).IsRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n))
⊢ n = m
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod n))
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
exact IsCyclic.exists_apply_ne_one
    (hc ▸ ⟨hζ.toRootsOfUnity.val, IsPrimitiveRoot.coe_units_iff.mp hζ⟩) <|
    by simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]

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

Goal state before:
pp: case inl
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
h : Irreducible (cyclotomic (p ^ n) R)
hmn : 0 ≤ n
⊢ Irreducible (cyclotomic (p ^ 0) R)

pp: case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)

Tactic:
· simpa using irreducible_X_sub_C (1 : R)

Goal state after:
case inr
p : ℕ
hp : Nat.Prime p
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n m : ℕ
hmn : m ≤ n
h : Irreducible (cyclotomic (p ^ n) R)
hm : m > 0
⊢ Irreducible (cyclotomic (p ^ m) R)
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
⊢ (minpoly K (zeta n K L)).natDegree = φ n

Tactic:
←
    (zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible hirr,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
⊢ (cyclotomic n K).natDegree = φ n
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)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
y : C
b₁ : B
h₁ : f b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ f b₁ ^ n = 1

Tactic:
← map_pow,

Goal state after:
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)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : (algebraMap B C) b ∈ adjoin A (⇑f '' {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
y : C
b₁ : B
h₁ : f b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ f (b₁ ^ n) = 1
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
⊢ ζ' ∈ primitiveRoots n ℂ → q - 1 ≤ ‖↑q - ζ'‖

Tactic:
hζ'

Goal state after:
n : ℕ
q : ℝ
hn' : 2 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ q - 1 ≤ ‖↑q - ζ'‖
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
⊢ ζ' ∈ primitiveRoots n ℂ → ‖↑q - ζ'‖ ≤ q + 1

Tactic:
hζ'

Goal state after:
n : ℕ
q : ℝ
hn' : 3 ≤ n
hq' : 1 < q
hn : 0 < n
hq : 0 < q
ζ' : ℂ
hζ' : ζ' ∈ primitiveRoots n ℂ
⊢ ‖↑q - ζ'‖ ≤ q + 1
Module: Mathlib.FieldTheory.Finite.GaloisField

Goal state before:
pp: case succ.refine_1.inl
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)
r : ZMod (n✝ + 1)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r ^ (n✝ + 1) ^ n -
      (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r =
    0

Tactic:
← map_pow,

Goal state after:
case succ.refine_1.inl
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)
r : ZMod (n✝ + 1)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) (r ^ (n✝ + 1) ^ n) -
      (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r =
    0