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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b') * (Algebra.norm R) (r • a - q * b)) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)

Tactic:
← map_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b' * (r • a - q * b))) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b' * (r • a - q * b))) =
    abv ((Algebra.norm R) (r • a' - b' • q) * (Algebra.norm R) b)

Tactic:
← map_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b' * (r • a - q * b))) = abv ((Algebra.norm R) ((r • a' - b' • q) * b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑b ∈ Ideal.span {↑(p ^ n)} → ↑a = ↑b

Tactic:
hb

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ ↑a = ↑b
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ↑p ≤ √x
⊢ log √x ≤ log ↑p + log √x

pp: case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
⊢ log √x ≤ log ↑p + 0

Tactic:
· simp [log_natCast_nonneg]

Goal state after:
case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
⊢ log √x ≤ log ↑p + 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 < x
this : 0 < log √x
⊢ ↑(π ⌊x⌋₊) * log √x ≤ log 4 * x + log √x * √x

Tactic:
grind [pi_mul_log_sqrt_le hx.le]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ ((f j) r * (f j) s).cast - ((f j) r).cast * ((f j) s).cast = 0

Tactic:
rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]

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)
⊢ discr ℚ ⇑b = discr ℚ ⇑b'

Tactic:
replace h' : ∀ i j, IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b')) i j) := by
    intro i j
    convert! h' i ((b.indexEquiv b').symm j)
    simp [Basis.toMatrix_apply]
  rw [← (b.reindex (b.indexEquiv b')).toMatrix_map_vecMul b', discr_of_matrix_vecMul,
    ← one_mul (discr ℚ b), Basis.coe_reindex, discr_reindex]
  congr
  have hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix b').det :=
    IsIntegral.det fun i j => h _ _
  obtain ⟨r, hr⟩ := IsIntegrallyClosed.isIntegral_iff.1 hint
  have hunit : IsUnit r := by
    have : IsIntegral ℤ (b'.toMatrix (b.reindex (b.indexEquiv b'))).det :=
      IsIntegral.det fun i j => h' _ _
    obtain ⟨r', hr'⟩ := IsIntegrallyClosed.isIntegral_iff.1 this
    refine isUnit_iff_exists_inv.2 ⟨r', ?_⟩
    suffices algebraMap ℤ ℚ (r * r') = 1 by
      rw [← map_one (algebraMap ℤ ℚ)] at this
      exact (IsFractionRing.injective ℤ ℚ) this
    rw [map_mul, hr, hr', ← Matrix.det_mul, Basis.toMatrix_mul_toMatrix_flip, Matrix.det_one]
  rw [← map_one (algebraMap ℤ ℚ), ← hr]
  rcases Int.isUnit_iff.1 hunit with hp | hm
  · simp [hp]
  · simp [hm]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this✝ : n * n + 1 = a * a
na : n < a
this : (n + 1) * (n + 1) ≤ n * n + 1
⊢ n + n + (n * n + 1) ≤ 0 + (n * n + 1)

Tactic:
by ring_nf at this ⊢; assumption

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

Goal state before:
pp: d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Tactic:
by
  constructor
  · rintro ⟨x, rfl⟩
    simp
  · rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
    use ⟨r, i⟩
    rw [smul_val, Zsqrtd.ext_iff]
    exact ⟨hr, hi⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a

Tactic:
← mul_one (yn a1 m)

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: 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))

pp: 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

Tactic:
· simp only [H, mul_comm _ (k + 1)]; norm_cast

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

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

Tactic:
← Int.natCast_add,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 (n + 2) + xn a1 n) = ↑(2 * a) * ↑(xn a1 (n + 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
← Int.natCast_add,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(yn a1 (n + 2) + yn a1 n) = ↑(2 * a) * ↑(yn a1 (n + 1))
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
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
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)| ≤ 1

Tactic:
exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: m₁ m₂ n : ℕ
hm1 : m₁ ∈ n.smoothNumbers
hm2 : m₂ ∈ n.smoothNumbers
⊢ m₁ * m₂ ∈ n.smoothNumbers

Tactic:
rw [smoothNumbers_eq_factoredNumbers] at hm1 hm2 ⊢
  exact mul_mem_factoredNumbers hm1 hm2

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N

Tactic:
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]

Goal state after:
N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
Module: Mathlib.NumberTheory.SmoothNumbers

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

Tactic:
refine ⟨l.primeFactorsList.toFinset, ?_, m, ?_⟩

Goal state after:
case refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

case refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ n = m ^ 2 * l.primeFactorsList.toFinset.prod id
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
⊢ ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1

Tactic:
sub_sub,

Goal state after:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
⊢ ↑t = 2 * ↑(xn hw1 j) * ↑n - (↑n * ↑n + 1)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
have step1 := mellin_comp_rpow P.g (-s) (-1)
  simp_rw [abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one, neg_neg,
    rpow_neg_one, ← one_div] at step1
  -- introduce a power of `t` to match the hypothesis `P.h_feq`
  have step2 := mellin_cpow_smul (fun t ↦ P.g (1 / t)) (P.k - s) (-P.k)
  rw [← sub_eq_add_neg, sub_right_comm, sub_self, zero_sub, step1] at step2
  -- put in the constant `P.ε`
  have step3 := mellin_const_smul (fun t ↦ (t : ℂ) ^ (-P.k : ℂ) • P.g (1 / t)) (P.k - s) P.ε
  rw [step2] at step3
  rw [← step3]
  -- now the integrand matches `P.h_feq'` on `Ioi 0`, so we can apply `setIntegral_congr_fun`
  refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
  simp_rw [P.h_feq' t ht, ← mul_smul]
  -- some simple `cpow` arithmetic to finish
  rw [cpow_neg, ofReal_cpow (le_of_lt ht)]
  have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
  field_simp [P.hε]

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

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

Tactic:
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

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

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b ↦ jacobiTheta₂_term_fderiv b z τ

Tactic:
rw [summable_jacobiTheta₂_term_fderiv_iff]

Goal state after:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

Tactic:
arg_ofReal_of_nonneg (abs_nonneg _)

Goal state after:
case e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * 0
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

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

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Tactic:
arg_ofReal_of_nonneg (abs_nonneg _)

Goal state after:
case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * 0 ≤ π
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * 0 ≤ π

Tactic:
linarith [pi_pos]

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

Goal state before:
pp: ⊢ Tendsto (fun s ↦ (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (𝓝[{s | 1 < s.re}] 1) (𝓝 1)

Tactic:
refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_

Goal state after:
case refine_1
⊢ {s | 1 < s.re} ⊆ {1}ᶜ

case refine_2
⊢ (fun s ↦ (s - 1) * riemannZeta s) =ᶠ[𝓝[{s | 1 < s.re}] 1] fun s ↦ (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
hF :
  ∀ (t : ℝ),
    0 < t → HasSum (fun n ↦ if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)
⊢ completedCosZeta (↑a) s = mellin (fun t ↦ (↑(cosKernel (↑a) t) - 1) / 2) (s / 2)

Tactic:
rw [mellin_div_const, completedCosZeta]
    congr 1
    refine ((hurwitzEvenFEPair a).symm.hasMellin (?_ : 1 / 2 < (s / 2).re)).2.symm
    rwa [div_ofNat_re, div_lt_div_iff_of_pos_right two_pos]

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∀ t ⊆ {n | k ≤ n}, ∑' (n : ↑t), {p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False

Tactic:
specialize hk ({p | Nat.Prime p} ∩ {p | k ≤ p}) inter_subset_right

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (n : ↑({p | Nat.Prime p} ∩ {p | k ≤ p})), {p | Nat.Prime p}.indicator (fun n ↦ 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s) - 1 / (s - 1))
    1

Tactic:
sub_sub,

Goal state after:
a : UnitAddCircle
⊢ DifferentiableAt ℂ
    (fun s ↦ completedHurwitzZetaEven₀ a s - ((if a = 0 then 1 else 0) / s + 1 / (1 - s) + 1 / (s - 1))) 1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
⊢ b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

Tactic:
hb

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
n : ℕ
h : FermatLastTheoremWith' R n
hn : ∀ (a b c : R), IsUnit a → IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
⊢ c ≠ 0 → a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
⊢ b✝ = 1 → c✝ = 1 → a✝ ^ n + b✝ ^ n ≠ c✝ ^ n

Tactic:
hb

Goal state after:
n a✝ b✝ c✝ : ℕ
ha : a✝ = 1
hb : b✝ = 1
⊢ c✝ = 1 → a✝ ^ n + b✝ ^ n ≠ c✝ ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
⊢ IsUnit b → IsUnit c → a ^ n + b ^ n ≠ c ^ n

Tactic:
hb

Goal state after:
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
ha : IsUnit a
hb : IsUnit b
⊢ IsUnit c → a ^ n + b ^ n ≠ c ^ n
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
ha : a ≠ 0
⊢ b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

Tactic:
hb

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
ha : a ≠ 0
hb : b ≠ 0
⊢ c ≠ 0 → a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1

Tactic:
rw [← Hgcd]

Goal state after:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ {a, b, c}.gcd id
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
⊢ S.Nonempty

Tactic:
use Int.natAbs c

Goal state after:
case h
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := ⋯
⊢ c.natAbs ∈ S
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ℤ
⊢ z * z % 4 ≠ 2

Tactic:
suffices ¬z * z % (4 : ℕ) = 2 % (4 : ℕ) by exact this
  rw [← ZMod.intCast_eq_intCast_iff']
  simpa using sq_ne_two_fin_zmod_four _

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

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b

Tactic:
apply Int.isCoprime_iff_gcd_eq_one.mpr
  by_contra hab
  obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab
  obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa
  obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb
  have hpc : (p : ℤ) ^ 2 ∣ c := by
    rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
    apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
    ring
  obtain ⟨c1, rfl⟩ := hpc
  have hf : Fermat42 a1 b1 c1 :=
    (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1
  apply Nat.le_lt_asymm (h.2 _ _ _ hf)
  rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_natCast]
  · exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)
  · exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

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

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

Tactic:
hb

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

Goal state before:
pp: case left
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
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ 2 * (x / (y + 1)) / (1 + (x / (y + 1)) ^ 2) = x

pp: case right
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
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ (1 - (x / (y + 1)) ^ 2) / (1 + (x / (y + 1)) ^ 2) = y

Tactic:
· simp [field, h3]

Goal state after:
case right
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
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
h4 : 2 ≠ 0
⊢ (1 - (x / (y + 1)) ^ 2) / (1 + (x / (y + 1)) ^ 2) = y