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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
a b : K
x : Fin n → K
⊢ logHeight (vecCons a (vecCons b (vecCons 0 x))) = logHeight (vecCons a (vecCons b x))

Tactic:
simp [logHeight_eq_log_mulHeight]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n.natAbs) = mulHeight₁ x ^ n.natAbs

Tactic:
mulHeight₁_pow

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ x ^ n.natAbs = mulHeight₁ x ^ n.natAbs
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
⊢ logHeight (-x) = logHeight x

Tactic:
simp [logHeight_eq_log_mulHeight]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ (∏ᶠ (i : FinitePlace K), i ↑a) / ∏ᶠ (i : FinitePlace K), i ↑b =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹

Tactic:
prod_eq_inv_abs_norm_int ha,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / ∏ᶠ (i : FinitePlace K), i ↑b =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑s

Tactic:
congr 1 with n

Goal state after:
case e_f
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑((↑n + 1) ^ s) = 1 / (↑n + 1) ^ ↑s
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1.hx
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ (-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1) ∈ ℤ[μ]

pp: case refine_1.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ ℤ[μ]

Tactic:
· apply Subalgebra.mul_mem
      · exact Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _
      · exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1

Goal state after:
case refine_1.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ ℤ[μ]
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = ↑(Fintype.card F) - 2

Tactic:
calc ∑ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x)
  _ = ∑ _ ∈ univ \ {0, 1}, 1 := sum_congr rfl this
  _ = #(univ \ {0, 1}) := (cast_card _).symm
  _ = Fintype.card F - 2 := by
    rw [card_sdiff_of_subset (subset_univ _), card_univ, card_pair zero_ne_one,
      Nat.cast_sub <| Nat.add_one_le_of_lt Fintype.one_lt_card, Nat.cast_two]

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

Goal state before:
pp: case «0»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨0, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨0, ⋯⟩) ^ (1 + 1)

Tactic:
simp [p, q, Fin.sum_univ_three]

Goal state after:
case «0»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ a✝ * c✝ * (a✝ * c✝) = (a✝ * c✝) ^ 2
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «1»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨1, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨1, ⋯⟩) ^ (1 + 1)

Tactic:
simp [p, q, Fin.sum_univ_three]

Goal state after:
case «1»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ a✝ * d✝ * (a✝ * d✝ + b✝ * c✝) + -(a✝ * c✝ * (b✝ * d✝)) = (a✝ * d✝) ^ 2
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «2»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨2, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨2, ⋯⟩) ^ (1 + 1)

Tactic:
simp [p, q, Fin.sum_univ_three]

Goal state after:
case «2»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ b✝ * c✝ * (a✝ * d✝ + b✝ * c✝) + -(a✝ * c✝ * (b✝ * d✝)) = (b✝ * c✝) ^ 2
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case «3»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ ∑ j,
      (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (q ((fun i ↦ i) ⟨3, ⋯⟩, j)) *
        (eval ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝]) (p j) =
    ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ((fun i ↦ i) ⟨3, ⋯⟩) ^ (1 + 1)

Tactic:
simp [p, q, Fin.sum_univ_three]

Goal state after:
case «3»
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ b✝ * d✝ * (b✝ * d✝) = (b✝ * d✝) ^ 2
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case refine_3
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0

Tactic:
exact Polynomial.map_monic_ne_zero (minpoly.monic hx')

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s = Φ j / (↑j.val + ↑N * ↑m) ^ s

Tactic:
by
    rw [mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr (NeZero.ne N))]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), LSeries.term (fun x ↦ 𝕖 (j * ↑x)) s n = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s

Tactic:
congr 1 with n

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ LSeries.term (fun x ↦ 𝕖 (j * ↑x)) s n = cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑n) / ↑n ^ s
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case pos.hb
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  ↑(Multiset.count (normalize J) (normalizedFactors (Ideal.map (algebraMap R S) I))) =
    emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Polynomial.map (Ideal.Quotient.mk I) (minpoly R x) ≠ 0

Tactic:
exact Polynomial.map_monic_ne_zero (minpoly.monic hx')

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(2 * ↑k) ≠ -↑n

Tactic:
← Int.cast_natCast n,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(2 * ↑k) ≠ -↑↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(2 * ↑k) + 1 ≠ -↑n

Tactic:
← Int.cast_natCast n,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(2 * ↑k) + 1 ≠ -↑↑n
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
simp_rw [this]

Goal state after:
k : ℕ
hk : 2 ≤ k
this : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
⊢ Summable fun n ↦ -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x ↦ ‖1 / ↑x ^ k‖) = fun x ↦ |1 / ↑x ^ k|
⊢ Summable fun a ↦ ‖1 / ↑a ^ k‖

Tactic:
simp_rw [this]

Goal state after:
k : ℕ
hk : 2 ≤ k
this✝ : ∀ (n : ℤ), -↑k ! / (2 * ↑π * I * ↑n) ^ k = -↑k ! / (2 * ↑π * I) ^ k * (1 / ↑n ^ k)
this : (fun x ↦ ‖1 / ↑x ^ k‖) = fun x ↦ |1 / ↑x ^ k|
⊢ Summable fun x ↦ |1 / ↑x ^ k|
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inl
k : ℕ
hk : 2 ≤ k
x : ℝ
hx✝ : x ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
hx : x ∈ Ico 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

pp: case inr
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑1) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1))

Tactic:
· exact this hx

Goal state after:
case inr
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑1) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

Tactic:
by_cases! hm : n + 1 < m

Goal state after:
case pos
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : n + 1 < m
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

case neg
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : m ≤ n + 1
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))) =
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2).re

Tactic:
· convert! (ofReal_re _).symm
    rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one]
    rw [bernoulliFun]
    ring

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * (∑' (p : Nat.Primes), -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))).re +
        4 * (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re

Tactic:
rw [re_tsum H₀, re_tsum H₁, re_tsum H₂, ← tsum_mul_left, ← tsum_mul_left,
    ← hsum₀.tsum_add hsum₁, ← (hsum₀.add hsum₁).tsum_add hsum₂]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    ∑' (b : Nat.Primes),
      (3 * (-log (1 - 1 ↑↑b * ↑↑b ^ (-(1 + ↑x)))).re + 4 * (-log (1 - χ ↑↑b * ↑↑b ^ (-(1 + ↑x + I * ↑y)))).re +
        (-log (1 - (χ ^ 2) ↑↑b * ↑↑b ^ (-(1 + ↑x + 2 * I * ↑y)))).re)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))

Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn

Goal state after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg.refine_1
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
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn

Goal state after:
case neg.refine_1
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
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (-↑b).valMinAbs.natAbs = b

Tactic:
natAbs_valMinAbs_neg,

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (↑b).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p q : ℕ
hp0 : p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p = #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q})

Tactic:
simp [hp0]

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

Goal state before:
pp: b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp ↦ legendreSym p 1) b.primeFactorsList ⋯
⊢ z = 1

Tactic:
by
    let ⟨p, hp, he⟩ := List.mem_pmap.1 hz
    rw [← he, legendreSym.at_one]

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R

Tactic:
· rw [isNontrivial_iff_nontrivial_units] at h; push Not at h
    refine ⟨⟨0, zero_lt_one, fun y hy ↦ ?_⟩⟩
    contrapose! hy
    have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _
    exact Units.val_le_val.mpr this.le

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

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ a.gcd ↑b ≠ 1

Tactic:
Int.gcd_eq_natAbs,

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (h : a_1 ∈ b.primeFactorsList), legendreSym a_1 a = 0) ↔ a.natAbs.gcd (↑b).natAbs ≠ 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * (-1 ^ (-s + 1) / (-s + 1))) = ε

Tactic:
Real.one_rpow

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * (-1 / (-s + 1))) = ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case h
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'
⊢ 4 * a = 8 * (2 ^ e * a')

Tactic:
rw [ha₂, Nat.pow_succ]

Goal state after:
case h
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'
⊢ 4 * (2 ^ e * 2 * a') = 8 * (2 ^ e * a')