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

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2 * √x) =o[atTop] fun x ↦ x

pp: ⊢ ∀ᶠ (x : ℝ) in atTop, log x ^ 2 ≠ 0

Tactic:
· conv => arg 2; ext; rw [mul_comm]
    apply isLittleO_mul_iff_isLittleO_div _ |>.mpr
    · simp_rw [div_sqrt, sqrt_eq_rpow, ← rpow_two]
      apply isLittleO_log_rpow_rpow_atTop _ (by norm_num)
    filter_upwards [eventually_gt_atTop 0] with x hx using sqrt_ne_zero'.mpr hx

Goal state after:
⊢ ∀ᶠ (x : ℝ) in atTop, log x ^ 2 ≠ 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ c

Tactic:
rw [unitCoeff_spec hc']

Goal state after:
case neg.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ c.valuation
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ x, ∏ x > x, -1 = (-1) ^ (n * (n - 1) / 2)

Tactic:
simp only [prod_pow_eq_pow_sum, prod_const]

Goal state after:
case e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (-1) ^ ∑ i, #(Ioi i) = (-1) ^ (n * (n - 1) / 2)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∑ i, #(Ioi i) = n * (n - 1) / 2

Tactic:
← @Nat.cast_inj ℚ,

Goal state after:
case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ↑(∑ i, #(Ioi i)) = ↑(n * (n - 1) / 2)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ ↑(π ⌊x⌋₊)

Tactic:
grw [div_le_iff₀ (log_pos hx), ← psi_le_primeCounting_mul_log', psi_ge']
  positivity

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, log √x ≤ ∑ p ∈ ⌊x⌋₊.primesLE, (log ↑p + if ↑p ≤ √x then log √x else 0)

Tactic:
refine sum_le_sum fun p _ ↦ ?_

Goal state after:
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
⊢ log √x ≤ log ↑p + if ↑p ≤ √x then log √x else 0
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ cyclotomicCharacter.toFun p 1 = 1

Tactic:
by
      by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
      · have _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
        refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
        simp [cyclotomicCharacter.toZModPow_toFun]
      · simp [cyclotomicCharacter.toFun, dif_neg H]

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
by
      by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
      · have _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
        refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
        simp [cyclotomicCharacter.toZModPow_toFun]
      · simp [cyclotomicCharacter.toFun, dif_neg H]

Goal state after:
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 : ι'
⊢ IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)

Tactic:
convert! h' i ((b.indexEquiv b').symm j)

Goal state after:
ι : 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)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ discr K ⇑B.basis • z ∈ R[B.gen]

Tactic:
have hinv : IsUnit (traceMatrix K B.basis).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ B.basis

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
⊢ discr K ⇑B.basis • z ∈ R[B.gen]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ b.re = c.re ∧ b.im = c.im

Tactic:
apply And.imp _ _ h

Goal state after:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).re = (↑a * c).re → b.re = c.re

d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).im = (↑a * c).im → b.im = c.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a : ℤ√d
⊢ a.re.gcd a.im = 0 ↔ a = 0

Tactic:
simp only [Int.gcd_eq_zero_iff, Zsqrtd.ext_iff, im_zero, re_zero]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % 0 > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False

Tactic:
Nat.mod_zero

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
e : m = 0
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ xz a1 (n + 2) + xz a1 n = ↑(2 * a) * xz a1 (n + 1)

Tactic:
by delta xz; rw [← Int.natCast_add, ← Int.natCast_mul, xn_succ_succ]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
let t := xn_modEq_x4n_sub a1 j42n
        rwa [tsub_tsub_cancel_of_le j4n] at t

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
⊢ p ∈ s

Tactic:
obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp

Goal state after:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
H₂ : p ∣ (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod
⊢ p ∈ s
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
⊢ DiophFn fun v ↦ f v ^ g v

Tactic:
by
  have : Dioph {v : Vector3 ℕ 3 |
    v &2 = 0 ∧ v &0 = 1 ∨ 0 < v &2 ∧
    (v &1 = 0 ∧ v &0 = 0 ∨ 0 < v &1 ∧
    ∃ w a t z x y : ℕ,
      (∃ a1 : 1 < a, xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
      x ≡ y * (a - v &1) + v &0 [MOD t] ∧
      2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧
      a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)} :=
  (D&2 D= D.0 D∧ D&0 D= D.1) D∨ (D.0 D< D&2 D∧
    ((D&1 D= D.0 D∧ D&0 D= D.0) D∨ (D.0 D< D&1 D∧
    ((D∃) 3 <| (D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    pell_dioph.reindex_dioph (Fin2 9) [&4, &8, &1, &0] D∧
    (D≡ (D&1) (D&0 D* (D&4 D- D&7) D+ D&6) (D&3)) D∧
    D.2 D* D&4 D* D&7 D= D&3 D+ (D&7 D* D&7 D+ D.1) D∧
    D&6 D< D&3 D∧ D&7 D≤ D&5 D∧ D&8 D≤ D&5 D∧
    D&4 D* D&4 D- ((D&5 D+ D.1) D* (D&5 D+ D.1) D- D.1) D* (D&5 D* D&2) D* (D&5 D* D&2) D= D.1))) :)
  exact diophFn_comp2 df dg <| (diophFn_vec _).2 <| Dioph.ext this fun v => Iff.symm <|
    eq_pow_of_pell.trans <| or_congr Iff.rfl <| and_congr Iff.rfl <| or_congr Iff.rfl <|
       and_congr Iff.rfl <|
        ⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
        fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩

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

Goal state before:
pp: case insert
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ insert p s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
| insert p s hp ih =>

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ -(2 * S * ↑|n|) ≤ 2 * ↑n * z.im

Tactic:
rw [← mul_neg, mul_assoc, mul_assoc, mul_le_mul_iff_right₀ two_pos, mul_comm, neg_mul, ← mul_neg]

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ↑|n| * -S ≤ ↑n * z.im
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) ↔ 0 < τ.im

Tactic:
by
  constructor
  · rw [← summable_jacobiTheta₂_term_iff (z := z)]
    intro h
    have := h.norm
    refine this.of_norm_bounded_eventually ?_
    have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
    filter_upwards [this] with n hn
    refine le_trans ?_ (norm_jacobiTheta₂_term_fderiv_ge n z τ)
    apply le_mul_of_one_le_left (norm_nonneg _)
    refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)
    refine (by norm_num : 2⁻¹ ≤ (1 : ℝ)).trans ?_
    rw [one_le_sq_iff_one_le_abs, ← Int.cast_abs, abs_abs, ← Int.cast_one, Int.cast_le]
    exact Int.one_le_abs hn
  · intro hτ
    refine ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 2).mul_left (3 * π)).of_norm_bounded (fun n ↦ ?_)
    refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)
    simp_rw [mul_assoc (3 * π)]
    refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by simp : 0 < (3 : ℝ)) pi_pos).le
    refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)
    exact norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ EqOn (fun x ↦ P.f_modif x - P.f x + P.f₀)
    (((Ioo 0 1).indicator fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x ↦ P.f₀ - P.f 1) (Ioi 0)

Tactic:
by
  intro x (hx : 0 < x)
  simp_rw [f_modif, Pi.add_apply]
  rcases lt_trichotomy x 1 with hx' | rfl | hx'
  · simp_rw [indicator_of_notMem (notMem_Ioi.mpr hx'.le), indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne)]
    abel
  · simp [add_comm, sub_eq_add_neg]
  · simp_rw [indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem (notMem_Ioo_of_ge hx'.le),
      indicator_of_notMem (mem_singleton_iff.not.mpr hx'.ne')]
    abel

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

Goal state before:
pp: z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂'_term x z τ) ↔ 0 < τ.im

Tactic:
constructor
  · rw [← summable_jacobiTheta₂_term_iff (z := z)]
    refine fun h ↦ (h.norm.mul_left (2 * π)⁻¹).of_norm_bounded_eventually ?_
    have : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0 :=
      Int.cofinite_eq ▸ (mem_sup.mpr ⟨eventually_ne_atBot 0, eventually_ne_atTop 0⟩)
    filter_upwards [this] with n hn
    rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]
    refine le_mul_of_one_le_left (norm_nonneg _) ?_
    simp_rw [norm_mul, norm_I, norm_real, mul_one, norm_of_nonneg pi_pos.le,
      ← ofReal_ofNat, norm_real, norm_of_nonneg two_pos.le, ← ofReal_intCast, norm_real,
      Real.norm_eq_abs, ← Int.cast_abs, ← mul_assoc _ (2 * π),
      inv_mul_cancel₀ (mul_pos two_pos pi_pos).ne', one_mul]
    rw [← Int.cast_one, Int.cast_le]
    exact Int.one_le_abs hn
  · refine fun hτ ↦ ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 1).mul_left (2 * π)).of_norm_bounded (fun n ↦ ?_)
    rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc, pow_one]
    refine mul_le_mul (le_of_eq ?_) (norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n)
      (norm_nonneg _) (by positivity)
    simp_rw [norm_mul, Complex.norm_two, norm_I, Complex.norm_of_nonneg pi_pos.le,
      norm_intCast, mul_one, Int.cast_abs]

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

Goal state before:
pp: case ofNat
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ f_int k a t (Int.ofNat a✝) = Int.rec (f_nat k a t) (f_nat k (1 - a) t) (Int.ofNat a✝)

Tactic:
rw [f_int_ofNat _ ha.1]

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

Goal state before:
pp: case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ ↑(evenKernel (↑a') x)) (Ioi 0)

Tactic:
simp only [evenKernel_def]

Goal state after:
case H
a' : ℝ
⊢ ContinuousOn (fun x ↦ cexp (-↑π * ↑a' ^ 2 * ↑x) * jacobiTheta₂ (↑a' * I * ↑x) (I * ↑x)) (Ioi 0)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
⊢ P.Λ = mellin P.f

Tactic:
ext s

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
⊢ P.Λ s = mellin P.f s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign 0) / ↑0 ^ s = (s + 1).Gammaℝ * (a i * ↑0) / ↑0 ^ (s + 1)

Tactic:
ofReal_zero,

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign 0) / 0 ^ s = (s + 1).Gammaℝ * (a i * 0) / 0 ^ (s + 1)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ ‖a i * ↑0‖ / 0 ^ (s + 1).re = ‖a i‖ / 0 ^ s.re

Tactic:
ofReal_zero,

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ ‖a i * 0‖ / 0 ^ (s + 1).re = ‖a i‖ / 0 ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case H
b : ℝ
⊢ ∃ p, 0 < p ∧ (fun x ↦ evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub b

Goal state after:
case H
b p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_int 0 (↑b) t - if ↑b = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
⊢ ∃ p, 0 < p ∧ (fun x ↦ evenKernel (↑b) x - if ↑b = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-p * x)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: ⊢ ¬LSeriesSummable (fun n ↦ ↑(μ n)) 1

Tactic:
refine fun h ↦ not_summable_one_div_on_primes <| summable_ofReal.mp <| .of_neg ?_
  refine (h.indicator {n | n.Prime}).congr fun n ↦ ?_
  by_cases hn : n.Prime
  · simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]
  · simp [hn]

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

Goal state before:
pp: ⊢ (L fun n ↦ ↑(ζ n)) = L 1

Tactic:
ext s

Goal state after:
s : ℂ
⊢ L (fun n ↦ ↑(ζ n)) s = L 1 s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ↑n + a = 0
⊢ 0 = ↑0 / 2

Tactic:
ofReal_zero,

Goal state after:
case pos
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ↑n + a = 0
⊢ 0 = 0 / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ s.Gammaℝ / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaEven (↑a) s)

Tactic:
by
  have hF (t : ℝ) (ht : 0 < t) : HasSum (fun n : ℤ ↦ if n + a = 0 then 0
      else (1 / 2 : ℂ) * rexp (-π * (n + a) ^ 2 * t))
      ((evenKernel a t - (if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) := by
    refine (ofReal_sub .. ▸ (hasSum_ofReal.mpr (hasSum_int_evenKernel₀ a ht)).div_const
      2).congr_fun fun n ↦ ?_
    split_ifs
    · rw [ofReal_zero, zero_div]
    · rw [mul_comm, mul_one_div]
  rw [show completedHurwitzZetaEven a s = mellin (fun t ↦ ((evenKernel (↑a) t : ℂ) -
        ↑(if (a : UnitAddCircle) = 0 then 1 else 0 : ℝ)) / 2) (s / 2) by
    simp_rw [mellin_div_const, apply_ite ofReal, ofReal_one, ofReal_zero]
    refine congr_arg (· / 2) ((hurwitzEvenFEPair a).hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]]
  refine (hasSum_mellin_pi_mul_sq (zero_lt_one.trans hs) hF ?_).congr_fun fun n ↦ ?_
  · simp_rw [← mul_one_div ‖_‖]
    apply Summable.mul_left
    rwa [summable_one_div_int_add_rpow]
  · rw [mul_one_div, div_right_comm]

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

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) 1

Tactic:
apply this.congr_of_eventuallyEq

Goal state after:
a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
⊢ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) =ᶠ[𝓝 1] fun s ↦
    completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_dirichletSummand χ hs

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

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ Associated ({A, B, C}.gcd fun x ↦ d * id x) d

Tactic:
gcd_eq_gcd_image

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ Associated ((image (fun x ↦ d * id x) {A, B, C}).gcd id) d
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
⊢ a.gcd b = 1

Tactic:
by_contra hab

Goal state after:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case right
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ 0 < -c0

Tactic:
exact neg_pos.mpr h1

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

Goal state before:
pp: case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign 0) / ↑0 ^ s = 1 / ↑0 ^ s

Tactic:
ofReal_zero,

Goal state after:
case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign 0) / 0 ^ s = 1 / 0 ^ s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
rcases Int.ne_zero_of_gcd hc' with hxz | hyz

Goal state after:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hxz : x ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hyz : y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
⊢ (↑(primeFactors a)).Pairwise IsRelPrime

Tactic:
intro x hx y hy hxy

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x : M
hx : x ∈ ↑(primeFactors a)
y : M
hy : y ∈ ↑(primeFactors a)
hxy : x ≠ y
⊢ IsRelPrime x y