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

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ x.appr (n + 1) < p ^ (n + 1)

Tactic:
simp only [appr, map_natCast, ZMod.natCast_self, map_pow, Int.natAbs, map_mul]

Goal state after:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ (if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (toZMod ↑(unitCoeff hy) *
              0 ^
                match ↑(x - ↑(x.appr n)).valuation - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ).val) <
    p ^ (n + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, log ↑n * a n = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
rw [sum_mul_eq_sub_integral_mul₁ a (by simp [a, not_prime_zero])
    (by simp [a, not_prime_one]) _ (fun z ⟨hz, _⟩ ↦ (by fun_prop (disch := linarith))) ?hint,
    ← intervalIntegral.integral_of_le hx]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

case hint
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ IntegrableOn (deriv log) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by
  obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A
  exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

pp: case refine_2
⊢ (fun x ↦ √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
· simp_rw [mul_div_assoc]
    apply isBigO_const_mul_self

Goal state after:
case refine_2
⊢ (fun x ↦ √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2
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
⊢ False

Tactic:
have y0l : (0 : ℤ√d a1) < ⟨x - x, y - -y⟩ :=
          sub_lt_sub h1l fun hn : (1 : ℤ√d a1) ≤ ⟨x, -y⟩ => by
            have t := mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)
            rw [bm, mul_one] at t
            exact h1l 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
y0l : 0 < { re := x - x, im := y - -y }
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 m * pellZd a1 n * { re := ↑a, im := 1 } = pellZd a1 m * (pellZd a1 n * { re := ↑a, im := 1 })

Tactic:
← mul_assoc

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 m * pellZd a1 n * { re := ↑a, im := 1 } = pellZd a1 m * pellZd a1 n * { re := ↑a, im := 1 }
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * (y.natAbs * y.natAbs))
⊢ x = 0 ∧ y = 0

Tactic:
← mul_assoc

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)
⊢ x = 0 ∧ y = 0
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
⊢ ‖χ a‖ ≤ 1

Tactic:
by_cases h : IsUnit a

Goal state after:
case pos
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : IsUnit a
⊢ ‖χ a‖ ≤ 1

case neg
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
h : ¬IsUnit a
⊢ ‖χ a‖ ≤ 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∃ m ∈ D, f m = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

pp: case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
· obtain ⟨m, hm, hf⟩ := H
    have hf' : ((n : ℤ) : ℝ) ≤ fract (ξ * m) * (n + 1) := hf ▸ floor_le (fract (ξ * m) * (n + 1))
    have hm₀ : 0 < m := by
      have hf₀ : f 0 = 0 := by
        simp only [f, cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
      refine Ne.lt_of_le (fun h => n_pos.ne ?_) (mem_Icc.mp hm).1
      exact mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)
    refine ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, ?_⟩
    rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]
    refine
      ⟨le_sub_iff_add_le.mpr ?_, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩
    simpa only [neg_add_cancel_comm_assoc] using! hf'

Goal state after:
case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ xn a1 (n + 2) + xn a1 n ≡ xn b1 (n + 2) + xn b1 n [MOD c]

Tactic:
rw [xn_succ_succ a1, xn_succ_succ b1]
        exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).left

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Tactic:
exact (h.mul_left _).mul (xy_modEq_of_modEq _ _ h (n + 1)).right

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ k ≤ yn a1 k ∧
    (xn a1 k = 1 ∧ yn a1 k = 0 ∨
      ∃ u v s t b,
        xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 k] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
rw [k0]

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ u v s t b,
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ x % y = z

Tactic:
← hc

Goal state after:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(N.smoothNumbersUpTo k) + #(N.roughNumbersUpTo k) = N

Tactic:
rw [smoothNumbersUpTo, roughNumbersUpTo,
    ← Finset.card_union_of_disjoint <| Finset.disjoint_filter.mpr fun n _ hn₂ h ↦ h.2 hn₂,
    Finset.filter_union_right]
  suffices #{x ∈ Finset.range (N + 1) | x ≠ 0} = N by
    have hn' (n) : n ∈ smoothNumbers k ∨ n ≠ 0 ∧ n ∉ smoothNumbers k ↔ n ≠ 0 := by
      have : n ∈ smoothNumbers k → n ≠ 0 := ne_zero_of_mem_smoothNumbers
      refine ⟨fun H ↦ Or.elim H this fun H ↦ H.1, fun H ↦ ?_⟩
      simp only [ne_eq, H, not_false_eq_true, true_and, or_not]
    rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]
  rw [Finset.filter_ne', Finset.card_erase_of_mem <| Finset.mem_range_succ_iff.mpr <| zero_le N]
  simp only [Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

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 ∈ if Nat.Prime p then insert p ({p ∈ s | Nat.Prime p}) else {p ∈ s | Nat.Prime p}, ∑' (n : ℕ), f (p ^ n))

Tactic:
split_ifs with hpp

Goal state after:
case pos
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))
hpp : Nat.Prime p
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

case neg
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))
hpp : ¬Nat.Prime p
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ x ∈ s with Nat.Prime x, ∑' (n : ℕ), f (x ^ n))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
exact mod_cast this.trans h

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

Goal state before:
pp: 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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ Filter.Tendsto (fun s ↦ ∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) (SummationFilter.unconditional ℕ).filter
    (𝓝 (∑' (n : ℕ), f n))

Tactic:
SummationFilter.unconditional,

Goal state after:
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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
⊢ Filter.Tendsto (fun s ↦ ∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) { filter := Filter.atTop }.filter
    (𝓝 (∑'[{ filter := Filter.atTop }] (n : ℕ), f n))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (fun x ↦ rexp (-(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ 2 * (π * (↑x * z.im))) atTop atBot

Tactic:
apply Filter.Tendsto.const_mul_atBot two_pos

Goal state after:
case refine_2.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im < 0
h : Tendsto (fun x ↦ rexp (-(2 * π * ↑x * z.im))) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ π * (↑x * z.im)) atTop atBot
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case neg
a : ℝ
ha : 0 ≤ a
h : ¬a = 0
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
· simp_rw [sub_zero]
    have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_le ha ht
    refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
    simpa only [neg_mul π (a ^ 2), mul_one] using! (isBigO_refl _ _).mul isBigO_one_aux

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

Goal state before:
pp: case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-(p i * t)) = (1 / p i) ^ s.re * Real.Gamma s.re
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re

Tactic:
simp_rw [← neg_mul (p i), one_div, inv_rpow hpi.le, ← div_eq_inv_mul] at this

Goal state after:
case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * (‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖)

Tactic:
← mul_assoc

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a.e_a.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-(1 / τ)) - jacobiTheta₂' (z / τ) (-(1 / τ)) =
    2 * ↑π * I * (z * jacobiTheta₂ (z / τ) (-(1 / τ))) - jacobiTheta₂' (z / τ) (-(1 / τ))

Tactic:
← mul_assoc

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
⊢ ↑x ^ (3 / 2) ≠ 0

Tactic:
simp only [Ne, cpow_eq_zero_iff, ofReal_eq_zero, hx.ne', false_and, not_false_eq_true]

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0) =O[atTop] fun x ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_evenKernel_sub a
    rw [← isBigO_norm_left] at hv' ⊢
    conv at hv' =>
      enter [2, x]; rw [← norm_real, ofReal_sub, apply_ite ((↑) : ℝ → ℂ), ofReal_one, ofReal_zero]
    exact hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑n ^ 2 * ↑t)) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Tactic:
← mul_assoc

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
n : ℤ
⊢ -2 * ↑π * (-I * ↑n) * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑n ^ 2 * ↑t) =
    2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (hurwitzOddFEPair a).ε • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2

Tactic:
hurwitzOddFEPair_ε,

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ 1 • (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2 = (hurwitzOddFEPair a).symm.Λ ((s + 1) / 2) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
simp_rw [Int.sign_zero, Int.cast_zero, mul_zero, zero_mul, zero_div, add_zero, abs_neg,
    Int.sign_neg, Nat.abs_cast, Int.cast_neg, Int.cast_natCast, ← add_div] at this

Goal state after:
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)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ ∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = L (fun n ↦ χ ↑n) s

Tactic:
simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
    LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple y x z

Tactic:
pythagoreanTriple_comm

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
⊢ PythagoreanTriple x y z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ 1

Tactic:
← hc

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ x.gcd y
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 : IsRadical a
ha₀ : a ≠ 0
⊢ Squarefree a

Tactic:
← isRadical_iff_squarefree_of_ne_zero ha₀

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
ha₀ : a ≠ 0
⊢ IsRadical a
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * (C (↑i + 1) * p ^ i * derivative p)

Tactic:
← mul_assoc

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * (C (↑i + 1) * p ^ i) * derivative p
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b - derivative a * b

Tactic:
apply dvd_sub

Goal state after:
case h₁
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ a * derivative b

case h₂
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical a ∣ derivative a * b
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : -(a + b) = c
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b c

Tactic:
← hsum,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : -(a + b) = c
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ IsCoprime b (-(a + b))
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case hb
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ normalizedFactors a
⊢ a ≠ 0

Tactic:
rintro rfl
      simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h
x y z : ℤ
h : PythagoreanTriple x y z ∧ x.gcd y = 1
m n : ℤ
H :
  (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
rcases H with ⟨⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, co, pp⟩

Goal state after:
case h.inl
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2 ∧ 2 * m * n = 2 * m * n ∨ m ^ 2 - n ^ 2 = 2 * m * n ∧ 2 * m * n = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n = m ^ 2 - n ^ 2 ∧ m ^ 2 - n ^ 2 = 2 * m * n ∨ 2 * m * n = 2 * m * n ∧ m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inl
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2) ∧
    (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
constructor; ring; exact coprime_sq_sub_mul co pp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inr
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) + 2 * m * n * (2 * m * n) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2) ∧
    (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
constructor; ring; exact coprime_sq_sub_mul co pp

Goal state after: