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

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
replace H := (mul_left_inj' fun h => ?_).1 H

Goal state after:
case e_a.refine_2
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
H : (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * (k.succ * (p - 1)).pred)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

case e_a.refine_1
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
⊢ False
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d : ℕ
x y : ℤ
⊢ Nonnegg c d x y = Nonnegg d c y x

Tactic:
cases x

Goal state after:
case ofNat
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.ofNat a✝) y = Nonnegg d c y (Int.ofNat a✝)

case negSucc
c d : ℕ
y : ℤ
a✝ : ℕ
⊢ Nonnegg c d (Int.negSucc a✝) y = Nonnegg d c y (Int.negSucc a✝)
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by decide

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

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 → z = 0

Tactic:
intro h

Goal state after:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a✝ : ℕ
xy : { re := -[a✝+1], im := 0 }.Nonneg
x✝ : (-{ re := -[a✝+1], im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
by decide

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
n✝ : ℕ
x✝ : { re := ↑(n✝ + 1), im := 0 }.Nonneg
yx : (-{ re := ↑(n✝ + 1), im := 0 }).Nonneg
⊢ 0 < 1

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : 2 + 1 ≤ 2 * 1
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
jn : j ≠ n
s : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i < j
x✝ : a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : i = 0
j2 : j = 2
⊢ ¬2 + 1 ≤ 2 * 1

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : 2 < 1
x✝ : a = 2 ∧ n = 1 ∧ 0 = 0 ∧ i + 1 = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : 0 = 0
i2 : i + 1 = 2
⊢ ¬2 < 1

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ ¬2 ≤ 1

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by decide

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case e_a
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x

Tactic:
cases x

Goal state after:
case e_a.fz
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) fz = (f v :: v) fz

case e_a.fs
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
a✝ : Fin2 n
⊢ ((f v ::ₒ v) ∘ none :: some) a✝.fs = (f v :: v) a✝.fs
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ ∑ χ, χ a = 0

Tactic:
refine eq_zero_of_mul_eq_self_left hχ ?_

Goal state after:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
χ : DirichletCharacter R n
hχ : χ a ≠ 1
⊢ χ a * ∑ χ, χ a = ∑ χ, χ a
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : ¬a = 1
⊢ ∑ χ, χ a = 0

Tactic:
· exact sum_characters_eq_zero R ha

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
⊢ m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
by
  obtain ⟨p, hp₁, hp₂⟩ := exists_infinite_primes (1 + Finset.sup s id)
  rw [mem_factoredNumbers_iff_forall_le]
  refine ⟨fun ⟨H₀, H₁⟩ ↦ fun p hp₁ hp₂ ↦ H₁ p (le_of_dvd (Nat.pos_of_ne_zero H₀) hp₂) hp₁ hp₂,
         fun H ↦ ⟨fun h ↦ lt_irrefl p ?_, fun p _ ↦ H p⟩⟩
  calc
    p ≤ s.sup id := Finset.le_sup (f := @id ℕ) <| H p hp₂ <| h.symm ▸ dvd_zero p
    _ < 1 + s.sup id := lt_one_add _
    _ ≤ p := hp₁

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
n : ℕ
⊢ (List.filter (fun x ↦ decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

Tactic:
have h₀ : (n.primeFactorsList.filter (· ∈ s)).prod ≠ 0 :=
    List.prod_ne_zero fun h ↦ (pos_of_mem_primeFactorsList (List.mem_of_mem_filter h)).false
  refine ⟨h₀, fun p hp ↦ ?_⟩
  obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp
  simpa only [decide_eq_true_eq] using List.of_mem_filter <| mem_list_primes_of_dvd_prod H₁.prime
    (fun _ hq ↦ (prime_of_mem_primeFactorsList (List.mem_of_mem_filter hq)).prime) H₂

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q < p.succ

Tactic:
rw [mem_primeFactorsList hp'] at H
    exact Nat.lt_succ_of_le <| le_of_dvd hp.bot_lt <| H.1.dvd_of_dvd_pow H.2

Goal state after:
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

Tactic:
refine (mul_nonneg_iff_of_pos_right hv₁).mp ?_

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) * (2 * v - 1)
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ≠ 0

Tactic:
have := hm ▸ ne_zero_of_mem_smoothNumbers hn₂

Goal state after:
case refine_1
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
this : m ^ 2 * s.prod id ≠ 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
⊢ 2 < 4

Tactic:
by decide

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

Goal state before:
pp: case refine_1
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ IsCoprime q.num ↑q.den

pp: case refine_2
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num

pp: case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹

Tactic:
· exact isCoprime_iff_nat_coprime.mpr (natAbs_natCast q.den ▸ q.reduced)

Goal state after:
case refine_2
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num

case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mp
z τ : ℂ
⊢ (Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ) → Summable fun x ↦ jacobiTheta₂_term x z τ

Tactic:
intro h

Goal state after:
case mp
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
⊢ Summable fun x ↦ jacobiTheta₂_term x z τ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
hu_sum : Summable u
hf_sum : Summable fun n ↦ f n (z, τ)
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
simpa only [jacobiTheta₂, jacobiTheta₂_fderiv, f, f'] using!
    hasFDerivAt_tsum_of_isPreconnected hu_sum hVo hVp hf hu hVmem hf_sum hVmem

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

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

Tactic:
by
  obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
  obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1
  obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_one (sub_nonneg.mpr ha.2.le)
  refine ⟨_, lt_min hp hq, ?_⟩
  have : F_int 1 a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t := by
    filter_upwards [eventually_gt_atTop 0] with t ht
    exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht
  refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;>
  apply isBigO_exp_neg_mul_of_le
  exacts [min_le_left .., min_le_right ..]

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

Tactic:
1

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 : ι
h : r i ≠ 0
| (s + 1).Gammaℝ * (a i * ↑(r i))
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : 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 (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / (↑|r i| ^ s * ↑|r i|)

Tactic:
conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]

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

Goal state before:
pp: ⊢ ¬Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)

Tactic:
intro h

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
⊢ False
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (fun n ↦ ↑(Λ n)) s

Tactic:
by
  have hf := LSeriesSummable_logMul_of_lt_re
    (show abscissaOfAbsConv 1 < s.re by rw [abscissaOfAbsConv_one]; exact_mod_cast hs)
  rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
  refine hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)
  have hΛ : ‖↗Λ n‖ ≤ ‖Complex.log n‖ := by
    simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg]
      using vonMangoldt_le_log
  exact hΛ.trans <| by simp

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
have hχ : LSeriesSummable ↗χ s := (LSeriesSummable_iff hN χ).mpr hs

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ((changeLevel hMN) χ) ↑n) s = L (fun n ↦ χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
prod_eq_tprod_mulIndicator,

Goal state after:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ((changeLevel hMN) χ) ↑n) s =
    L (fun n ↦ χ ↑n) s * ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) x
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ ∏' (p : Primes), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) x

Tactic:
have (f : Primes → ℂ) : ∏' (p : Primes), f p = ∏' (p : ↑{p : ℕ | p.Prime}), f p := rfl

Goal state after:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (p : Primes), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) x
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
intro h

Goal state after:
x y z k : ℤ
hk : k ≠ 0
h : k * x * (k * x) + k * y * (k * y) = k * z * (k * z)
⊢ x * x + y * y = z * z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 1 < 2

Tactic:
by decide

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
⊢ a % 2 * (a % 2) % 2 = 1

Tactic:
ha2

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
⊢ 1 * 1 % 2 = 1
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

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

Tactic:
by
      refine tsum_congr fun p ↦ tsum_congr fun k ↦ ?_
      have : Complex.log p ≠ 0 := mod_cast p.prop.log_ne_zero
      simp [mul_pow, ← cpow_nat_mul, ← natCast_cpow_natCast_mul, vonMangoldt_apply_pow,
        vonMangoldt_apply_prime p.2, field]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
change Nat.gcd 0 (Int.natAbs y) = 1 at hc

Goal state after:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
n : ℕ
⊢ -2 * ↑n - 1 + 1 = -(2 * ↑n)

Tactic:
by rw [neg_mul, sub_add_cancel]

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

Goal state before:

Tactic:
(wronskian a b).degree ≤ max (a * derivative b).degree (derivative a * b).degree :=
      Polynomial.degree_sub_le _ _
    _ < a.degree + b.degree := by
      rw [max_lt_iff]
      constructor
      case left =>
        apply lt_of_le_of_lt
        · exact degree_mul_le a (derivative b)
        · rw [← Polynomial.degree_ne_bot] at ha
          rw [WithBot.add_lt_add_iff_left ha]
          exact Polynomial.degree_derivative_lt hb
      case right =>
        apply lt_of_le_of_lt
        · exact degree_mul_le (derivative a) b
        · rw [← Polynomial.degree_ne_bot] at hb
          rw [WithBot.add_lt_add_iff_right hb]
          exact Polynomial.degree_derivative_lt ha

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
⊢ a ≠ 0

Tactic:
intro h

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
h : a = 0
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : n ∉ {n | IsPrimePow n}
⊢ n ∉ Function.support f

Tactic:
simp [f, vonMangoldt_eq_zero_iff.mpr hn]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
⊢ b ≠ 0

Tactic:
intro h

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
h : b = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Wronskian

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

Tactic:
hdb

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hda : derivative a = 0
hdb : derivative b = 0
⊢ a * 0 - 0 * b = 0
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 * p ∣ p ^ i * normalize p

Tactic:
mul_dvd_mul_iff_left (pow_ne_zero i hp.ne_zero),

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ∣ normalize p
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: case a
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := ⋯
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := ⋯
⊢ ?n + c.natDegree < ?n + abc_r.natDegree

pp: case n
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := ⋯
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := ⋯
⊢ ℕ

Tactic:
calc
    a.natDegree + b.natDegree + c.natDegree = (a * b * c).natDegree := by
      rw [Polynomial.natDegree_mul ab_nz hc, Polynomial.natDegree_mul ha hb]
    _ = ((divRadical (a * b * c)) * (radical (a * b * c))).natDegree := by
      rw [mul_comm _ (radical _), radical_mul_divRadical]
    _ = abc_dr.natDegree + abc_r.natDegree := by
      rw [← Polynomial.natDegree_mul (divRadical_ne_zero abc_nz) radical_ne_zero]
    _ < a.natDegree + b.natDegree + abc_r.natDegree := by
      exact Nat.add_lt_add_right abc_dr_ndeg_lt _

Goal state after: