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

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N,
      (1 / (s - 1) * (1 / ↑(n + 1) ^ (s - 1) - 1 / (↑(n + 1) + 1) ^ (s - 1)) -
        ↑(n + 1) / s * (1 / ↑(n + 1) ^ s - 1 / (↑(n + 1) + 1) ^ s)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
Finset.sum_sub_distrib

Goal state after:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) -
      ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
rcases isEmpty_or_nonempty ι'

Goal state after:
case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : IsEmpty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : Nonempty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖term (n + 1) s‖ ≤ term (n + 1) 1

Tactic:
term,

Goal state after:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ term (n + 1) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ term (n + 1) 1

Tactic:
term,

Goal state after:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ‖∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)‖ ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_2.e_a
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 := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))

Tactic:
rw [← prod_range_mul_prod_Ico _ (Nat.le_add_left k m), mul_comm _ (_ ^ #_), ← mul_assoc,
      prod_mul_pow_card]

Goal state after:
case refine_2.e_a
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 := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ a ∈ range k, Z (a + 1) * (μ - 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
hn : k < n
μ : R
hμ : IsPrimitiveRoot μ n
⊢ ∃ z ∈ ℤ[μ], ↑n = z * (μ - 1) ^ k

Tactic:
let n' + 1 := n
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.le_of_lt_succ hn)
  have hdvd k : ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1) := by
    refine ⟨(Finset.range k).sum (μ ^ ·), ?_, (geom_sum_mul μ k).symm⟩
    exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _
  let Z k := Classical.choose <| hdvd k
  have Zdef k : Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1) :=
    Classical.choose_spec <| hdvd k
  refine ⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1),
    ?_, ?_⟩
  · apply Subalgebra.mul_mem
    · apply Subalgebra.mul_mem
      · exact Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _
      · exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1
    · refine Subalgebra.prod_mem _ fun _ _ ↦ ?_
      apply Subalgebra.sub_mem
      · exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _
      · exact Subalgebra.one_mem _
  · push_cast
    have := Nat.cast_add (R := R) m k ▸ hμ.prod_pow_sub_one_eq_order
    rw [← this, mul_assoc, mul_assoc]
    congr 1
    conv => enter [2, 2, 2]; rw [← card_range k]
    rw [← prod_range_mul_prod_Ico _ (Nat.le_add_left k m), mul_comm _ (_ ^ #_), ← mul_assoc,
      prod_mul_pow_card]
    conv => enter [2, 1, 2, j]; rw [← (Zdef _).2]

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)
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
rcases isEmpty_or_nonempty ι'

Goal state after:
case inl
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)
h✝ : IsEmpty ι'
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

case inr
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)
h✝ : Nonempty ι'
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)
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
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)) →
        C * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
rcases isEmpty_or_nonempty ι'

Goal state after:
case inl
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
h✝ : IsEmpty ι'
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)) →
        C * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

case inr
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
h✝ : Nonempty ι'
⊢ ∃ C > 0,
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)) →
        C * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)
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 * log (mulHeight x) ≤
    log (mulHeight fun j ↦ (eval x) (p j))

Tactic:
rcases isEmpty_or_nonempty ι'

Goal state after:
case inl
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)
h✝ : IsEmpty ι'
⊢ -log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * log (mulHeight x) ≤
    log (mulHeight fun j ↦ (eval x) (p j))

case inr
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)
h✝ : Nonempty ι'
⊢ -log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * log (mulHeight x) ≤
    log (mulHeight fun j ↦ (eval x) (p j))
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inl
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)
h✝ : IsEmpty ι'
⊢ -log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * log (mulHeight x) ≤
    log (mulHeight fun j ↦ (eval x) (p j))

Tactic:
simp [show q = 0 from Subsingleton.elim .., mulHeight_eval_ge_aux p h,
      max_mulHeightBound_zero_one_eq_one K ι (ι × ι')]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
ha : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
⊢ ↑a / ↑n ∈ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}

Tactic:
simp only [Set.mem_ofPred_eq] at ha ⊢
    rw [mul_div_cancel₀ (a : K) hn', mulHeight₁_div_eq_mulHeight]
    exact ⟨a.isIntegral_coe, ha⟩

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

Goal state before:
pp: case e'_3.refine_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin 2
⊢ |![q.num, ↑q.den] i| ≤ max |q.num| ↑q.den

Tactic:
· fin_cases i <;> simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
⊢ (fun x ↦ Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp.coeff ⋯)
      ((fun g ↦ h.map { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }) g) =
    g

Tactic:
nontriviality R
    ext i
    simp only [h.modByMonicHom_map, Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
    rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
    · rw [Finsupp.mapDomain_apply Fin.val_injective]
    rw [degree_eq_natDegree h.monic.ne_zero, degree_lt_iff_coeff_zero]
    intro m hm
    rw [Polynomial.coeff]
    rw [Finsupp.mapDomain_of_notMem_range]
    rw [Set.mem_range, not_exists]
    rintro i rfl
    exact i.prop.not_ge hm

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst✝ : CommRing U
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
⊢ (h'.lift i x hx) ((h.algEquiv h') z) = (h.lift i x hx) z

Tactic:
rw [← h.map_repr z]; simp [-map_repr]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')
  have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'
  rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible 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 * (1 / ↑↑N ^ s * (1 / ↑((↑j.val + ↑N * ↑m) / ↑N) ^ s)) = Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s

Tactic:
by -- this is the delicate step!
    rw [one_div_mul_one_div, mul_one_div, mul_cpow_ofReal_nonneg] <;> positivity

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hint
k : ℕ
x y : ℝ
⊢ IntervalIntegrable (fun t ↦ ↑(k + 1) * bernoulliFun k t) volume x y

Tactic:
· exact Continuous.intervalIntegrable (by fun_prop) _ _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
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:
· exact Continuous.intervalIntegrable (by fun_prop) _ _

Goal state after:
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.ZetaValues

Goal state before:
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:
· exact Continuous.intervalIntegrable (by fun_prop) _ _

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ term (f + g) s = term f s + term g s

Tactic:
ext ⟨- | n⟩ <;>
  simp [add_div]

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

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (z / ↑m ^ ↑x) = z / (↑m / (↑n + 1)) ^ ↑x

Tactic:
rw [← mul_div_assoc, mul_comm, div_eq_mul_inv z, mul_div_assoc]

Goal state after:
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ z * ((↑n + 1) ^ ↑x / ↑m ^ ↑x) = z * ((↑m / (↑n + 1)) ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
⊢ r ≤ s.re

Tactic:
exact hs.le

Goal state after:
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:
by have := le_of_lt_succ (mem_Ico.mp hx).2; gcongr

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

Goal state before:
pp: case mp.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
hy0 : y ≠ 0
⊢ y ≤ x

Tactic:
rw [← map_one e.symm, ← map_inv_lt_iff, ← log_lt_log (by simp [hy0]) (by simp)] at hy

Goal state after:
case mp.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : (EquivLike.inv e.symm y).log < log 1
hy0 : y ≠ 0
⊢ y ≤ x
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

Tactic:
pick_goal 2

Goal state after:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a ^ x✝.succ | b) = J(a | b) ^ x✝.succ

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

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

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a ^ 2 | b) = 1

Tactic:
pow_left,

Goal state after:
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case nil
n : ℕ
⊢ J([].prod | n) = (List.map (fun a ↦ J(a | n)) []).prod

Tactic:
simp only [List.prod_nil, List.map_nil, one_left]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx✝ : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∀ (a : R), x = ϖ ^ n * a → g a = ⟨x, hx✝⟩

Tactic:
simp [g, LinearMap.codRestrict, eq_comm, mul_comm]

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

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ J(a | p) = -1 ↔ ¬IsSquare ↑a

Tactic:
rw [← legendreSym.to_jacobiSym]

Goal state after:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * qrSign m n * x

Tactic:
← pow_two,

Goal state after:
case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n ^ 2 * x
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * qrSign m n * y = y

Tactic:
← pow_two,

Goal state after:
case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n ^ 2 * y = y
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑2 ^ e | b) * (qrSign b a' * J(↑b | a')) =
    J(↑2 ^ e | b % (4 * a)) * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))

Tactic:
pow_left,

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑2 | b) ^ e * (qrSign b a' * J(↑b | a')) =
    J(↑2 ^ e | b % (4 * a)) * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑2 | b) ^ e * (qrSign b a' * J(↑b | a')) =
    J(↑2 ^ e | b % (4 * a)) * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))

Tactic:
pow_left,

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑2 | b) ^ e * (qrSign b a' * J(↑b | a')) =
    J(↑2 | b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
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))

pp: case inr
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:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ fastJacobiSymAux (a / 4) b flip ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
rw [IH (a / 4) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]

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

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K) x ≤ (valuation K) r} ⊆ s
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}

Tactic:
← (valuation K).restrict_le_iff

Goal state after:
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
⊢ IsCompact {x | (valuation K).restrict x ≤ (valuation K).restrict γ}
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : IsCompact Set.univ
this : IsDiscreteValuationRing ↥𝒪[K]
⊢ Finite 𝓀[K]

Tactic:
isCompact_iff_totallyBounded_isComplete,

Goal state after:
case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : TotallyBounded Set.univ ∧ IsComplete Set.univ
this : IsDiscreteValuationRing ↥𝒪[K]
⊢ Finite 𝓀[K]