mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ¬p ∣ b ^ 2 - 1

Tactic:
rw [mul_comm] at not_dvd

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ (b ^ 2 - 1) * b
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
⊢ ¬p ∣ b ^ 2 - 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mp.left
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬P ∣ differentIdeal A B
⊢ Algebra.IsSeparable (A ⧸ Ideal.under A P) (B ⧸ P)

Tactic:
contrapose H

Goal state after:
case inr.mp.left
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : ¬Algebra.IsSeparable (A ⧸ Ideal.under A P) (B ⧸ P)
⊢ P ∣ differentIdeal A B
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case hgt
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) := ⋯
H : ¬P ∣ differentIdeal A B
⊢ ¬Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ (1 + 1)

Tactic:
contrapose H

Goal state after:
case hgt
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) P) ≤ P ^ (1 + 1)
⊢ P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ S.x
⊢ False

Tactic:
by
  replace h := mul_dvd_mul_left (λ ^ (3 * S.multiplicity - 2)) h
  rw [mul_comm, ← x_spec] at h
  replace h :=
    mul_dvd_mul (mul_dvd_mul h S.lambda_dvd_a_add_eta_mul_b) S.lambda_dvd_a_add_eta_sq_mul_b
  simp only [← a_cube_add_b_cube_eq_mul, S.H, w_spec, Units.isUnit, IsUnit.dvd_mul_left] at h
  rw [← pow_succ', mul_comm, ← mul_assoc, ← pow_succ'] at h
  have := S.two_le_multiplicity
  rw [show 3 * multiplicity S - 2 + 1 + 1 = 3 * multiplicity S by lia, mul_pow, ← pow_mul,
    mul_comm _ 3, mul_dvd_mul_iff_left _] at h
  · exact lambda_not_dvd_w _ <| hζ.zeta_sub_one_prime'.dvd_of_dvd_pow h
  · simp [hζ.zeta_sub_one_prime'.ne_zero]

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

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

Tactic:
by rfl

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
⊢ S.multiplicity ≠ 0

Tactic:
by have := S.two_le_multiplicity; lia

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

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
| term (n + 1) s

Tactic:
term_of_lt (by simp) hs

Goal state after:
N : ℕ
s : ℝ
hs : 1 < s
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)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
Nat.cast_add_one,

Goal state after:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s + (1 / (↑N + 1) ^ s - 1 / (↑N + 1 + 1) ^ s) * (↑N + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + 1 / (↑N + 1) ^ s - (↑N + 1) / (↑N + 1 + 1) ^ s
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1)))

Tactic:
rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]

Goal state after:
case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

pp: case hgf
s : ℝ
hs : 1 < s
⊢ (fun x ↦ 0) ≤ fun x ↦ ↑x / (↑x + 1) ^ s

pp: case hfh
s : ℝ
hs : 1 < s
⊢ (fun x ↦ ↑x / (↑x + 1) ^ s) ≤ fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
· rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
        refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
        exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)

Goal state after:
case hgf
s : ℝ
hs : 1 < s
⊢ (fun x ↦ 0) ≤ fun x ↦ ↑x / (↑x + 1) ^ s

case hfh
s : ℝ
hs : 1 < s
⊢ (fun x ↦ ↑x / (↑x + 1) ^ s) ≤ fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x - y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ y

Tactic:
rw [sub_eq_add_neg, ← logHeight₁_neg y]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x + -y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ (-y)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hl
⊢ ?f₁ =ᶠ[𝓝[>] 1] fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm

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

Goal state before:
pp: case refine_2.refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)

Tactic:
simp_rw [div_eq_mul_inv, inv_inv, sub_mul,
        (by ring_nf : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1) - f 1 * (1 - 1)))]
      apply Tendsto.sub
      · simp_rw [mul_comm (f _), f, mul_sub]
        apply riemannZeta_residue_one.sub
        refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)
        filter_upwards [self_mem_nhdsWithin] with x hx
        field [sub_ne_zero.mpr <| mem_compl_singleton_iff.mp hx]
      · exact ((tendsto_id.sub tendsto_const_nhds).mono_left nhdsWithin_le_nhds).const_mul _

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

Goal state before:
pp: ⊢ HasDerivAt (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1)))
    (-log (2 * ↑π) / 2) 0

Tactic:
have h₁ : HasDerivAt ((id * completedRiemannZeta₀ - 1) - id / (1 - id)) _ 0 :=
    .sub
      (.sub (.mul (hasDerivAt_id 0) differentiable_completedZeta₀.differentiableAt.hasDerivAt)
        (hasDerivAt_const 0 1))
      (.div (hasDerivAt_id 0) (.sub (hasDerivAt_const 0 1) (hasDerivAt_id 0)) (by simp))

Goal state after:
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
⊢ HasDerivAt (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1)))
    (-log (2 * ↑π) / 2) 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ HasDerivAt (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1)))
    (-log (2 * ↑π) / 2) 0

Tactic:
suffices h : -(log (2 * π) * 2) = γ - log (2 * 2 * π) + (-log π + -γ) by
    norm_num only at h
    convert! h₁.mul ((h₂.mul h₃).inv (by simp)) using 1
    simpa [completedRiemannZeta₀_zero, hasDerivAt_Gamma_one.deriv, field]

Goal state after:
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -(log (2 * ↑π) * 2) = ↑γ - log (2 * 2 * ↑π) + (-log ↑π + -↑γ)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (fun s ↦ deriv riemannZeta₁ s / riemannZeta₁ s - ↑γ) =O[𝓝 1] fun x ↦ x - 1
⊢ (fun s ↦ deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹ - ↑γ) =O[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
refine (this.mono nhdsWithin_le_nhds).congr' ?_ .rfl
    filter_upwards [log_deriv_riemannZeta_eq_neg_inv_sub_add]
    simp +contextual

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) =
    -1 + (-↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2

Tactic:
enter [1, 2, 2, x]; rw [(Hcs x).2]

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
x : F
| ⋯.choose * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ 0 = 1

Tactic:
by rfl

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
have hUo : IsOpen U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using! isOpen_compl_singleton
    · simp only [h, ↓reduceIte, isOpen_univ, U]

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ ∫ (x : ℝ) in 0..1, bernoulliFun k x = if k = 0 then 1 else 0

Tactic:
by
  simp +contextual [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
      (intervalIntegrable_bernoulliFun k _ _), bernoulliFun_eval_one, ← sub_div, ite_div]

Goal state after:
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
⊢ ↑((have f_surj := ⋯;
        have fsym_surj := ⋯;
        OrderIso.ofHomInv (IsDedekindDomain.idealFactorsFunOfQuotHom f_surj)
          (IsDedekindDomain.idealFactorsFunOfQuotHom fsym_surj) ⋯ ⋯)
        ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
rw [OrderIso.ofHomInv_apply]

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
⊢ ↑((IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⟨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: case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 1 n = -↑1! / (2 * ↑π * I * ↑n) ^ 1

Tactic:
bernoulliFourierCoeff_recurrence 1 hn

Goal state after:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / (-2 * ↑π * I * ↑n) * ((if 1 = 1 then 1 else 0) - ↑1 * bernoulliFourierCoeff (1 - 1) n) =
    -↑1! / (2 * ↑π * I * ↑n) ^ 1
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Tactic:
simpa [LSeriesHasSum, term_sum, Finset.sum_fn S fun i ↦ term (f i) s] using hasSum_sum hf

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
x : ZMod N
⊢ Φ (-x) * expZeta (toAddCircle (-x)) s = Φ ((Equiv.neg (ZMod N)) x) * expZeta (toAddCircle ((Equiv.neg (ZMod N)) x)) s

Tactic:
by rfl

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2 * (↑0 + 1)) = 0
⊢ B.F ↑(-2) = 0

Tactic:
rw [Nat.cast_zero, zero_add, mul_one] at this

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ B.F ↑(-2) = 0
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ LFunctionResidueClassAux a ↑x = ↑(LFunctionResidueClassAux a ↑x).re

Tactic:
by
  rw [eqOn_LFunctionResidueClassAux ha hx]
  simp only [sub_re, ofReal_sub]
  congr 1
  · rw [LSeries, re_tsum <| LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]
    push_cast
    refine tsum_congr fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp only [term_zero, zero_re, ofReal_zero]
    · simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div,
        ofReal_re]
  · rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv,
      ← ofReal_div, ofReal_re]

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

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

Tactic:
rw [if_neg (zero_lt_one.trans_le (mem_Icc.mp h).1).ne']

Goal state after:
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 ^ ((p / 2).succ - 1) * ↑(p / 2)!)

Tactic:
Nat.add_one_sub_one

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ∏ x ∈ Ico 1 (p / 2).succ, (if (↑a * ↑x).val ≤ p / 2 then 1 else -1) * ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
by
      rw [prod_mul_distrib, Finset.prod_ite]
      simp

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
H : DenselyOrdered (ValueGroupWithZero R)
⊢ False

Tactic:
obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
H : DenselyOrdered (ValueGroupWithZero R)
x : ValueGroupWithZero R
hx : x < 1
hx' : ∀ δ < 1, δ ≤ x
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ (rhs a) ↑p = J(↑a | p)

Tactic:
rhs_apply,

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ qrSign (↑p) a * J(↑↑p | a) = J(↑a | p)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = (rhs p) ↑q

Tactic:
rhs_apply,

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = qrSign (↑q) p * J(↑↑q | p)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
χ₄_nat_mod_four (b % (4 * _)),

Goal state after:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ χ₄ ↑(b % 4) * J(↑a.natAbs | b % (4 * a.natAbs)) = χ₄ ↑(b % (4 * a.natAbs) % 4) * J(↑a.natAbs | b % (4 * a.natAbs))
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x✝ : A
hx1✝ : x✝ ∈ Subring.center A
hx1 : ∀ (g : A), g * x✝ = x✝ * g
hx2 : x✝ ≠ 0
x : A
⊢ -(fun x ↦ x✝ * x) x ∈ Set.range fun x ↦ x✝ * x

Tactic:
exact ⟨-x, by simp⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 3 = ↑3

Tactic:
by rfl

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ 0 ≤ sMod p i

Tactic:
cases i <;> dsimp [sMod]
  · exact sup_eq_right.mp rfl
  · apply Int.emod_nonneg
    exact mersenne_int_ne_zero p hp

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
hH : DiscreteTopology ↥H
this : IsOpen[inst✝³] ↑H
⊢ DiscreteTopology G

Tactic:
rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : h ∈ g • Γ
⊢ GeneralLinearGroup.det h = 1

Tactic:
rw [mem_pointwise_smul_iff_inv_smul_mem] at hh
    simpa [ConjAct.smul_def] using HasDetOne.det_eq hh

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ IsCusp c 𝒢 ↔ IsCusp c 𝒢'

Tactic:
rw [← isCusp_iff_of_relIndex_ne_zero inf_le_left, isCusp_iff_of_relIndex_ne_zero inf_le_right]

Goal state after:
case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0