mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x - 1
⊢ λ ∣ x * (x - 1) * (x - (↑⋯.unit + 1))

Tactic:
exact dvd_mul_of_dvd_left (dvd_mul_of_dvd_right h _) _

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n : ℕ
⊢ ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Tactic:
by
  grind [Pseudoperfect]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
by
  simp only [quadraticCharFun, ha, if_false]
  simp_rw [FiniteField.isSquare_iff hF ha]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ringChar F = 2
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
      quadraticCharFun_eq_one_of_char_two hF hab, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ ∑ x ∈ Finset.range b, 1 < ∑ k ∈ Finset.range b, a ^ k

Tactic:
refine Finset.sum_lt_sum (fun i hi => Nat.one_le_pow _ _ (by lia)) ?_
      exact ⟨1, Finset.mem_range.mpr (by lia), by simpa using! ha⟩

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n * 2 ^ (succ 1 + 1) + 1) % 8 = 1

Tactic:
← mod_add_mod,

Goal state after:
k n : ℕ
hn : 1 < n + succ 1
hp : Prime (k * 2 ^ (n + succ 1 + 1) + 1)
hpdvd : k * 2 ^ (n + succ 1 + 1) + 1 ∣ (n + succ 1).fermatNumber
this : Fact (Prime (k * 2 ^ (n + succ 1 + 1) + 1))
hp2 : k * 2 ^ (n + succ 1 + 1) + 1 ≠ 2
⊢ (k * 2 ^ n * 2 ^ (succ 1 + 1) % 8 + 1) % 8 = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (p * 2) - b ^ 2 = (b ^ p) ^ 2 - b ^ 2

Tactic:
by rw [pow_mul]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_2.«1»
⊢ (![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }]
        ((fun i ↦ i) ⟨1, ⋯⟩).castSucc,
      ![⊥, { asIdeal := span {2}, isPrime := ⋯ }, { asIdeal := maximalIdeal ℕ, isPrime := ⋯ }]
        ((fun i ↦ i) ⟨1, ⋯⟩).succ) ∈
    {(a, b) | a < b}

Tactic:
simp_rw [Nat.maximalIdeal_eq_span_two_three]
      exact SetLike.lt_iff_le_and_exists.mpr ⟨Ideal.span_mono (by simp),
        3, Ideal.subset_span (by simp), Ideal.mem_span_singleton.not.mpr <| by simp⟩

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1

Tactic:
have : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1 := by
      simpa only [one_pow] using Nat.sub_dvd_pow_sub_pow _ 1 c

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
k : ℕ
hk : p = 2 * k + 1
c : ℕ
hc : p - 1 = 2 * c
this : b ^ 2 - 1 ∣ (b ^ 2) ^ c - 1
⊢ b ^ 2 - 1 ∣ b ^ (p - 1) - 1
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ ∣ S.a + ↑η ^ 2 * S.b

Tactic:
show S.a + η ^ 2 * S.b = (S.a + S.b) + λ ^ 2 * S.b + 2 * λ * S.b by rw [coe_eta]; ring

Goal state after:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ S.a + ↑η * S.b
⊢ p ∣ λ
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ S.a + S.b
hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b
⊢ p ∣ λ

Tactic:
rw [← one_mul S.a, ← one_mul S.b] at hpab

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηsqb : p ∣ S.a + ↑η ^ 2 * S.b
⊢ p ∣ λ
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight (![y, x] ∘ ⇑e) = mulHeight ![y, x]

Tactic:
exact mulHeight_comp_equiv e ![y, x]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) * ↑↑((Algebra.norm ℤ) x).natAbs = 1

Tactic:
← absNorm_span_singleton,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) * ↑↑(absNorm (span {x})) = 1
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
h_prod,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
h_prod :
  ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ∏ᶠ (v : HeightOneSpectrum (𝓞 K)), ↑(absNorm (v.maxPowDividing (span {x}))) =
    1
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∀ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0

Tactic:
simp only [mem_insert, mem_singleton, forall_eq_or_imp, χ.map_zero, neg_zero, add_zero, map_one,
    mul_one, forall_eq, add_neg_cancel, ψ.map_zero, mul_zero, and_self]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

Tactic:
by
  rcases eq_or_ne s 1 with rfl | hs
  · have h : riemannZeta 1 = ((γ - Real.log (4 * π)) / 2 : ℝ) := by
      rw [riemannZeta_one, ofReal_div, ofReal_sub, ofReal_log (by positivity : (0 : ℝ) ≤ 4 * π)]
      norm_cast
    rw [map_one, h, conj_ofReal]
  · -- `conj ∘ ζ ∘ conj` is analytic on `{1}ᶜ` and agrees with `ζ` termwise on `1 < re z`, so
    -- the identity principle propagates the equality to the connected set `{1}ᶜ`.
    have hg_an : AnalyticOnNhd ℂ (fun z ↦ conj (riemannZeta (conj z))) {1}ᶜ :=
      DifferentiableOn.analyticOnNhd
        (fun z hz ↦ (differentiableAt_conj_conj_iff.mpr <| differentiableAt_riemannZeta <|
          (map_ne_one_iff _ (starRingEnd ℂ).injective).mpr hz).differentiableWithinAt)
        isOpen_compl_singleton
    have hgz (z : ℂ) (hz : 1 < z.re) : conj (riemannZeta (conj z)) = riemannZeta z := by
      rw [zeta_eq_tsum_one_div_nat_cpow (by rwa [conj_re]), conj_tsum,
        zeta_eq_tsum_one_div_nat_cpow hz]
      exact tsum_congr fun n ↦ by
        rw [map_div₀, map_one, ← conj_cpow _ _ (by rw [natCast_arg]; positivity), conj_natCast]
    have heq : EqOn (fun z ↦ conj (riemannZeta (conj z))) riemannZeta {1}ᶜ :=
      hg_an.eqOn_of_preconnected_of_eventuallyEq analyticOn_riemannZeta
        (isConnected_compl_singleton_of_one_lt_rank (by simp) 1).isPreconnected
        (by norm_num : (2 : ℂ) ∈ _)
        (eventuallyEq_of_mem
          ((isOpen_lt continuous_const continuous_re).mem_nhds (by norm_num)) hgz)
    simpa using congrArg (starRingEnd ℂ) (heq hs)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e'_9
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
h : -(log (2 * ↑π) * 2) = ↑γ - log (4 * ↑π) + (-log ↑π + -↑γ)
⊢ -log (2 * ↑π) / 2 =
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
          (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2) *
        (((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2)) * Gamma ∘ fun x ↦ x / 2 + 1)⁻¹ 0 +
      (id * completedRiemannZeta₀ - 1 - id / (1 - id)) 0 *
        (-((0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) *
                (Gamma ∘ fun x ↦ x / 2 + 1) 0 +
              ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2)) 0 * (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0))) /
          (((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2)) * Gamma ∘ fun x ↦ x / 2 + 1) 0 ^ 2)

Tactic:
simpa [completedRiemannZeta₀_zero, hasDerivAt_Gamma_one.deriv, field]

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
⊢ -log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)

Tactic:
simp only [logHeight_eq_log_mulHeight]
  rcases isEmpty_or_nonempty ι'
  · simp [show q = 0 from Subsingleton.elim .., mulHeight_eval_ge_aux p h,
      max_mulHeightBound_zero_one_eq_one K ι (ι × ι')]
  have : (Nat.card ι' : ℝ) ^ totalWeight K ≠ 0 := by simp
  pull (disch := first | assumption | positivity) log
  exact (log_le_log <| by positivity) <| mulHeight_eval_ge hq p h

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
⊢ x ∈ {x | mulHeight₁ x ≤ B} ↔ x ∈ ⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}

Tactic:
obtain ⟨n, hn₀, hn₁, hn⟩ := exists_nat_le_mulHeight₁ x

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : K
n : ℕ
hn₀ : n ≠ 0
hn₁ : ↑n ≤ mulHeight₁ x
hn : IsIntegral ℤ (↑n * x)
⊢ x ∈ {x | mulHeight₁ x ≤ B} ↔ x ∈ ⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
⊢ logHeight (Int.cast ∘ x) = log ↑(⨆ i, |x i|)

Tactic:
by
  rw [logHeight_eq_log_mulHeight, mulHeight_eq_max_abs_of_gcd_eq_one hx]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
f : R[X]
h : IsAdjoinRootMonic S f
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : Function.Surjective ⇑(aeval α)
monic : (minpoly R α).Monic
this✝ : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
φ : AdjoinRoot (minpoly R α) →ₐ[R] S := AdjoinRoot.liftAlgHom (minpoly R α) (Algebra.ofId R S) α ⋯
s : S
p : R[X]
hp : (aeval α) p = s
⊢ ∃ a, φ.toLinearMap a = s

Tactic:
exact ⟨AdjoinRoot.mk (minpoly R α) p, by simp [φ, ← aeval_def, hp]⟩

Goal state after:
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
z : ℂ
⊢ 1 < z.re → LFunction χ z = LSeries (fun x ↦ χ ↑x) z

Tactic:
hz

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
z : ℂ
hz : 1 < z.re
⊢ LFunction χ z = LSeries (fun x ↦ χ ↑x) z
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ (∫ (x : ℝ) in 0..(↑m)⁻¹, bernoulliFun (k + 1) (↑m * x)) -
      ∫ (x : ℝ) in 0..(↑m)⁻¹, ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) =
    0

pp: case hf
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (↑m * x)) volume 0 (↑m)⁻¹

pp: case hg
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0
    (↑m)⁻¹

Tactic:
intervalIntegral.integral_comp_mul_left _ m0',

Goal state after:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ((↑m)⁻¹ • ∫ (x : ℝ) in ↑m * 0..↑m * (↑m)⁻¹, bernoulliFun (k + 1) x) -
      ∫ (x : ℝ) in 0..(↑m)⁻¹, ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) =
    0

case hf
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (↑m * x)) volume 0 (↑m)⁻¹

case hg
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0
    (↑m)⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!

Tactic:
convert riemannZeta_two_mul_nat hk

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * ↑k - 1) = 2 ^ (2 * k - 1)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ 1 / ↑n ^ k * (fourier n) ↑y = -(2 * ↑π * I) ^ k / ↑k ! * (-↑k ! / (2 * ↑π * I * ↑n) ^ k) • (fourier n) ↑y

Tactic:
rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0

case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) (-↑2) = 0

Tactic:
ofReal_ofNat,

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) (-2) = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x = (fourier ↑x✝) ↑x + ((-1) ^ 2) ^ k * (fourier (-↑x✝)) ↑x

Tactic:
neg_one_sq,

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
x✝ : ℕ
⊢ (fourier ↑x✝) ↑x + (fourier (-↑x✝)) ↑x = (fourier ↑x✝) ↑x + 1 ^ k * (fourier (-↑x✝)) ↑x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((‖z‖ ^ n) ^ 2 - (z ^ n).re ^ 2))

Tactic:
hz

Goal state after:
case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * a ^ n + 4 * (a ^ n * (z ^ n).re) + a ^ n * ((z ^ n).re ^ 2 - ((1 ^ n) ^ 2 - (z ^ n).re ^ 2))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp only [rank_real_complex, Nat.one_lt_ofNat]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + ((-1) ^ 2) ^ k * (-1) ^ 1 * (fourier (-↑n)) ↑x)

Tactic:
neg_one_sq,

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + 1 ^ k * (-1) ^ 1 * (fourier (-↑n)) ↑x)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x ↦ LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x ↦ 1

Tactic:
refine IsBigO.mono ?_ nhdsWithin_le_nhds

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
⊢ (fun x ↦ LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x ↦ 1
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: ⊢ Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}

Tactic:
intro f hf g hg h
  push _ ∈ _ at hf hg
  replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h
  ext1 n
  cases n with
  | zero => exact hf.1.trans hg.1.symm
  | succ n => exact h _ n.zero_ne_add_one.symm

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))

Tactic:
refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).mpr hS.hasSum.tendsto_sum_nat) ?_

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ Tendsto (fun n ↦ ∑ i ∈ range (n + 1), LSeries.term f s i) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(bernoulli 4) / ↑4!

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]

Goal state after:
⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(-1 / 30) / ↑4!

⊢ 4 ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Tactic:
have hp' : Fact (p % 2 = 1) := ⟨(Nat.Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp⟩
  have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
  rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]

Goal state after: