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

Goal state before:
pp: case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
g' : ↥(Lp F p volume)
hg : (besselPotential E F s) g = Lp.toTemperedDistribution g'
⊢ (besselPotential E F s) (f - g) = Lp.toTemperedDistribution (f' - g')

Tactic:
rw [← Lp.toTemperedDistributionCLM_apply]

Goal state after:
case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f g : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
g' : ↥(Lp F p volume)
hg : (besselPotential E F s) g = Lp.toTemperedDistribution g'
⊢ (besselPotential E F s) (f - g) = (Lp.toTemperedDistributionCLM F volume p) (f' - g')
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (-f) = Lp.toTemperedDistribution (-f')

Tactic:
rw [← Lp.toTemperedDistributionCLM_apply]

Goal state after:
case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (-f) = (Lp.toTemperedDistributionCLM F volume p) (-f')
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (c • f) = Lp.toTemperedDistribution (c • f')

Tactic:
rw [← Lp.toTemperedDistributionCLM_apply]

Goal state after:
case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
c : ℂ
f : 𝓢'(E, F)
f' : ↥(Lp F p volume)
hf : (besselPotential E F s) f = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) (c • f) = (Lp.toTemperedDistributionCLM F volume p) (c • f')
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ (besselPotential E F s) 0 = Lp.toTemperedDistribution 0

Tactic:
rw [← Lp.toTemperedDistributionCLM_apply]

Goal state after:
case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ (besselPotential E F s) 0 = (Lp.toTemperedDistributionCLM F volume p) 0
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (besselPotential E F s) ((SchwartzMap.toTemperedDistributionCLM E F volume) f) =
    Lp.toTemperedDistribution (((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f).toLp p volume)

Tactic:
besselPotential,

Goal state after:
case h
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : 𝓢(E, F)
⊢ (fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) ((SchwartzMap.toTemperedDistributionCLM E F volume) f) =
    Lp.toTemperedDistribution (((SchwartzMap.fourierMultiplierCLM F fun x ↦ (1 + ‖x‖ ^ 2) ^ (s / 2)) f).toLp p volume)
Module: Mathlib.Analysis.Distribution.Sobolev

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ (besselPotential E F s) f = Lp.toTemperedDistribution (𝓕⁻ f')

Tactic:
besselPotential,

Goal state after:
case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
f : 𝓢'(E, F)
f' : ↥(Lp F 2 volume)
hf' : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution f'
⊢ (fourierMultiplierCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) f = Lp.toTemperedDistribution (𝓕⁻ f')
Module: Mathlib.Analysis.Fourier.AddCircleMulti

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
x : UnitAddTorus d
⊢ HasSum (fun i ↦ mFourierCoeff (⇑f) i • (mFourier i) x) (f x)

Tactic:
by
  simpa only [map_smul] using! (ContinuousMap.evalCLM ℂ x).hasSum
    (hasSum_mFourier_series_of_summable h)

Goal state after:
Module: Mathlib.GroupTheory.FiniteAbelian.Basic

Goal state before:
pp: case intro.succ
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Finite G
val✝ : Fintype G
ι : Type
fι : Fintype ι
p : ι → ℕ
hp : ∀ (i : ι), Nat.Prime (p i)
e : ι → ℕ
n : ℕ
f : G ≃+ (Fin (n + 1) →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i)
⊢ ∃ ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ ⨁ (i : ι), ZMod (p i ^ e i))

Tactic:
· have := @Fintype.prodLeft _ _ _ (Fintype.ofEquiv G f.toEquiv) _
    exact
      (Fintype.ofSurjective (fun f : Fin n.succ →₀ ℤ => f 0) fun a =>
            ⟨Finsupp.single 0 a, Finsupp.single_eq_same⟩).false.elim

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

Goal state before:
pp: case h
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : InnerProductSpace ℂ F
inst✝ : CompleteSpace F
s : ℝ
hs : ↑(Module.finrank ℝ E) < 2 * s
f : 𝓢'(E, F)
hf : MemSobolev s 2 f
u : ↥(Lp F 2 volume)
hu : (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (s / 2))) (𝓕 f) = Lp.toTemperedDistribution u
this✝ : MemLp (fun x ↦ (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 volume
this : MemLp (fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) 2 volume
⊢ 𝓕 f = (smulLeftCLM F fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2))) (Lp.toTemperedDistribution u)

Tactic:
rw [← hu, smulLeftCLM_smulLeftCLM_apply (by fun_prop) (by fun_prop)]
    convert! (smulLeftCLM_const 1 (𝓕 f)).symm using 1
    · simp
    · congr
      ext x
      rw [Pi.mul_apply]
      norm_cast
      rw [← Real.rpow_add (by positivity)]
      ring_nf
      simp

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
h₀ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
⊢ False

Tactic:
have h₁ := congr_fun ((complexBasis α).sum_repr f) a

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
ha : a ≠ 0
h : ∀ (ψ : AddChar α ℂ), ψ a = 1
f : α → ℂ := fun b ↦ if a = b then 1 else 0
h₀ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) 0 = f 0
h₁ : (∑ i, ((complexBasis α).repr f) i • (complexBasis α) i) a = f a
⊢ False
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 * ∑' (i : ℤ), (f.comp (ContinuousMap.addRight ↑i)) x =
    ∫ (x : ℝ) in 0..1, ∑' (n : ℤ), e x * (f.comp (ContinuousMap.addRight ↑n)) x

Tactic:
tsum_mul_left

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommGroupWithZero R
s : Set ℕ
hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s
f g : ℕ → R
hf : ∀ n > 0, f n ≠ 0
hg : ∀ n > 0, g n ≠ 0
n : ℕ
hn : n > 0
⊢ (n ∈ s →
      ∏ x ∈ n.divisorsAntidiagonal, (if h : 0 < x.2 then Units.mk0 (g x.2) ⋯ else 1) ^ μ x.1 =
        if h : 0 < n then Units.mk0 (f n) ⋯ else 1) ↔
    n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n

Tactic:
· rw [dif_pos hn, ← Units.val_inj, ← Units.coeHom_apply, map_prod, Units.val_mk0,
      prod_congr rfl _]
    intro x hx
    rw [dif_pos (pos_of_mem_divisors (snd_mem_divisors_of_mem_antidiagonal hx)),
      Units.coeHom_apply, Units.val_zpow_eq_zpow_val, Units.val_mk0]

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:
simp [hk] at h

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Periodic

Goal state before:
pp: case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ ∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p))) (x + p) =
    (∑' (c : ℤ), f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))) x

Tactic:
← tsum_apply this

Goal state after:
case e'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : AddCommGroup X
inst✝³ : ContinuousAdd X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n ↦ f.comp (ContinuousMap.addRight (n • p))
this : Summable fun c ↦ f.comp (ContinuousMap.addRight ((Equiv.addRight 1) c • p))
⊢ ∑' (i : ℤ), (f.comp (ContinuousMap.addRight (i • p))) (x + p) =
    ∑' (i : ℤ), (f.comp (ContinuousMap.addRight ((Equiv.addRight 1) i • p))) x
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
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ 1 / (2 * ‖w‖) ≤ 1

Tactic:
← div_div

Goal state after:
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
hB_pos : 0 < B
hB_vol : volume A ≤ ↑B
δ : ℝ
hδ1 : δ > 0
hδ2 : ∀ ⦃a b : V⦄, dist a b < δ → dist (f a) (f b) < ε / ↑B
w : V
hw_bd : 1 / 2 + 1 / (2 * δ) ≤ ‖w‖
hw_ne : w ≠ 0
hw'_nm : ‖i w‖ = 1 / (2 * ‖w‖)
this : ‖1 / 2‖ = 2⁻¹
v : V
hv : R + 1 < ‖v‖
⊢ 1 / 2 / ‖w‖ ≤ 1
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
i : ℤ
hi : i.gcd ↑k = 1
⊢ IsPrimitiveRoot (ζ ^ i) k

Tactic:
by
  by_cases h0 : 0 ≤ i
  · lift i to ℕ using h0
    exact_mod_cast h.pow_of_coprime i hi
  have : 0 ≤ -i := (Int.neg_pos_of_neg <| Int.lt_of_not_ge h0).le
  lift -i to ℕ using this with i' hi'
  rw [← inv_iff, ← zpow_neg, ← hi', zpow_natCast]
  apply h.pow_of_coprime
  rwa [Int.gcd, ← Int.natAbs_neg, ← hi'] at hi

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
inst✝ : CommRing R
ζ : Rˣ
h✝ h : IsPrimitiveRoot ζ k
⊢ ∀ (x y : ℤ),
    Additive.ofMul ⟨(fun x ↦ ζ ^ x) (x + y), ⋯⟩ =
      Additive.ofMul ⟨(fun x ↦ ζ ^ x) x, ⋯⟩ + Additive.ofMul ⟨(fun x ↦ ζ ^ x) y, ⋯⟩

Tactic:
intro i j

Goal state after:
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
i j : ℤ
⊢ Additive.ofMul ⟨(fun x ↦ ζ ^ x) (i + j), ⋯⟩ =
    Additive.ofMul ⟨(fun x ↦ ζ ^ x) i, ⋯⟩ + Additive.ofMul ⟨(fun x ↦ ζ ^ x) j, ⋯⟩
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

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

Tactic:
replace hm := Nat.mem_properDivisors.2
    ⟨hm, lt_of_le_of_ne (Nat.divisor_le (Nat.mem_divisors.2 ⟨hm, hpos.ne'⟩)) hdiff⟩

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, cyclotomic i R
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
hpos : 0 < n
⊢ Irreducible (cyclotomic n ℤ)

Tactic:
cyclotomic_eq_minpoly (isPrimitiveRoot_exp n hpos.ne') hpos

Goal state after:
n : ℕ
hpos : 0 < n
⊢ Irreducible (minpoly ℤ (cexp (2 * ↑Real.pi * I / ↑n)))
Module: Mathlib.RingTheory.Adjoin.PowerBasis

Goal state before:
pp: K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
⊢ ∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)

Tactic:
intro i j

Goal state after:
K : Type u_1
S : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing S
inst✝⁴ : Algebra K S
R : Type u_3
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen) P = B'.gen
hB : IsIntegral R B.gen
hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Eval

Goal state before:
pp: n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : (cyclotomic n ℝ).IsRoot y
⊢ False

Tactic:
rw [@isRoot_cyclotomic_iff] at hy

Goal state after:
n : ℕ
hn : 2 < n
R : Type u_1
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
this✝ : NeZero n
h0 : eval 0 (cyclotomic n ℝ) = 1
hx : eval (-1) (cyclotomic n ℝ) ≤ 0
this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x ↦ eval x (cyclotomic n ℝ)
y : ℝ
hy : IsPrimitiveRoot y n
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: n : ℕ
inst✝³ : NeZero n
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hno : Odd n
ζ x : K
hζ : IsPrimitiveRoot ζ n
hx : IsOfFinOrder x
⊢ ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r

Tactic:
obtain ⟨r, hr⟩ := hζ.exists_neg_pow_of_isOfFinOrder hno hx
  refine ⟨r % n, Nat.mod_lt _ (NeZero.pos _), ?_⟩
  rw [show ζ ^ (r % n) = ζ ^ r from (IsPrimitiveRoot.eq_orderOf hζ).symm ▸ pow_mod_orderOf .., hr]
  rcases Nat.even_or_odd r with (h | h) <;> simp [neg_pow, h.neg_one_pow]

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

Goal state before:
pp: 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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K⟮η + 1⟯.toSubalgebra

Tactic:
rw [H]

Goal state after:
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 η
hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s))
HKη : K⟮η⟯ = K⟮η + 1⟯
H : K⟮η + 1⟯.toSubalgebra = K[η + 1]
⊢ IsCyclotomicExtension {p ^ (k - s + 1)} K ↥K[η + 1]
Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots

Goal state before:
pp: case refine_2
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
⊢ (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K η) ^ Module.finrank (↥K⟮η⟯) L = ↑p ^ p ^ s

Tactic:
rw [H]

Goal state after:
case refine_2
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
⊢ ↑(p ^ (k - s + 1)).minFac ^ Module.finrank (↥K⟮η⟯) L = ↑p ^ p ^ s
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 ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s

Tactic:
Hex,

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 - s).succ - 1 + s)
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
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
h : d = N
⊢ False

Tactic:
simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₄.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Goal state after:
⊢ ∀ (a : ZMod 4), χ₄ a = 0 ∨ χ₄ a = 1 ∨ χ₄ a = -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₈.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Goal state after:
⊢ ∀ (a : ZMod 8), χ₈ a = 0 ∨ χ₈ a = 1 ∨ χ₈ a = -1
Module: Mathlib.NumberTheory.LegendreSymbol.ZModChar

Goal state before:
pp: ⊢ χ₈'.IsQuadratic

Tactic:
unfold MulChar.IsQuadratic

Goal state after:
⊢ ∀ (a : ZMod 8), χ₈' a = 0 ∨ χ₈' a = 1 ∨ χ₈' a = -1
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ ↑(ringChar R) = 0

Tactic:
rw [ringChar.Nat.cast_ringChar, χ.map_zero]

Goal state after: