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

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))

Tactic:
have h_denom_rat : (2 * (k : ℚ) - 2 * m + 1) = ((d + 1 : ℕ) : ℚ) := by
    simp only [hd_def]; push_cast [Nat.cast_sub hkm]; ring

Goal state after:
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : 2 * ↑k - 2 * ↑m + 1 = ↑(d + 1)
⊢ pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (d - 1) / (2 * ↑k - 2 * ↑m + 1))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x = ψ ↑⌊x⌋₊

Tactic:
unfold psi
  rw [floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ (∑ n ∈ Ioc 0 ⌊x⌋₊, Λ n - ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) =
    ∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then Λ a else 0

Tactic:
← sum_sub_distrib

Goal state after:
x : ℝ
⊢ ∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ x - if Nat.Prime x then log ↑x else 0) = ∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then Λ a else 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ¬p ∣ r.den

Tactic:
rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ 1 ≤ ‖↑↑r.den‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ θ t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)

Tactic:
theta_le_log4_mul_x (by linarith)

Goal state after:
x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ log 4 * t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑(p ^ n)} → x - ↑b ∈ Ideal.span {↑(p ^ n)} → ↑a = ↑b

Tactic:
intro x a b ha hb
      apply zmod_congr_of_sub_mem_span n x a b
      · simpa using ha
      · simpa using hb

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}

Tactic:
by
  ext x
  rw [RingHom.mem_ker]
  constructor
  · intro h
    suffices x.appr n = 0 by
      convert! appr_spec n x
      simp only [this, sub_zero, cast_zero]
    dsimp [toZModPow, toZModHom] at h
    rw [ZMod.natCast_eq_zero_iff] at h
    apply eq_zero_of_dvd_of_lt h (appr_lt _ _)
  · intro h
    rw [← sub_zero x] at h
    dsimp [toZModPow, toZModHom]
    rw [zmod_congr_of_sub_mem_span n x _ 0 _ h, cast_zero]
    apply appr_spec

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ discr K = discr L

Tactic:
rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f,
    ← discr_eq_discr L ((RingOfIntegers.basis K).map f₀)]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = ↑(Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)
i j : ι'
⊢ b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j = b'.toMatrix (⇑b) i ((b.indexEquiv b').symm j)

Tactic:
simp [Basis.toMatrix_apply]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
⊢ lift f_compat = g

Tactic:
by
  ext1 r
  apply eq_of_forall_dist_le
  intro ε hε
  obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
  apply le_trans _ (le_of_lt hn)
  rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker,
    map_sub, ← RingHom.comp_apply, ← RingHom.comp_apply, lift_spec, hg, sub_self]

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
by
  have : NumberField K := @NumberField.mk _ _ _ (IsCyclotomicExtension.finiteDimensional {n} ℚ K)
  have H₁ : (aeval (hζ.powerBasis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.subOnePowerBasis ℚ).gen := by simp
  have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp
  refine discr_eq_discr_of_toMatrix_coeff_isIntegral _ (fun i j => toMatrix_isIntegral H₁ ?_ ?_ _ _)
    fun i j => toMatrix_isIntegral H₂ ?_ ?_ _ _
  · exact hζ.isIntegral (NeZero.pos _)
  · refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) (hζ.isIntegral (NeZero.pos _))
  · exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
  · refine minpoly.isIntegrallyClosed_eq_field_fractions' (K := ℚ) ?_
    exact (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
hn : 1 ≤ { re := x, im := -y }
t : { re := x, im := y } * 1 ≤ { re := x, im := y } * { re := x, im := -y }
⊢ False

Tactic:
rw [bm, mul_one] at t

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
x y : ℤ
h1 : 1 ≤ { re := x, im := y }
hp : IsPell { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬{ re := ↑a, im := 1 } ≤ { re := x, im := y }
h1l : 1 < { re := x, im := y }
bm : { re := x, im := y } * { re := { re := x, im := y }.re, im := -{ re := x, im := y }.im } = 1
hn : 1 ≤ { re := x, im := -y }
t : { re := x, im := y } ≤ 1
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n := by
          rcases k with - | k <;> simp [_root_.pow_succ]; ring_nf
        rw [← this]
        gcongr

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ n + n - (n + 1) = n - 1

Tactic:
tsub_add_eq_tsub_tsub,

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
⊢ n + n - n - 1 = n - 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
⊢ xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]

Tactic:
induction q with
    | zero => simp [ModEq.refl]
    | succ q IH =>
      rw [Nat.mul_succ, ← add_assoc, add_comm]
      exact (xn_modEq_x4n_add _ _ _).trans IH

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

Goal state before:
pp: ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos
  replace h : |ξ * q.den - q.num| < 1 / q.den := by
    rw [← mul_lt_mul_iff_left₀ hq₀] at h
    conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
    rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
  constructor
  · rcases eq_or_ne ξ q with (rfl | H)
    · exact le_rfl
    · have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
      rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' hξ₀.ne', abs_div, abs_of_pos hξ₀,
        div_lt_iff₀ hξ₀, div_mul_comm, mul_one] at h
      refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le
      norm_cast
      rw [mul_comm _ q.num]
      exact Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)
  · obtain ⟨h₁, h₂⟩ :=
      abs_sub_lt_iff.mp
        (h.trans_le <|
          (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
    rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
    rw [← sub_lt_iff_lt_add] at h₂
    norm_cast at h₁ h₂
    exact
      ⟨sub_le_iff_le_add.mpr (Int.ceil_le.mpr h₁.le), sub_le_iff_le_add.mp (Int.le_floor.mpr h₂.le)⟩

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q ∈ insert p s

Tactic:
rw [mem_primeFactorsList hp'] at H
    rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]
    exact Finset.mem_insert_self p s

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

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * g p.2 / (↑p.2 * ↑p.1) ^ s

Tactic:
← cast_mul,

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 ≠ 0
hp₂ : p.2 ≠ 0
⊢ f p.1 * g p.2 / ↑n ^ s = f p.1 * g p.2 / ↑(p.2 * p.1) ^ s
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n ↦ ‖f p ^ n‖

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ s with Nat.Prime p, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable (HPow.hPow ‖f p‖)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(u - ⌊ξ⌋ * ↑v).toNat
n : ℕ
hn : ↑↑v / ↑(u - ⌊ξ⌋ * ↑v).toNat = (fract ξ)⁻¹.convergent n
⊢ ↑u / ↑v = ↑⌊ξ⌋ + (↑u / ↑v - ↑⌊ξ⌋ * ↑v / ↑v)

Tactic:
mul_div_cancel_right₀ _ Hv,

Goal state after:
case h
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : (u - ⌊ξ⌋ * ↑v).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(u - ⌊ξ⌋ * ↑v).toNat
n : ℕ
hn : ↑↑v / ↑(u - ⌊ξ⌋ * ↑v).toNat = (fract ξ)⁻¹.convergent n
⊢ ↑u / ↑v = ↑⌊ξ⌋ + (↑u / ↑v - ↑⌊ξ⌋)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
have : (Int.negSucc n) + a = -(n + (1 - a)) := by { push_cast; ring }
  rw [f_int, f_nat, this, abs_neg, neg_sq, abs_of_nonneg (by linarith)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : F_nat 1 a =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ F_int 1 ↑a =O[atTop] fun t ↦ rexp (-p * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂'' (z + 1) τ = jacobiTheta₂'' z τ

Tactic:
simp only [jacobiTheta₂'', add_mul z 1, one_mul, jacobiTheta₂'_add_left', jacobiTheta₂_add_left']
  generalize jacobiTheta₂ (z * τ) τ = J
  generalize jacobiTheta₂' (z * τ) τ = J'
  -- clear denominator
  simp_rw [div_add' _ _ _ two_pi_I_ne_zero, ← mul_div_assoc]
  refine congr_arg (· / (2 * π * I)) ?_
  -- get all exponential terms to left
  rw [mul_left_comm _ (cexp _), ← mul_add, mul_assoc (cexp _), ← mul_add, ← mul_assoc (cexp _),
    ← Complex.exp_add]
  congrm (cexp ?_ * ?_) <;> ring

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

Goal state before:
pp: z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / τ = -I / -I / τ

Tactic:
div_self (neg_ne_zero.mpr I_ne_zero)

Goal state after:
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 1 / τ = 1 / τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ Function.Periodic (fun ξ ↦ (jacobiTheta₂' (↑ξ) (I * ↑x) / (-2 * ↑π)).re) 1

Tactic:
simp [jacobiTheta₂'_add_left]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * sinZeta (-a) s)) / 2

Tactic:
sinZeta_neg

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * sinZeta (-a) s)) / (2 * I)

Tactic:
sinZeta_neg

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (cosZeta a s + I * sinZeta a s - (cosZeta a s + I * -sinZeta a s)) / (2 * I)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ 1 / (-I * τ) ^ (1 / 2) * deriv (fun z ↦ cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z =
    1 / (-I * τ) ^ (1 / 2) *
      (deriv (fun z ↦ cexp (-↑π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ) +
        cexp (-↑π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z)

Tactic:
rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * ↑(Real.sin (2 * π * a * ↑n)) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))) * ↑(rexp (-π * ↑n ^ 2 * t))

Tactic:
ofReal_sin,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * Complex.sin ↑(2 * π * a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) + -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n))) * ↑(rexp (-π * ↑n ^ 2 * t))
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
h : L (fun n ↦ ↑(ζ n)) s = 0
⊢ False

Tactic:
simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

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

Goal state before:
pp: case inr
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s =
    ((s + 1).Gammaℝ * -I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)) /
        2 /
      ↑n ^ s

Tactic:
ofReal_sin,

Goal state after:
case inr
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (s + 1).Gammaℝ * Complex.sin ↑(2 * π * a * ↑n) / ↑n ^ s =
    ((s + 1).Gammaℝ * -I * 1 * cexp (2 * ↑π * I * ↑a * ↑n) + (s + 1).Gammaℝ * -I * -1 * cexp (2 * ↑π * I * ↑a * -↑n)) /
        2 /
      ↑n ^ s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = z * z * (k * k)

Tactic:
convert! h using 1

Goal state after:
case e'_2
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ (x * x + y * y) * (k * k) = k * x * (k * x) + k * y * (k * y)

case e'_3
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ z * z * (k * k) = k * z * (k * z)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaOdd (↑a) s)

Tactic:
by
  refine (hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_
  suffices ∀ b : ℝ, 0 ≤ b → SignType.sign (n + b) / (↑|n + b| : ℂ) ^ s = 1 / (n + b) ^ s by
    simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]
  intro b hb
  rw [abs_of_nonneg (by positivity), (by simp : (n : ℂ) + b = ↑(n + b))]
  rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb
  · simp [sign_pos hb]
  · rw [← hb, ofReal_zero, zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),
      div_zero, div_zero]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ IsCoprime (a * a) n

Tactic:
rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
⊢ IsCoprime (m ^ 2 + -n * n) n
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
⊢ ∑' (p : Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s)) = L (fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n)) s

Tactic:
rw [tsum_congr (fun p ↦ (hasSum_taylorSeries_neg_log' (hpow_le p)).tsum_eq.symm),
    LSeries_def₀ (by simp)]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
⊢ ∑' (b : Primes) (b_1 : ℕ), (χ ↑↑b * ↑↑b ^ (-s)) ^ (b_1 + 1) / (↑b_1 + 1) =
    ∑' (n : ℕ), χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ s
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
⊢ False

Tactic:
rw [Int.gcd_comm] at hcp

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
⊢ False
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative a = 0

Tactic:
← dvd_derivative_iff

Goal state after:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative b = 0

Tactic:
← dvd_derivative_iff

Goal state after:
case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ b ∣ derivative b
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Real.log (riemannZeta ↑s).re = ∑' (n : ℕ), Λ n / (↑n ^ s * Real.log ↑n)

Tactic:
by
  rw [← riemannZeta_eq_exp_LSeries (by simpa using hs), LSeries_def₀ (by simp)]
  convert Real.log_exp _
  convert exp_ofReal_re _
  push_cast
  congr! 2 with p
  rw [ofReal_cpow (by positivity)]
  simp [field]

Goal state after: