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

Goal state before:
pp: case inr.inl
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
⊢ (-1) ^ n * bernoulli' n = bernoulli' n

Tactic:
heven.neg_one_pow,

Goal state after:
case inr.inl
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
⊢ 1 * bernoulli' n = bernoulli' n
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 512 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)

Tactic:
conv in 512 => equals 2 ^ 9 => norm_num1

Goal state after:
case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ 9 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ ∑ i ∈ Icc 0 n, ‖f ↑i * c i‖ = ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖

Tactic:
by simp_rw [norm_mul]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
⊢ (fun n ↦ f ↑n * if n = 0 then 0 else c n) =ᶠ[atTop] fun n ↦ f ↑n * c n

Tactic:
filter_upwards [eventually_ne_atTop 0] with k hk

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
k : ℕ
hk : k ≠ 0
⊢ (f ↑k * if k = 0 then 0 else c k) = f ↑k * c k
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
theta_eq_log_primorial

Goal state after:
x : ℝ
hx : 0 ≤ x
⊢ log ↑(primorial ⌊x⌋₊) ≤ log 4 * x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case e'_4
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ Fintype.card ι •
      ((Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) =
    Finset.univ.card • y * ?convert_5

Tactic:
Finset.card_univ,

Goal state after:
case e'_4
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
a : S
y : ℤ
hy : ∀ (k : ι), abv ((bS.repr a) k) ≤ y
⊢ Fintype.card ι •
      ((Finset.image (fun ijk ↦ abv ((Algebra.leftMulMatrix bS) (bS ijk.1) ijk.2.1 ijk.2.2)) Finset.univ).max' ⋯ * y) =
    Fintype.card ι • y * ?convert_5
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊ ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)

Tactic:
← Nat.le_ceil

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq) ≤ ↑b.natDegree - -log ε / log ↑(Fintype.card Fq)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ cardPowDegree (x - z) < a

Tactic:
refine lt_of_le_of_lt ?_ (max_lt hxy hyz)

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ cardPowDegree (x - z) ≤ max (cardPowDegree (x - y)) (cardPowDegree (y - z))
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ Fin.cons j t' i₀ = Fin.cons j t' i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
refine Fin.cases ?_ (fun i₀ => ?_) i₀

Goal state after:
case succ.refine_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ Fin.cons j t' 0 = Fin.cons j t' i₁ ↔ ↑(cardPowDegree (A i₁ % b - A 0 % b)) < cardPowDegree b • ε

case succ.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁ : Fin (n + 1)
i₀ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀.succ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑↑(r.den.gcd p) % ↑p = ↑(↑r.den * r.den.gcdA p + ↑p * r.den.gcdB p) % ↑p
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0

Tactic:
simp only [Int.cast_natCast, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add,
    Int.cast_mul, zero_mul, add_zero] at this

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑(r.num * r.den.gcdA p % ↑p) * ↑r.den = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
| IntegrableOn (fun t ↦ θ t / (t * log t ^ 2)) (Set.Icc 2 x) volume

Tactic:
arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Goal state after:
x x✝ : ℝ
| 1 / (x✝ * log x✝ ^ 2) * ∑ a ∈ Ioc 0 ⌊x✝⌋₊, if Nat.Prime a then log ↑a else 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), x - ↑x.zmodRepr ∈ Ideal.span {↑p}

Tactic:
rw [← maximalIdeal_eq_span_p]
      exact sub_zmodRepr_mem

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

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

Tactic:
rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x✝ : ℝ
| √x✝ / log 2 ^ 2

Tactic:
← mul_one_div,

Goal state after:
x✝ : ℝ
| √x✝ * (1 / log 2 ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε

Tactic:
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt_rat p hε

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε

Tactic:
simp only [← Int.cast_sub]

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p ↑(f j - f i) < ε
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = 1 ↔
    star { re := x, im := y } * { re := x, im := y } = 1 ∧ { re := x, im := y } * star { re := x, im := y } = 1

Tactic:
mul_comm (star _),

Goal state after:
d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = 1 ↔
    { re := x, im := y } * star { re := x, im := y } = 1 ∧ { re := x, im := y } * star { re := x, im := y } = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
⊢ IsCoprime b.re b.im

Tactic:
by
  apply isCoprime_of_dvd
  · rintro ⟨hre, him⟩
    obtain rfl : b = 0 := Zsqrtd.ext hre him
    rw [zero_dvd_iff] at hdvd
    simp [hdvd, im_zero, re_zero, not_isCoprime_zero_zero] at hcoprime
  · rintro z hz - hzdvdu hzdvdv
    apply hz
    obtain ⟨ha, hb⟩ : z ∣ a.re ∧ z ∣ a.im := by
      rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩
    exact hcoprime.isUnit_of_dvd' ha hb

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
n : ℤ
⊢ IsPoly fun v ↦ (const n) (v ∘ f)

Tactic:
simpa using IsPoly.const _

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

Goal state before:
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:
· have := hne.1
      rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by lia)] at this
      exact absurd (eq_zero_of_pow_eq_zero h) this

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

Goal state before:
pp: case inl.inr.inr
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
refine nonnegg_cases_left fun i h => sqLe_of_le ?_ ?_ (nonnegg_neg_pos.1 hb)

Goal state after:
case inl.inr.inr.refine_1
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ i ≤ z

case inl.inr.inr.refine_2
d x y : ℕ
ha : { re := ↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := ↑x, im := ↑y }.re + { re := -↑z, im := ↑w }.re = -↑i
⊢ w ≤ y + w
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: 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
⊢ p = 2

Tactic:
rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ∈ factoredNumbers s
⊢ m.primeFactors ⊆ s

Tactic:
by
  rw [mem_factoredNumbers] at hm
  exact fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

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

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

Tactic:
rw [filter_insert]

Goal state after:
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))
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' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u' / ↑v - ↑⌊ξ⌋
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
sub_right_comm,

Goal state after:
ξ : ℝ
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' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑⌊ξ⌋ - ↑u' / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
⊢ toArithmeticFunction f = toArithmeticFunction f'

Tactic:
ext
  simp_all [toArithmeticFunction]

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

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
hsum : Summable fun x ↦ term f s x.1 * term g s x.2
⊢ LSeriesHasSum (f ⍟ g) s (a * b)

Tactic:
simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _

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

Goal state before:
pp: a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
⊢ 0 < f ↑y

Tactic:
have hxy : x < max x y + 1 := (le_max_left x y).trans_lt (lt_add_one _)

Goal state after:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
⊢ 0 < f ↑y
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t ↦ P.g (1 / t)) (↑P.k - s - ↑P.k)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
sub_right_comm,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t ↦ P.g (1 / t)) (↑P.k - ↑P.k - s)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

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

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

Tactic:
· replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero
        simp_rw [Function.comp_def, Int.cast_natCast] at h
        refine atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop 0) ?_)
        refine tendsto_exp_atTop.comp ?_
        simp only [tendsto_neg_atTop_iff, mul_assoc]
        apply Filter.Tendsto.const_mul_atBot two_pos
        exact (tendsto_natCast_atTop_atTop.atTop_mul_const_of_neg hz).const_mul_atBot pi_pos

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

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

Goal state before:
pp: case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ 1 * π * ↑|n| ^ 2

Tactic:
simp_rw [hns, norm_mul, one_mul, norm_I, mul_one,
      norm_real, norm_of_nonneg pi_pos.le, ← ofReal_intCast, ← ofReal_pow, norm_real,
      Real.norm_eq_abs, Int.cast_abs, abs_pow]
    apply mul_le_of_le_one_right (mul_nonneg pi_pos.le (pow_nonneg (abs_nonneg _) _))
    exact ContinuousLinearMap.norm_snd_le ..

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

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ * ‖(0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖

Tactic:
simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]

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

Goal state before:
pp: a x : ℝ
⊢ ↑(cosKernel (↑a) x) = jacobiTheta₂ (↑a) (I * ↑x)

Tactic:
by
  simp [cosKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two,
    mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

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

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

pp: case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
· rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]
    exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx

Goal state after:
case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
⊢ HasMellin (fun x ↦ P.f x - P.f₀) s (P.Λ s)

Tactic:
refine ⟨hc1, ?_⟩

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
hc1 : MellinConvergent (fun x ↦ P.f x - P.f₀) s
⊢ mellin (fun x ↦ P.f x - P.f₀) s = P.Λ s