mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case refine_2.inr
m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
gt : m < n
⊢ m ∈ Submodule.span ℕ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

Tactic:
exact Submodule.subset_span (by simpa using .inr ⟨gt, hm⟩)

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)
p_odd : Odd p
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
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
ha₅ : 2 * p * (b ^ 2 - 1) ∣ (b ^ 2 - 1) * (A * B - 1)
ha₇ : A * B ∣ b ^ (2 * p) - 1
q : ℕ
hq : A * B - 1 = 2 * p * q
⊢ b ^ (2 * p) - 1 ∣ b ^ (A * B - 1) - 1

Tactic:
simpa only [one_pow, pow_mul, hq] using Nat.sub_dvd_pow_sub_pow _ 1 q

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case inr
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
P : ℕ → Prop := fun n ↦ n ∉ AddSubmonoid.closure s
this : P 1
k : ℕ
gt : k > findGreatest P n
le : n ≤ k
⊢ k ∈ AddSubmonoid.closure s

Tactic:
exact hn k le (h.1.dvd.trans <| one_dvd k)

Goal state after:
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
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : S.b * (↑η + 1) + λ * k' = λ * k
⊢ S.b = λ * ((k - k') * -↑η)

Tactic:
apply_fun (· * -↑η) at hk

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
k k' : 𝓞 K
hk' : S.a + S.b = λ ^ 2 * k'
hk : (S.b * (↑η + 1) + λ * k') * -↑η = λ * k * -↑η
⊢ S.b = λ * ((k - k') * -↑η)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ (Multiset.map ((fun x ↦ log x) ∘ fun v ↦ max (v x) 1) archAbsVal).sum + ∑ᶠ (a : ↑nonarchAbsVal), log (max (↑a x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)

Tactic:
congr 2

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ Multiset.map ((fun x ↦ log x) ∘ fun v ↦ max (v x) 1) archAbsVal = Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal

case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ (fun a ↦ log (max (↑a x) 1)) = fun v ↦ log⁺ (↑v x)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 =
    log (↑n + 1) - log ↑n - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2)

Tactic:
congr 2

Goal state after:
case e_a.e_a
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2 = ∫ (x : ℝ) in ↑n..↑n + 1, x ^ (-2)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hf
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-s)) volume (↑n) (↑n + 1)

Tactic:
refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith

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

Goal state before:
pp: case hg
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ x ^ (-(s + 1))) volume (↑n) (↑n + 1)

Tactic:
refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith

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

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -(((↑n + 1) ^ (-(s - 1)) - ↑n ^ (-(s - 1))) / (s - 1)) = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1))

Tactic:
← neg_div,

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -((↑n + 1) ^ (-(s - 1)) - ↑n ^ (-(s - 1))) / (s - 1) = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * -(((↑n + 1) ^ (-s) - ↑n ^ (-s)) / s) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
← neg_div,

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (-((↑n + 1) ^ (-s) - ↑n ^ (-s)) / s) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ i ∈ p.support, v (coeff i p * ∏ i_1 ∈ i.support, x i_1 ^ i i_1) ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N

Tactic:
v.map_mul,

Goal state after:
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ x_1 ∈ p.support, v (coeff x_1 p) * v (∏ i ∈ x_1.support, x i ^ x_1 i) ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p * ∏ i ∈ s.support, x i ^ s i) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N

Tactic:
v.map_mul,

Goal state after:
case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p) * v (∏ i ∈ s.support, x i ^ s i) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommSemiring S
inst✝¹ : LinearOrder S
inst✝ : IsOrderedRing S
v : AbsoluteValue R S
hv : IsNonarchimedean ⇑v
ι : Type u_3
s : Finset ι
x : ι → R
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ v (x i)) ≤ ∏ i ∈ s, max (v (x i)) 1

Tactic:
exact sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)

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

Goal state before:
pp: case inl
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
⊢ (mulHeight fun j ↦ (eval 0) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight 0 ^ N

pp: case inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
· rcases eq_or_ne (fun j ↦ constantCoeff (p j)) 0 with h | h
    · simp [h]
    · simpa using le_max_of_le_left <| mulHeight_constantCoeff_le_mulHeightBound h

Goal state after:
case inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case bound_integrable
n : ℕ
⊢ IntervalIntegrable (fun x ↦ (x - ↑(n + 1)) / x ^ 2) volume (↑(n + 1)) (↑(n + 1) + 1)

Tactic:
exact_mod_cast term_welldef (by lia : 0 < (n + 1)) zero_lt_one

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

Goal state before:
pp: case h₁
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 ≤ x
⊢ 1 ≤ s

Tactic:
· exact hs

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

Goal state before:
pp: case h
this : ContinuousWithinAt termTSum (Ici 1) 1
⊢ Tendsto termTSum (𝓝[>] 1) (𝓝 (termTSum 1))

Tactic:
exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ¬a = 1

Tactic:
exact ne_of_gt ha

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

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
rw [hcd, mulHeight_zero, mul_one, show c = 0 from congrFun hcd 0,
      show d = 0 from congrFun hcd 1,
      show ![a * 0, a * 0 + b * 0, b * 0] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
    grw [← one_le_mulHeight]
    grind

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

Goal state before:
pp: s : ℝ
hs : s > 1
⊢ Real.log (riemannZeta ↑s).re = -Real.log (s - 1) + Real.log (riemannZeta₁ ↑s).re

Tactic:
have : (riemannZeta s).re = (s - 1)⁻¹ * (riemannZeta₁ s).re := by
    rw_mod_cast [riemannZeta_eq_inv_sub_mul (by aesop), re_ofReal_mul]
  rw [this, Real.log_mul, Real.log_inv] <;>
  grind [riemannZeta_re_pos_of_one_lt hs]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ ↑N ^ (-(1 - s)) * ∑ j, Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    ↑N ^ (s - 1) * (2 * ↑π) ^ (-s) * Gamma s *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
have (j : ZMod N) : Φ j * hurwitzZeta (toAddCircle j) (1 - s) = Φ j *
      ((2 * π) ^ (-s) * Gamma s * (cexp (-π * I * s / 2) *
      expZeta (toAddCircle j) s + cexp (π * I * s / 2) * expZeta (-toAddCircle j) s)) := by
    rcases eq_or_ne j 0 with rfl | hj
    · rcases hs' with hΦ | hs'
      · simp only [hΦ, zero_mul]
      · rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]
    · rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
⊢ ↑N ^ (-(1 - s)) * ∑ j, Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    ↑N ^ (s - 1) * (2 * ↑π) ^ (-s) * Gamma s *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ C *
      (↑N ^ (s - 1) *
        ∑ x,
          Φ x *
            (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s +
              cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s)) =
    C *
      (↑N ^ (s - 1) *
        (cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s))

Tactic:
congr 2

Goal state after:
case e_a.e_a
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ∑ x,
      Φ x *
        (cexp (-↑π * (I * s) / 2) * expZeta (toAddCircle x) s + cexp (↑π * (I * s) / 2) * expZeta (-toAddCircle x) s) =
    cexp (↑π * (I * s) / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * (I * s) / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ Complex.cos (↑π * (2 * ↑k) / 2) * (-1) ^ (k + 1) / (2 * ↑k) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
congr 2

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ Complex.cos (↑π * (2 * ↑k) / 2) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ Complex.sin (↑π * (2 * ↑k + 1) / 2) * (-1) ^ (k + 1) / (2 * ↑k + 1) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
congr 2

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ Complex.sin (↑π * (2 * ↑k + 1) / 2) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * (↑(if k = 1 then 1 else 0) - fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n) =
    1 / (-2 * ↑π * I * ↑n) *
      ((if k = 1 then 1 else 0) -
        ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n)

Tactic:
congr 2

Goal state after:
case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0

case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ fourierCoeffOn ⋯ (fun x ↦ ↑(↑k * bernoulliFun (k - 1) x)) n =
    ↑k * fourierCoeffOn bernoulliFourierCoeff._proof_1 (fun x ↦ ↑(bernoulliFun (k - 1) x)) n
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
erw [IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          ↑⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
n : ℤ
⊢ -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)

Tactic:
rw [mul_one_div, div_div, ← mul_pow]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
congr 2

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

Goal state before:
pp: case e'_5.e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ log (1 - χ ↑n * ↑n ^ (-(↑x + I * ↑y))) = log (1 - ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))))

Tactic:
congr 2

Goal state after:
case e'_5.e'_6.e_a
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n * ↑n ^ (-(↑x + I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y)))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ -((cexp (2 * ↑π * I * ↑x✝ * ↑x) - cexp (2 * ↑π * I * -↑x✝ * ↑x)) * I / 2) =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2

Tactic:
← neg_div,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ -((cexp (2 * ↑π * I * ↑x✝ * ↑x) - cexp (2 * ↑π * I * -↑x✝ * ↑x)) * I) / 2 =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x ↦ ↑n ^ ↑x * LSeries F ↑x) =ᶠ[atTop] fun x ↦ 0

Tactic:
simp only [h']

Goal state after:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) =ᶠ[atTop] fun x ↦ 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)

Tactic:
convert! hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one) using 1

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
⊢ (fun n ↦ 1 / ↑n ^ (2 * k)) = fun n ↦ 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

case e'_6
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_2
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ (C + C') * min (1 + (↑q.totient)⁻¹ / (C + C') / 2 - 1) (2 - 1) < (↑q.totient)⁻¹

Tactic:
add_sub_cancel_left,

Goal state after:
case refine_2
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ (C + C') * min ((↑q.totient)⁻¹ / (C + C') / 2) (2 - 1) < (↑q.totient)⁻¹
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ #(Ico 1 (p / 2).succ) * ↑(p / 2)!)

Tactic:
card_Ico,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ ((p / 2).succ - 1) * ↑(p / 2)!)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ x * q / p ≤ p / 2 * q / p

Tactic:
have := le_of_lt_succ (mem_Ico.mp hx).2; gcongr

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

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
rw [hb, zero_right] at h

Goal state after:
case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ χ₈ ↑b ^ (e + 1) = χ₈ ↑(b % (4 * a)) ^ (e + 1)

Tactic:
χ₈_nat_mod_eight,

Goal state after:
case inr.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ χ₈ ↑(b % 8) ^ (e + 1) = χ₈ ↑(b % (4 * a)) ^ (e + 1)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(↑a.natAbs | b) = J(↑a.natAbs | b % (4 * a.natAbs))

Tactic:
exact mod_right' a.natAbs hb

Goal state after: