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

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ xn a1 n * xn a1 n * xn a1 j

Tactic:
mul_assoc

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
suffices xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n from
      (lt_or_eq_of_le (Nat.le_of_succ_le_succ ij)).elim
        (fun h => lt_trans (eq_of_xn_modEq_lem1 h (le_of_lt jn)) this) fun h => by
        rw [h]; exact this

Goal state after:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
rw [Nat.mod_eq_of_lt (strictMono_x _ (Nat.lt_of_succ_lt jn)),
        Nat.mod_eq_of_lt (strictMono_x _ jn)]

Goal state after:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case neg
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : ¬p ^ (k + 1) = 2
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
exact discr_prime_pow_ne_two hζ hirr hk

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

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * a.im * a.im ≤ 0

Tactic:
mul_assoc

Goal state after:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
h : d < 0
⊢ d * (a.im * a.im) ≤ 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)
⊢ ↑(a * b).re + ↑(a * b).im * ↑r = (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r)

Tactic:
simp only [re_mul, Int.cast_add, Int.cast_mul, im_mul, this, r.prop]

Goal state after:
R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)
⊢ ↑a.re * ↑b.re + ↑d * ↑a.im * ↑b.im + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * ↑d
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
exact Nat.pred_lt (_root_.ne_of_gt <| tsub_pos_of_lt j2n)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
⊢ (v ⊗ f v :: fun i ↦ fl i v) ∈ S ↔ (v ⊗ fun i ↦ (f :: fl) i v) ∈ S

Tactic:
congr! 3 with x

Goal state after:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
this✝ : Dioph {v | (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) ∈ S}
this : Dioph {v | (v ⊗ f v :: fun i ↦ fl i v) ∈ S}
v : α → ℕ
x : Fin2 (n + 1)
⊢ (f v :: fun i ↦ fl i v) x = (f :: fl) x v
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
mul_assoc

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(Finset.range N.succ) - 1 = N

Tactic:
simp only [Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n k : ℕ
h : n ∈ k.smoothNumbers
⊢ ∃ s ∈ k.primesBelow.powerset, ∃ m, n = m ^ 2 * s.prod id

Tactic:
by
  obtain ⟨l, m, H₁, H₂⟩ := sq_mul_squarefree n
  have hl : l ∈ smoothNumbers k := mem_smoothNumbers_of_dvd h (Dvd.intro_left (m ^ 2) H₁)
  refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩
  · simp only [toFinset_factors, Finset.mem_powerset]
    refine fun p hp ↦ mem_primesBelow.mpr ⟨?_, (mem_primeFactors.mp hp).1⟩
    rw [mem_primeFactors] at hp
    exact mem_smoothNumbers'.mp hl p hp.1 hp.2.1
  rw [← H₁]
  congr
  simp only [toFinset_factors]
  exact (prod_primeFactors_of_squarefree H₂).symm

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

Goal state before:
pp: case empty
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)‖
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
| empty =>

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| = |(fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)|

Tactic:
by
      rw [abs_sub_comm]; congr 1; field

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

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : ξ - ↑u / ↑v < (↑v * (2 * ↑v - 1))⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v

Tactic:
rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h'

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.g (1 / x) - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
P.h_feq' _ hx

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖(P.ε⁻¹ * ↑(x ^ P.k)) • P.f x - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_3.inr
ι : 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
⊢ Integrable (fun t ↦ a i * ↑t ^ (s - 1) * ↑(rexp (-p i * t))) (volume.restrict (Ioi 0))

Tactic:
mul_assoc

Goal state after:
case convert_3.inr
ι : 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
⊢ Integrable (fun t ↦ a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
rw [← Real.exp_nat_mul, ← Real.exp_add]

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t + ↑n * (-π * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
revert h

Goal state after:
case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ (Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))) → False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
| cexp (-↑π * I * (τ + 2 * z)) * ∑' (n : ℤ), jacobiTheta₂_term n z τ

Tactic:
← tsum_mul_left,

Goal state after:
z τ : ℂ
| ∑' (x : ℤ), cexp (-↑π * I * (τ + 2 * z)) * jacobiTheta₂_term x z τ
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : 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))
⊢ HasSum (fun i ↦ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s) (mellin F ((s + 1) / 2))

Tactic:
convert! hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 with i

Goal state after:
ι : 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 : ι
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)

ι : 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))
⊢ Summable fun i ↦ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
jacobiTheta₂_undef z hτ,

Goal state after:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
have h : -2 * (π : ℂ) ≠ (0 : ℂ) := by
    simp only [neg_mul, ne_eq, neg_eq_zero, mul_eq_zero,
      OfNat.ofNat_ne_zero, ofReal_eq_zero, pi_ne_zero, or_self, not_false_eq_true]

Goal state after:
a t : ℝ
ht : 0 < t
h : -2 * ↑π ≠ 0
⊢ HasSum (fun n ↦ -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: case hf
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Function.Even fun n ↦ (↑n ^ k)⁻¹

pp: case hf2
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable fun n ↦ (↑n ^ k)⁻¹

Tactic:
· intro n
    simp [Even.neg_pow hk2]

Goal state after:
case hf2
k : ℕ
hk : 2 ≤ k
hk2 : Even k
hkk : 1 < k
⊢ Summable fun n ↦ (↑n ^ k)⁻¹
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
s : ℂ
H : LSeriesSummable (fun n ↦ χ ↑n) s
h : s.re ≤ 1
⊢ False

Tactic:
exact not_LSeriesSummable_at_one hN χ <| LSeriesSummable.of_re_le_re (by simp [h]) H

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (cosZeta (↑a) s)

Tactic:
rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
  refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_
  rw [mul_div_assoc _ (cexp _), div_right_comm _ (2 : ℂ),
    mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

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

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
f : ℕ →*₀ ℂ := dirichletSummandHom χ ⋯
⊢ term (fun n ↦ χ ↑n) s 0 = f 0

Tactic:
simp only [term_zero, map_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
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
⊢ ↑2 ∣ 2 * m * n

Tactic:
mul_assoc

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 : m.gcd (r * s) = 1
⊢ ↑2 ∣ 2 * (m * n)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ z ≠ 0

Tactic:
suffices 0 < z * z by
    rintro rfl
    norm_num at this
  rw [← h.eq, ← sq, ← sq]
  have hc' : Int.gcd x y ≠ 0 := by
    rw [hc]
    exact one_ne_zero
  rcases Int.ne_zero_of_gcd hc' with hxz | hyz
  · apply lt_add_of_pos_of_le (sq_pos_of_ne_zero hxz) (sq_nonneg y)
  · apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero hyz)

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
completedHurwitzZetaOdd_one_sub,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a s * (s.Gammaℂ * Complex.sin (↑π * s / 2) * (s + 1).Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hxy : (x, y).1 ^ 2 + (x, y).2 ^ 2 = 1
hy : (x, y).2 ≠ -1
⊢ (fun x ↦ ⟨(2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)), ⋯⟩) ((fun p ↦ (↑p).1 / ((↑p).2 + 1)) ⟨(x, y), ⋯⟩) =
    ⟨(x, y), ⋯⟩

Tactic:
change x ^ 2 + y ^ 2 = 1 at hxy
    have h2 : y + 1 ≠ 0 := mt eq_neg_of_add_eq_zero_left hy
    have h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1) := by
      rw [(add_neg_eq_iff_eq_add.mpr hxy.symm).symm]
      ring
    have h4 : (2 : K) ≠ 0 := by
      convert! hk 1
      rw [one_pow 2]
      ring
    simp only [Prod.mk_inj, Subtype.mk_eq_mk]
    constructor
    · simp [field, h3]
    · grind

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case e'_4.e'_5
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = ↑a.natDegree

pp: case e'_4.e'_6
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = ↑b.natDegree

Tactic:
· exact Polynomial.degree_eq_natDegree ha

Goal state after:
case e'_4.e'_6
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = ↑b.natDegree
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : IsUnit a
⊢ primeFactors a = ∅

Tactic:
classical
  rw [primeFactors, normalizedFactors_of_isUnit h, Multiset.toFinset_zero]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : IsRadical a
⊢ (primeFactors a).val = normalizedFactors a

Tactic:
by
  classical
  rw [primeFactors, Multiset.toFinset_val, Multiset.dedup_eq_self]
  exact normalizedFactors_nodup ha

Goal state after:
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) ∣ C (↑i + 1) * p ^ i * normalize 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) ∣ C (↑i + 1) * (p ^ i * normalize p)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ radical a = normalize a

Tactic:
rw [radical, primeFactors]
  rw [normalizedFactors_irreducible ha.irreducible]
  simp only [Multiset.toFinset_singleton, id, Finset.prod_singleton]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ ∃ n, a ∣ radical a ^ n

Tactic:
rw [exists_dvd_pow_iff_radical_dvd ha]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
h : (↑∅).Pairwise (Function.onFun IsRelPrime f)
⊢ radical (∏ i ∈ ∅, f i) = ∏ i ∈ ∅, radical (f i)

Tactic:
| empty =>

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
⊢ radical (∏ i ∈ ∅, f i) ∣ ∏ i ∈ ∅, radical (f i)

Tactic:
| empty =>

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
⊢ IsCoprime (C u * a ^ p) (C v * b ^ q)

Tactic:
isCoprime_mul_units_left hu.isUnit_C hv.isUnit_C

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
⊢ IsCoprime (a ^ p) (b ^ q)
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ (algebraMap K L) ((Algebra.norm K) ↑x) = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)

Tactic:
norm_eq_prod_automorphisms

Goal state after:
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : 𝓞 L
hint : IsIntegral ℤ (∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x)
⊢ ∏ σ, σ ↑x = ↑(x * ⟨∏ σ ∈ univ.erase AlgEquiv.refl, σ ↑x, hint⟩)
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' closure (range Rat.cast)

Tactic:
DenseRange.closure_range Rat.isDenseEmbedding_coe_real.dense

Goal state after:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' univ