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

Goal state before:
pp: case refine_2.refine_1.e_6
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ ∑ x, ((rs k x • bS.repr (bS x)) i - (rs j x • bS.repr (bS x)) i) = rs k i - rs j i

Tactic:
Finsupp.smul_apply,

Goal state after:
case refine_2.refine_1.e_6
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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ ∑ x, (rs k x • (bS.repr (bS x)) i - rs j x • (bS.repr (bS x)) i) = rs k i - rs j i
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f (x * y)) = ↑(f x) * ↑(f y)

Tactic:
f_congr (x * y) _ (f x * f y),

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f x * f y) = ↑(f x) * ↑(f y)

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x * y - ↑(f (x * y)) ∈ Ideal.span {↑v}

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x * y - ↑(f x * f y) ∈ Ideal.span {↑v}
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
intro n

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n ≤ x.appr (n + 1)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
⊢ dist (↑((cyclotomicCharacter L p) ((MulSemiringAction.toRingAut Gal(L/K) L) σ))) 1 ≤ ↑p ^ (-↑k)

Tactic:
dist_eq_norm,

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
⊢ ‖↑((cyclotomicCharacter L p) ((MulSemiringAction.toRingAut Gal(L/K) L) σ)) - 1‖ ≤ ↑p ^ (-↑k)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
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 : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
intro n

Goal state after:
case h
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 : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
⊢ n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist ((lift f_compat) r) (g r) ≤ ↑p ^ (-↑n)

Tactic:
dist_eq_norm,

Goal state after:
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖(lift f_compat) r - g r‖ ≤ ↑p ^ (-↑n)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
⊢ ∀ (n : ℕ), (toZModPow n) (g x) = (toZModPow n) (g' x)

Tactic:
intro n

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
x : R
n : ℕ
⊢ (toZModPow n) (g x) = (toZModPow n) (g' x)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: 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
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) =
    (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
have hp2 : p = 2 → k ≠ 0 := by
    rintro rfl rfl
    exact absurd rfl hk

Goal state after:
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
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) *
      (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) =
    (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : b ∣ a
z : ℤ
hz : z ∈ nonunits ℤ
hzdvdu : z ∣ b.re
hzdvdv : z ∣ b.im
⊢ z ∣ a.re ∧ z ∣ a.im

Tactic:
rw [← intCast_dvd]
      apply dvd_trans _ hdvd
      rw [intCast_dvd]
      exact ⟨hzdvdu, hzdvdv⟩

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h : { re := x, im := y } * { re := z, im := w } = 0
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0

Tactic:
injection h with h1 h2

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y z w : ℤ
h1 : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0
h2 : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0
⊢ { re := x, im := y } = 0 ∨ { re := z, im := w } = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
obtain ⟨d', rfl⟩ := Int.eq_ofNat_of_zero_le h
    have : Nonsquare d' := ⟨fun n h => h_nonsquare n <| mod_cast h⟩
    exact divides_sq_eq_zero_z ha

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ a = 0

Tactic:
suffices lift r a.norm = 0 by
      simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) ↑a.norm = 0
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
⊢ False

Tactic:
exact absurd j2n (by decide)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
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' : i + 1 < n
⊢ 0 < xn a1 (i + 1) % xn a1 n

Tactic:
exact
          x0.trans
            (eq_of_xn_modEq_lem3 _ (Nat.pos_of_ne_zero npos) (Nat.succ_pos _) (le_trans ij j2n)
              (_root_.ne_of_lt ij') fun ⟨_, n1, _, i2⟩ => by
              rw [n1, i2] at ij'; exact absurd ij' (by decide))

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
⊢ (factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
intro n

Goal state after:
N : ℕ
s : Finset ℕ
h : N.primesBelow ⊆ s
n : ℕ
⊢ n ∈ (factoredNumbers s)ᶜ \ {0} → n ∈ {n | N ≤ n}
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ False

Tactic:
have H : (2 * v - 1 : ℝ) < 1 := by
    refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))
    have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field
    rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_iff_of_pos_right hv₀]
    norm_cast
    rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]
    rintro rfl
    cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2) <;> lia

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
H : 2 * ↑v - 1 < 1
⊢ False
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactorsList.toFinset.prod id

Tactic:
simp only [toFinset_factors]

Goal state after:
case refine_2.e_a
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ l = l.primeFactors.prod id
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ N.smoothNumbersUpTo k ⊆
    Finset.image
      (fun x ↦
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
intro n

Goal state after:
N k n : ℕ
⊢ n ∈ N.smoothNumbersUpTo k →
    n ∈
      Finset.image
        (fun x ↦
          match x with
          | (s, m) => m ^ 2 * s.prod id)
        (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x : ℕ
⊢ 0 = 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ x / 0 = z

pp: case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z

Tactic:
· simp [eq_comm]

Goal state after:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with Nat.Prime p, F p
⊢ dist (∏ p ∈ s with Nat.Prime p, F p) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
dist_eq_norm,

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with Nat.Prime p, F p
⊢ ‖∏ p ∈ s with Nat.Prime p, F p - ∑'[{ filter := Filter.atTop }] (n : ℕ), f n‖ < ε
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
⊢ HasProd ({p | Nat.Prime p}.mulIndicator fun p ↦ ∑' (e : ℕ), f (p ^ e)) (∑' (n : ℕ), f n)

Tactic:
rw [← hasProd_subtype_iff_mulIndicator]

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
⊢ HasProd ((fun p ↦ ∑' (e : ℕ), f (p ^ e)) ∘ Subtype.val) (∑' (n : ℕ), f n)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖P.ε‖ * ‖P.g₀‖ * ‖x ^ (-P.k)‖) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖

Tactic:
apply (isBigO_refl _ _).const_mul_left

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

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (-π * 0 ^ 2 * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t

Tactic:
pow_two,

Goal state after:
case e'_3
t : ℝ
ht : 0 < t
⊢ rexp (-π * (0 * 0) * t) + ∑' (b : ℕ), f_nat 0 0 t (b + 1) - 1 = F_nat 0 1 t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
neg_neg

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

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ (fun b ↦ ↑b * rexp (-π * (↑b + a ^ 2) * t)) = fun i ↦ rexp (-π * a ^ 2 * t) * (↑i * rexp (-π * t) ^ i)

pp: case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)

Tactic:
· ext1 n
      rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
      ring_nf

Goal state after:
case e'_6
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
⊢ rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 =
    rexp (-π * a ^ 2 * t) * (rexp (-π * t) / (1 - rexp (-π * t)) ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ), ‖f_int k a t n‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Tactic:
intro n

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℤ
⊢ ‖f_int k a t n‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖
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}
⊢ IsOpen {v | T < v.im}

Tactic:
exact continuous_im.isOpen_preimage _ isOpen_Ioi

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

Goal state before:
pp: case refine_1.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : s ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

pp: case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s

Tactic:
· fun_prop

Goal state after:
case refine_1.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
hs' : s ≠ ↑P.k ∨ P.g₀ = 0
hs : P.f₀ = 0
⊢ DifferentiableAt ℂ (fun s ↦ (1 / s) • P.f₀) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ I / ↑x = - -I / ↑x

Tactic:
neg_neg

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I / ↑x = I / ↑x
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ 𝓝 0 = 𝓝 (0 • (P.ε / (↑P.k - 0)) • P.g₀)

Tactic:
rw [zero_smul]

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

Goal state before:
pp: z τ J J' : ℂ
⊢ cexp (↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ))) * (J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I)) =
    cexp (↑π * I * z ^ 2 * τ) * (J' + z * J * (2 * ↑π * I))

Tactic:
congrm (cexp ?_ * ?_)

Goal state after:
case refine_1
z τ J J' : ℂ
⊢ ↑π * I * (z + 1) ^ 2 * τ + -↑π * I * (τ + 2 * (z * τ)) = ↑π * I * z ^ 2 * τ

case refine_2
z τ J J' : ℂ
⊢ J' - 2 * ↑π * I * J + (z * J + J) * (2 * ↑π * I) = J' + z * J * (2 * ↑π * I)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H.refine_1
a x : ℝ
hx : x ∈ Ioi 0
⊢ Continuous fun x ↦ cexp (-↑π * ↑a ^ 2 * ↑x)

pp: case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x

Tactic:
· fun_prop

Goal state after:
case H.refine_2
a x : ℝ
hx : x ∈ Ioi 0
⊢ ContinuousAt (fun x ↦ jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
    x
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
⊢ ‖a i * ↑(r i)‖ / (|r i| ^ s.re * |r i| ^ 1) = ‖a i‖ / |r i| ^ s.re

Tactic:
rpow_one,

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
⊢ ‖a i * ↑(r i)‖ / (|r i| ^ s.re * |r i|) = ‖a i‖ / |r i| ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ∀ (i : ℕ),
    ‖2 * Real.cos (2 * π * a * (↑i + 1)) * rexp (-π * (↑i + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t i

Tactic:
intro n

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 0 1 t n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < - -(τ.im / normSq τ)

Tactic:
neg_neg

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedHurwitzZetaEven 0 (1 - s) = completedCosZeta 0 s

Tactic:
completedHurwitzZetaEven_one_sub

Goal state after:
s : ℂ
⊢ completedCosZeta 0 s = completedCosZeta 0 s