mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Fourier.LpSpace

Goal state before:
pp: case hp
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)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ IsClosed {b | p b}

pp: case ih
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)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ ∀ (a : 𝓢(E, F)), p ((toLpCLM ℝ F 2 volume) a)

Tactic:
· apply isClosed_eq
    · exact (fourierCLM ℂ 𝓢'(E, F) ∘L toTemperedDistributionCLM F volume 2).continuous
    · exact (toTemperedDistributionCLM F volume 2 ∘L fourierCLM ℂ (Lp (α := E) F 2)).continuous

Goal state after:
case ih
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)
p : ↥(Lp F 2 volume) → Prop := ⋯
⊢ ∀ (a : 𝓢(E, F)), p ((toLpCLM ℝ F 2 volume) a)
Module: Mathlib.Analysis.Distribution.TemperedDistribution

Goal state before:
pp: case h
E : Type u_3
F : Type u_4
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
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : (toTemperedDistributionCLM F μ p) f = 0
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
⊢ ∫ (x : E), g x • ↑↑f x ∂μ = 0

Tactic:
have hg₁ : HasCompactSupport (Complex.ofRealCLM ∘ g) := g_cpt.comp_left rfl

Goal state after:
case h
E : Type u_3
F : Type u_4
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
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
f : ↥(Lp F p μ)
hf : (toTemperedDistributionCLM F μ p) f = 0
g : E → ℝ
g_smooth : ContDiff ℝ ∞ g
g_cpt : HasCompactSupport g
hg₁ : HasCompactSupport (⇑Complex.ofRealCLM ∘ g)
⊢ ∫ (x : E), g x • ↑↑f x ∂μ = 0
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
inst✝ : CompleteSpace F
s : ℝ
p : ℝ≥0∞
hp : Fact (1 ≤ p)
⊢ MemSobolev s p 0

Tactic:
use 0
  rw [← Lp.toTemperedDistributionCLM_apply]
  simp only [map_zero]

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

Goal state before:
pp: d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ volume = Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume))

Tactic:
convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm

Goal state after:
case e'_2
d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ volume = Measure.pi fun i ↦ volume

case e'_3
d : Type u_1
inst✝ : Fintype d
a : d → ℝ
this :
  Measure.map (fun x i ↦ ↑(x i)) (Measure.map Subtype.val (Measure.comap Subtype.val volume)) =
    Measure.map (fun x i ↦ ↑(↑x i)) (Measure.comap Subtype.val volume)
⊢ Measure.map Subtype.val (Measure.comap Subtype.val volume) = Measure.pi fun i ↦ volume.restrict (Ioc (a i) (a i + 1))
Module: Mathlib.Analysis.Fourier.Convolution

Goal state before:
pp: case e_f
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ : E
⊢ (fun y ↦ ∫ (x : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y)) = fun y ↦
    ∫ (x : E), 𝐞 (-inner ℝ (y + x) ξ) • (B (f₁ x)) (f₂ y)

Tactic:
ext y

Goal state after:
case e_f
𝕜 : Type u_1
E : Type u_3
F₁ : Type u_5
F₂ : Type u_6
F₃ : Type u_7
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup F₁
inst✝⁹ : NormedAddCommGroup F₂
inst✝⁸ : NormedAddCommGroup F₃
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedSpace 𝕜 F₁
inst✝² : NormedSpace 𝕜 F₂
inst✝¹ : NormedSpace 𝕜 F₃
inst✝ : NormedSpace ℂ F₃
B : F₁ →L[𝕜] F₂ →L[𝕜] F₃
f₁ : E → F₁
f₂ : E → F₂
hf₁ : Integrable f₁ volume
hf₂ : Integrable f₂ volume
ξ y : E
⊢ ∫ (x : E), 𝐞 (-inner ℝ x ξ) • (B (f₁ (x - y))) (f₂ y) = ∫ (x : E), 𝐞 (-inner ℝ (y + x) ξ) • (B (f₁ x)) (f₂ y)
Module: Mathlib.Analysis.RCLike.Inner

Goal state before:
pp: case refine_2
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪toLp 2 (f k₁), toLp 2 (f k₂)⟫_𝕜 = 0
this : LinearIndependent 𝕜 fun i ↦ toLp 2 (f i)
⊢ LinearIndependent 𝕜 f

pp: case refine_1
ι : Type u_1
κ : Type u_2
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f : κ → ι → 𝕜
hf : ∀ (k : κ), f k ≠ 0
hinner : Pairwise fun k₁ k₂ ↦ ⟪toLp 2 (f k₁), toLp 2 (f k₂)⟫_𝕜 = 0
⊢ ∀ (i : κ), toLp 2 (f i) ≠ 0

Tactic:
exacts [(WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm.toLinearMap.linearIndependent_iff_of_injOn
    (toLp_injective 2).injOn |>.1 this, fun i ↦ (toLp_eq_zero 2).ne.2 (hf i)]

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 𝓕 (delta 0) = volume.toTemperedDistribution

Tactic:
ext f

Goal state after:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : 𝓢(E, ℂ)
⊢ (𝓕 (delta 0)) f = volume.toTemperedDistribution 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✝¹ : 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)]

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 : ℝ
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))) * fun x ↦ ↑((1 + ‖x‖ ^ 2) ^ (-s / 2)))) (𝓕 f)
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
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
this : (fun v ↦ 𝐞 (-⟪v, w⟫) • f (v + i w)) = fun v ↦ (fun x ↦ -(𝐞 (-⟪x, w⟫) • f x)) (v + i w)
⊢ ∫ (x : V), -(𝐞 (-⟪x, w⟫) • f x) ∂volume = -∫ (v : V), 𝐞 (-⟪v, w⟫) • f v

Tactic:
simp only [integral_neg]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n 1, (X - C ζ)

Tactic:
classical
  rw [nthRootsFinset, ← Multiset.toFinset_eq (IsPrimitiveRoot.nthRoots_one_nodup h)]
  simp only [Finset.prod_mk]
  rw [nthRoots]
  have hmonic : (X ^ n - C (1 : R)).Monic := monic_X_pow_sub_C (1 : R) (ne_of_lt hpos).symm
  symm
  apply prod_multiset_X_sub_C_of_monic_of_roots_card_eq hmonic
  rw [@natDegree_X_pow_sub_C R _ _ n 1, ← nthRoots]
  exact IsPrimitiveRoot.card_nthRoots_one h

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

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

Tactic:
obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x :=
      (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h

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

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

pp: case mpr
n : ℕ
inst✝ : NeZero n
x : ℂˣ
hn0 : ↑n ≠ 0
⊢ (∃ i < n, cexp (2 * ↑π * I * (↑i / ↑n)) = ↑x) → ↑x ^ n = 1

Tactic:
· intro h
    obtain ⟨i, hi, H⟩ : ∃ i < (n : ℕ), exp (2 * π * I / n) ^ i = x :=
      (isPrimitiveRoot_exp n NeZero.out).eq_pow_of_pow_eq_one h
    refine ⟨i, hi, ?_⟩
    rw [← H, ← exp_nat_mul]
    congr 1
    ring

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

Goal state before:
pp: n : ℕ
ζ : ℂ
h : IsPrimitiveRoot ζ n
hn : n ≠ 0
⊢ ∃ i, ζ.arg = ↑i / ↑n * (2 * Real.pi) ∧ IsCoprime i ↑n ∧ i.natAbs < n

Tactic:
by
  rw [Complex.isPrimitiveRoot_iff _ _ hn] at h
  obtain ⟨i, h, hin, rfl⟩ := h
  rw [mul_comm, ← mul_assoc, Complex.exp_mul_I]
  refine ⟨if i * 2 ≤ n then i else i - n, ?_, ?isCoprime, by lia⟩
  case isCoprime =>
    replace hin := Nat.isCoprime_iff_coprime.mpr hin
    split_ifs
    · exact hin
    · convert! hin.add_mul_left_left (-1) using 1
      rw [mul_neg_one, sub_eq_add_neg]
  split_ifs with h₂
  · convert! Complex.arg_cos_add_sin_mul_I _
    · push_cast; rfl
    · push_cast; rfl
    simp only [Int.cast_natCast, Set.mem_Ioc]
    refine ⟨(neg_lt_neg Real.pi_pos).trans_le ?_, ?_⟩
    · rw [neg_zero]
      positivity
    refine Eq.trans_le (b := Real.pi * (i * 2 / n)) (by ring) ?_
    rw [← mul_one n] at h₂
    exact mul_le_of_le_one_right Real.pi_pos.le
      ((div_le_iff₀' <| mod_cast pos_of_gt h).mpr <| mod_cast h₂)
  rw [← Complex.cos_sub_two_pi, ← Complex.sin_sub_two_pi]
  convert! Complex.arg_cos_add_sin_mul_I _
  · push_cast
    rw [← sub_one_mul, sub_div, div_self]
    exact mod_cast hn
  · push_cast
    rw [← sub_one_mul, sub_div, div_self]
    exact mod_cast hn
  simp only [Int.cast_sub, Int.cast_natCast, Set.mem_Ioc]
  field_simp
  constructor
  · push Not at h₂
    rify at h₂
    linear_combination h₂
  · rify at h
    linear_combination 2 * h + (n : ℝ) * one_pos (α := ℝ)

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

Goal state before:
pp: n : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ map f (cyclotomic n R) = cyclotomic n S

Tactic:
rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
  have : Subsingleton (ℤ →+* S) := inferInstance
  congr!

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℕ
a✝ : Nontrivial R
⊢ (cyclotomic n R).natDegree ≤ n.totient

Tactic:
natDegree_cyclotomic

Goal state after:
R : Type u_1
inst✝ : Ring R
n : ℕ
a✝ : Nontrivial R
⊢ n.totient ≤ n.totient
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Roots

Goal state before:
pp: n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
⊢ False

Tactic:
have hn := (X_pow_sub_one_separable_iff.mpr <| NeZero.natCast_ne n K).squarefree

Goal state after:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
j : K[X]
hj : cyclotomic n K = (X - C μ) * j
this : (∏ x ∈ n.divisors \ {i, n}, cyclotomic x K) * ((X - C μ) * k * ((X - C μ) * j)) = X ^ n - 1
hn : Squarefree (X ^ n - 1)
⊢ False
Module: Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : DecidableEq R
hp : Nat.Prime p
⊢ nthRootsFinset p 1 = primitiveRoots p R ∪ {1}

Tactic:
by
  simp [nthRoots_one_eq_biUnion_primitiveRoots, hp.divisors]

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

Goal state before:
pp: case pos
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
x : A
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
n : ℕ
a✝¹ : Nontrivial A
a✝ : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
i : Fin B.dim
h✝ : ⟨0, ⋯⟩ = i
⊢ IsIntegral R 1

Tactic:
exact isIntegral_one

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
⊢ 0 < eval x (cyclotomic n R)

Tactic:
have hn' : 0 < n := pos_of_gt hn

Goal state after:
case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℕ
ih : ∀ m < n, 2 < m → 0 < eval x (cyclotomic m R)
hn : 2 < n
hn' : 0 < n
⊢ 0 < eval x (cyclotomic n 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
⊢ (cyclotomic n K).natDegree = φ n

Tactic:
natDegree_cyclotomic

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
⊢ φ n = φ n
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 ℤ)) *
      ↑p ^ #(range (padicValNat p n))
⊢ False

Tactic:
Finset.card_range,

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 ℤ)) *
      ↑p ^ padicValNat p n
⊢ False
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_2.inr
S T : Set ℕ
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ T ∧ n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}

Tactic:
exact ⟨n, Or.inr hn.1, hn.2⟩

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

Goal state before:
pp: case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (-1) ^ (cyclotomic n K).natDegree = 1

Tactic:
natDegree_cyclotomic

Goal state after:
case neg
n : ℕ
inst✝⁵ : NeZero n
K : Type u
L : Type v
inst✝⁴ : CommRing L
ζ : L
inst✝³ : Field K
inst✝² : Algebra K L
hζ : IsPrimitiveRoot ζ n
inst✝¹ : IsDomain L
inst✝ : IsCyclotomicExtension {n} K L
hn : n ≠ 2
hirr : Irreducible (cyclotomic n K)
this : NeZero ↑n
h1 : 2 ≤ n
⊢ (-1) ^ φ n = 1
Module: Mathlib.NumberTheory.Cyclotomic.Basic

Goal state before:
pp: case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ x ∈ ↑A[ζ]

Tactic:
suffices hx : x ^ n = 1 by
      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)

Goal state after:
case refine_1
A : Type u
B : Type v
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
n : ℕ
inst✝¹ : NeZero n
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ (cyclotomic n A).rootSet B
⊢ x ^ n = 1
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
⊢ (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s

Tactic:
have hirr₁ : Irreducible (cyclotomic (p ^ (k - s + 1)) K) :=
    cyclotomic_irreducible_pow_of_irreducible_pow hpri.1 (by lia) hirr
  set η := ζ ^ p ^ s - 1
  let η₁ : K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
  have hη : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by
    rw [sub_add_cancel]
    refine IsPrimitiveRoot.pow (pos_of_neZero (p ^ (k + 1))) hζ ?_
    rw [← pow_add, add_comm s, Nat.sub_add_cancel (le_trans hs (Nat.le_succ k))]
  have : IsCyclotomicExtension {p ^ (k - s + 1)} K K⟮η⟯ := by
    have HKη : K⟮η⟯ = K⟮η + 1⟯ := by
      refine le_antisymm ?_ ?_
      all_goals rw [IntermediateField.adjoin_simple_le_iff]
      · nth_rw 2 [← add_sub_cancel_right η 1]
        exact sub_mem (IntermediateField.mem_adjoin_simple_self K (η + 1)) (one_mem _)
      · exact add_mem (IntermediateField.mem_adjoin_simple_self K η) (one_mem _)
    rw [HKη]
    have H := IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
      ((integral {p ^ (k + 1)} K L).isIntegral (η + 1)).isAlgebraic
    refine IsCyclotomicExtension.equiv _ _ _ (h := ?_) (.refl : K⟮η + 1⟯.toSubalgebra ≃ₐ[K] _)
    rw [H]
    have hη' : IsPrimitiveRoot (η + 1) (p ^ (k + 1 - s)) := by simpa using hη
    convert! hη'.adjoin_isCyclotomicExtension K using 1
    rw [Nat.sub_add_comm hs]
  replace hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1)) := by
    apply coe_submonoidClass_iff.1
    convert! hη using 1
    rw [Nat.sub_add_comm hs]
  have := IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} K L
  have := IsCyclotomicExtension.isGalois {p ^ (k + 1)} K L
  rw [norm_eq_norm_adjoin K]
  have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo
  swap; · exact hpri.1.isPrimePow.pow (Nat.succ_ne_zero _)
  rw [add_sub_cancel_right] at H
  rw [H]
  congr
  · rw [Nat.pow_minFac, hpri.1.minFac_eq]
    exact Nat.succ_ne_zero _
  have := Module.finrank_mul_finrank K K⟮η⟯ L
  rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁,
    Nat.totient_prime_pow hpri.out (k - s).succ_pos, Nat.totient_prime_pow hpri.out k.succ_pos,
    mul_comm _ (p - 1), mul_assoc, mul_comm (p ^ (k.succ - 1))] at this
  replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this
  have Hex : k.succ - 1 = (k - s).succ - 1 + s := by
    simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]
    exact (Nat.sub_add_cancel hs).symm
  rw [Hex, pow_add] at this
  exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this

Goal state after:
Module: Mathlib.Data.ZMod.Units

Goal state before:
pp: case inr
n : ℤ
m : ℕ
h : IsUnit ↑n
hm : m ≠ 0
⊢ IsCoprime (↑m) n

Tactic:
have : NeZero m := ⟨hm⟩

Goal state after:
case inr
n : ℤ
m : ℕ
h : IsUnit ↑n
hm : m ≠ 0
this : NeZero m
⊢ IsCoprime (↑m) n
Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod ↑pp) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar F (CyclotomicField (↑ψ.n) F') := ψ.char.compAddMonoidHom (Algebra.trace (ZMod p) F).toAddMonoidHom
hψ' : ψ' ≠ 1
⊢ PrimitiveAddChar F F'

Tactic:
exact ⟨ψ.n, ψ', IsPrimitive.of_ne_one hψ'⟩

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

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
k : Type u_3
inst✝² : AddCommGroup k
inst✝¹ : Fintype k
inst✝ : Module (ZMod p) k
⊢ p ^ Module.finrank (ZMod p) k = Fintype.card k

Tactic:
rw [pow_finrank_eq_natCard, Fintype.card_eq_nat_card]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑(⋯.lift ↑(↑j / ↑N)) = cexp (2 * ↑π * I * ↑j / ↑N)

Tactic:
Function.Periodic.lift_coe,

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ℤ
⊢ ↑(Circle.exp (2 * π / 1 * (↑j / ↑N))) = cexp (2 * ↑π * I * ↑j / ↑N)
Module: Mathlib.NumberTheory.MulChar.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (x y : R),
    (if hx : IsUnit (x * y) then ↑(f hx.unit) else 0) =
      (if hx : IsUnit x then ↑(f hx.unit) else 0) * if hx : IsUnit y then ↑(f hx.unit) else 0

Tactic:
by
    classical
      intro x y
      by_cases hx : IsUnit x
      · simp only [hx, IsUnit.mul_iff, true_and, dif_pos]
        by_cases hy : IsUnit y
        · simp only [hy, dif_pos]
          have hm : (hx.mul hy).unit = hx.unit * hy.unit := Units.ext rfl
          rw [hm, map_mul]
          norm_cast
        · simp only [hy, not_false_iff, dif_neg, mul_zero]
      · simp only [hx, IsUnit.mul_iff, false_and, not_false_iff, dif_neg, zero_mul]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommMonoid R
R' : Type u_2
inst✝² : CommMonoidWithZero R'
S : Type u_3
inst✝¹ : SetLike S R
inst✝ : SubmonoidClass S R
T : S
χ : MulChar R R'
⊢ domRestrict T χ = 1 ↔ ∀ (x : (↥T)ˣ), χ ↑↑x = 1

Tactic:
by
  simp [eq_one_iff]

Goal state after: