mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 2 ^ 9 * (2 * 512) ^ 32 ≤ 4 ^ (512 / 3)

Tactic:
conv in 2 * 512 => equals 2 ^ 10 => 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 ^ 10) ^ 32 ≤ 4 ^ (512 / 3)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : p = 2 ∧ m = 2
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
obtain ⟨rfl, rfl⟩ := hm2

Goal state after:
case pos
d : ℕ
hd : d ≥ 2
n : ℕ
inst✝ : Fact (Nat.Prime 2)
hcase : ¬(2 = 2 ∧ d = 2)
hp2 : 2 ≤ 2
hm : Nat.le 2 2
IH : ¬(2 = 2 ∧ 2 = 2) → 2 + 1 ≤ 2 ^ (2 - 1)
hne' : ¬(2 = 2 ∧ succ 2 = 2)
⊢ succ 2 + 1 ≤ 2 ^ (succ 2 - 1)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ.inl
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
      simp only [hi_eq]
      exact pIntegral_bernoulli_even_term hm_lt (ih m hm_pos hm_lt)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h.e_a
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
hAlg :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
simpa using faulhaber_sum_div_prime_eq

Goal state after:
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
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, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
let q := ∑ i, (qs k i - qs j i) • bS i

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
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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x.zmodRepr).zmodRepr = x.zmodRepr

Tactic:
apply zmodRepr_unique _ _ (zmodRepr_lt_p _)

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x.zmodRepr - ↑x.zmodRepr ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_2.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 • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₀.succ % b)) <
    cardPowDegree b • ε
⊢ False

Tactic:
rw [Fin.cons_succ, Fin.cons_succ] at approx
      rw [Ne, Fin.succ_inj] at j_ne
      have : j₀ = j₁ := (Classical.choose_spec (hg j₀)).1.symm.trans
        (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
          (Classical.choose_spec (hg j₁)).1)
      contradiction

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ a 0 = 0

Tactic:
by simp [a, not_prime_zero]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False

Tactic:
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi

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

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
⊢ χ₀ n (RingEquiv.refl L) = 1

Tactic:
refine (toFun_unique n (RingEquiv.refl L) 1 <| fun t ↦ ?_).symm
  have : 1 ≤ Nat.card { x // x ∈ rootsOfUnity n L } := Nat.card_pos
  obtain (h | h) := this.lt_or_eq
  · have := Fact.mk h
    simp [ZMod.val_one]
  · have := Finite.card_le_one_iff_subsingleton.mp h.ge
    obtain rfl : t = 1 := Subsingleton.elim t 1
    simp

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
g : L ≃+* L
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (χ p g) = ↑((modularCyclotomicCharacter L ⋯) g)

Tactic:
rw [toFun_apply]

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
g : L ≃+* L
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (PadicInt.ofIntSeq (fun n ↦ aux g (p ^ n)) ⋯) = ↑((modularCyclotomicCharacter L ⋯) g)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
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) < ε
⊢ ∃ ia ∈ galGroupBasis K L,
    ∀ x ∈ id ia,
      ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
        Metric.ball 1 ε

Tactic:
refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩

Goal state after:
case pos.refine_1
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) < ε
⊢ IsIntegral K (ζ k)

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) < ε
⊢ ∀ x ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup),
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
      Metric.ball 1 ε
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: b : Basis (Fin 1) ℤ (𝓞 ℚ) := (Basis.singleton (Fin 1) ℤ).map ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
⊢ (Algebra.trace ℤ (𝓞 ℚ)) 1 = 1

Tactic:
by rw [Algebra.trace_eq_matrix_trace b]; simp

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
⊢ nthHomSeq f_compat (r * s) ≈ nthHomSeq f_compat r * nthHomSeq f_compat s

Tactic:
intro ε hε
  obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
  use n
  intro j hj
  dsimp [nthHomSeq]
  apply lt_of_le_of_lt _ hn
  rw [← Int.cast_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]
  dsimp [nthHom]
  simp only [ZMod.natCast_val, map_mul, Int.cast_sub, ZMod.intCast_cast, Int.cast_mul]
  rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]

Goal state after:
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
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ∀ i ≥ N, padicNormE (mk s - ↑(↑s i)) < ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)

Tactic:
replace hN := hN (N + n) (Nat.le_add_right N n)

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : padicNormE (mk s - ↑(↑s (N + n))) < ↑p ^ (-↑n)
⊢ (toZModPow n) x = ↑(f n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
rintro ⟨x, rfl⟩
    simp

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

Goal state before:
pp: case nonzero
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : 0 ∣ a
hre : re 0 = 0
him : im 0 = 0
⊢ False

Tactic:
rw [zero_dvd_iff] at hdvd

Goal state after:
case nonzero
d : ℤ
a : ℤ√d
hcoprime : IsCoprime a.re a.im
hdvd : a = 0
hre : re 0 = 0
him : im 0 = 0
⊢ False
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
⊢ (SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧
    (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
      (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧
        (SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1)

Tactic:
by
  refine ⟨?_, ?_, ?_, ?_⟩ <;>
    · intro xy zw
      have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
      refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
      convert! this using 1
      simp only [one_mul, Int.natCast_add, Int.natCast_mul]
      ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]

Tactic:
← ke

Goal state after:
a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
xm : yn a1 t ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case zero
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
hζone : ζ = 1
⊢ (Matrix.of fun i j ↦ ((traceForm K L) (ζ ^ ↑i)) (ζ ^ ↑j)).det = 1 * ↑p ^ (p ^ (0 - 1) * (0 - 1))

Tactic:
hζ.powerBasis_dim _,

Goal state after:
case zero
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
hζone : ζ = 1
⊢ (Matrix.of fun i j ↦ ((traceForm K L) (ζ ^ ↑i)) (ζ ^ ↑j)).det = 1 * ↑p ^ (p ^ (0 - 1) * (0 - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
by
    have : 2 * n - j + j ≤ n + j := by
      rw [tsub_add_cancel_of_le h, two_mul]; exact Nat.add_le_add_left jn _
    let t := xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
    rwa [tsub_tsub_cancel_of_le h, add_comm] at t

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (4 * n + j) + xn a1 (2 * n + j) ≡ xn a1 j + xn a1 (2 * n + j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_add _ _ _).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_assoc]
    apply xn_modEq_x2n_add

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
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 ≤ N.sqrt

Tactic:
le_sqrt'

Goal state after:
case refine_2
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 ^ 2 ≤ N
Module: Mathlib.NumberTheory.EulerProduct.Basic

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

Tactic:
rw [factoredNumbers_empty]

Goal state after:
case empty
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
⊢ ∃ x < s.re, LSeriesSummable f ↑x

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs
  exact ⟨x, by simpa using hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩

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

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ↑x

Tactic:
refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_

Goal state after:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})
a : EReal
⊢ ↑x < a → y ≤ a
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ⊆ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (x : ↑(factoredNumbers s)ᶜ), f ↑x‖ < ε

Tactic:
tsum_eq_tsum_sdiff_singleton (factoredNumbers s)ᶜ hf₀

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hsum : Summable f
hf₀ : f 0 = 0
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ t ⊆ {n | N ≤ n}, ‖∑' (n : ↑t), f ↑n‖ < ε
s : Finset ℕ
hs : N.primesBelow ⊆ s
this : ‖∑' (n : ↑((factoredNumbers s)ᶜ \ {0})), f ↑n‖ < ε
⊢ ‖∑' (a : ↑((factoredNumbers s)ᶜ \ {0})), f ↑a‖ < ε
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: case succ
f : ℕ → ℂ
n : ℕ
ih : abscissaOfAbsConv (logMul^[n] f) = abscissaOfAbsConv f
⊢ abscissaOfAbsConv (logMul^[n + 1] f) = abscissaOfAbsConv f

Tactic:
simp [ih, Function.iterate_succ', Function.comp_def,
      -Function.comp_apply, -Function.iterate_succ]

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

Goal state before:
pp: case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u - 1 / 2 < ↑u - 1
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
sub_lt_sub_iff_left

Goal state after:
case h.inr.inl.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * cexp ↑(-(p i * t)) = (1 / ↑(p i)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / ↑(p i) ^ s) = a i * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume

Tactic:
← ofReal_exp,

Goal state after:
case e'_5.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * ↑(rexp (-(p i * t))) = (1 / ↑(p i)) ^ s * Complex.Gamma s
⊢ a i * (Complex.Gamma s / ↑(p i) ^ s) = a i * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ ‖rexp (-d * t)‖ ≤ rexp (-c * t)

Tactic:
norm_of_nonneg (exp_pos _).le

Goal state after:
c d : ℝ
hcd : c ≤ d
t : ℝ
ht : 0 < t
⊢ rexp (-d * t) ≤ rexp (-c * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: t : ℝ
ht : 0 < t
⊢ ‖F_nat 0 0 t - 1‖ ≤ rexp (-π * t) / (1 - rexp (-π * t))

Tactic:
by
  convert! F_nat_zero_le zero_le_one ht using 2
  · rw [F_nat, (summable_f_nat 0 0 ht).tsum_eq_zero_add, f_nat, Nat.cast_zero, add_zero, pow_zero,
      one_mul, pow_two, mul_zero, mul_zero, zero_mul, exp_zero, add_comm, add_sub_cancel_right]
    simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]
  · rw [one_pow, mul_one]

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

pp: case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ

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:
case mpr
z τ : ℂ
⊢ 0 < τ.im → Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
let a' i := if p i = 0 then 0 else a i

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
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
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ -(P.ε * ((∫ (x : ℝ) in 0..1, ↑x ^ (s - ↑P.k - 1)) * 1)) = P.ε / (↑P.k - s) * 1

Tactic:
· simp [integral_cpow (.inl h_re2), zero_cpow (show s - P.k ≠ 0 by grind [P.hk, ofReal_re])]
        grind

Goal state after: