mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f * (↑(n i) - ↑1 + 1) = (coeff n) g * (↑(n i) - ↑1 + 1)
⊢ (coeff n) f = (coeff n) g

Tactic:
Nat.cast_one,

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f * (↑(n i) - 1 + 1) = (coeff n) g * (↑(n i) - 1 + 1)
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_2
p : ℕ
hp : Nat.Prime p
odd : Odd p
q m : ℕ
hq : Nat.Prime q
hn : Odd (q ^ m)
hn0 : q ^ m ≠ 0
h1 : q ^ m ≠ 1
dvd : p ∣ q ^ m
hnp : ¬q ^ m = p ^ (q ^ m).factorization p
⊢ q ^ m = p ^ (q ^ m).factorization p

Tactic:
cases (Nat.prime_dvd_prime_iff_eq hp hq).mp (hp.dvd_of_dvd_pow dvd)

Goal state after:
case neg.refine_2.refl
p : ℕ
hp : Nat.Prime p
odd : Odd p
m : ℕ
hq : Nat.Prime p
hn : Odd (p ^ m)
hn0 : p ^ m ≠ 0
h1 : p ^ m ≠ 1
dvd : p ∣ p ^ m
hnp : ¬p ^ m = p ^ (p ^ m).factorization p
⊢ p ^ m = p ^ (p ^ m).factorization p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
p m : ℕ
h0 : ¬p ^ m = 0
h1 : ¬p ^ m = 1
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
⊢ 1 ≤ m

Tactic:
contrapose! h1

Goal state after:
case neg.inl
p m : ℕ
h0 : ¬p ^ m = 0
h2 : ¬p ^ m = 2
h4 : ¬p ^ m = 4
hn : Odd (p ^ m)
h1 : m < 1
⊢ p ^ m = 1
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ _root_.bernoulli n * ↑1 = _root_.bernoulli n

Tactic:
Nat.cast_one,

Goal state after:
n : ℕ
⊢ _root_.bernoulli n * 1 = _root_.bernoulli n
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Tendsto π' atTop atTop

Tactic:
by
  apply tendsto_atTop_atTop_of_monotone' monotone_primeCounting'
  simp [Set.range_eq_univ.mpr surjective_primeCounting']

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ioo 1 n)

Tactic:
by
  ext p
  simp +contextual [primesBelow_eq_filter_range, Nat.Prime.one_lt]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 +
      (f ↑1 * c 1 +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * ∑ k ∈ Icc 0 1, c k -
          ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
Nat.cast_one,

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * c 0 +
      (f 1 * c 1 +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * ∑ k ∈ Icc 0 1, c k -
          ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (C (-1) * X)).coeff i =
    ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i

Tactic:
Polynomial.comp_C_mul_X_coeff,

Goal state after:
case succ
n i : ℕ
⊢ (bernoulli (n + 1)).coeff i * (-1) ^ i = ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large
  have n2_pos : 1 ≤ 2 * n := mul_pos (zero_lt_two' ℕ) n_pos
  let S := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
  let f x := x ^ n.centralBinom.factorization x
  have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by
    refine Finset.prod_filter_of_ne fun p _ h => ?_
    contrapose h; dsimp only [f]
    rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]
  rw [centralBinom_factorization_small n n_large no_prime, ← this, ←
    Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))]
  apply mul_le_mul'
  · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
    · exact pow_factorization_choose_le (mul_pos two_pos n_pos)
    have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
    rw [Finset.prod_const]
    refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)
    obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
    exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩
  · refine le_trans ?_ (primorial_le_four_pow (2 * n / 3))
    refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_
    · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
      refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le
      exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)
    refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_
    exact fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case b0
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
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ 0 < ↑(normBound abv bS)

Tactic:
exact Int.cast_pos.mpr (normBound_pos abv bS)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ N

Tactic:
· apply le_trans _ hN
    rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]
    gcongr

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
⊢ (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * ↑T

Tactic:
exact_mod_cast hT_int

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ ψ x ≤ (log 4 + 4) * x

Tactic:
by
  by_cases! hx : x < 1
  · rw [psi_eq_zero_of_lt_two (by linarith)]
    bound
  apply le_trans (psi_le hx)
  rw [add_mul]
  gcongr 1
  grw [sqrt_eq_rpow, log_le_rpow_div (ε := 1 / 2) (by linarith) (by linarith), ← mul_div_assoc,
    ← mul_one_div]
  nth_rw 2 [mul_assoc]
  rw [← rpow_add (by linarith)]
  norm_num
  linarith

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
n : ℕ
a : R[X]
⊢ (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) ((monomial n) a)) =
    (aeval y) ((Transcendental.algEquivAdjoin hx) ((monomial n) a))

Tactic:
| monomial n a =>

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.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 • ε
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₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε

Tactic:
exact ht' i₀ i₁

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x

Tactic:
← hx2

Goal state after:
ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤
    log 4 * x / log x + ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (discr R ⇑b)

Tactic:
rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
    Algebra.traceMatrix_localizationLocalization]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case f
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
| fun σ ↦ σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
ext σ

Goal state after:
case f
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), σ pb.gen ∈ (minpoly K pb.gen).aroots E
σ : L →ₐ[K] E
| σ ((aeval pb.gen) (derivative (minpoly K pb.gen)))
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)

Tactic:
rw [discr_def]
  exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

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

Goal state before:
pp: c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ SqLe z c w d

Tactic:
apply le_of_not_gt

Goal state after:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬d * w * w < c * z * z
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
⊢ ¬d * w * w < c * z * z

Tactic:
intro l

Goal state after:
c d x y z w : ℕ
zw : SqLe y d x c
h : SqLe (x + z) c (y + w) d
l : d * w * w < c * z * z
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ xn a1 (n % m) * yn a1 (m * (n / m)) + yn a1 (n % m) * xn a1 (m * (n / m))
hp : n % m > 0
co : (yn a1 m).Coprime (xn a1 (m * (n / m)))
m0 : 0 < m
⊢ False

Tactic:
exact
          not_le_of_gt (strictMono_y _ <| Nat.mod_lt n m0)
            (Nat.le_of_dvd (strictMono_y _ hp) <|
              co.dvd_of_dvd_mul_right <|
                (Nat.dvd_add_iff_right <| (y_mul_dvd _ _ _).mul_left _).2 h)

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a‖ ^ Nat.card (ZMod n)ˣ = 1

Tactic:
← norm_pow,

Goal state after:
F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : (ZMod n)ˣ
⊢ ‖χ ↑a ^ Nat.card (ZMod n)ˣ‖ = 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num - 1 < ξ * ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
norm_cast at h₁ h₂

Goal state after:
case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑(q.num + 1)
h₂ : ↑(q.num - 1) < ξ * ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
Module: Mathlib.NumberTheory.SmoothNumbers

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

Tactic:
mem_factoredNumbers

Goal state after:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s
Module: Mathlib.NumberTheory.SmoothNumbers

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

Tactic:
mem_factoredNumbers

Goal state after:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 k = xn a1 0 ∧ yn a1 k = yn a1 0

Tactic:
ky

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧
              b ≡ 1 [MOD 4 * yn a1 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 0 = xn a1 0 ∧ yn a1 0 = yn a1 0
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
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ ↑t ∣ ↑(yn a1 k * (xn hw1 j - n) + n ^ k) - ↑(xn a1 k)

Tactic:
te,

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
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1 ∣ ↑(yn a1 k * (xn hw1 j - n) + n ^ k) - ↑(xn a1 k)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h.inl
v : ℕ
ih : ∀ m < v, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ| < 0
⊢ ∃ n, ↑u / ↑v = ξ.convergent n

Tactic:
exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)

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

Goal state before:
pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = ξ.convergent n

Tactic:
Nat.cast_one,

Goal state after:
case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / 1 = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
m : ℕ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
⊢ iteratedDeriv m (LSeries f) s = (-1) ^ m * LSeries (logMul^[m] f) s

Tactic:
induction m generalizing s with

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

Goal state before:
pp: case e'_5.inl
ι : 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 : ι
hai : a i = 0
⊢ a i * (Complex.Gamma s / ↑(p i) ^ s) = a i * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume

Tactic:
rw [hai, zero_mul, zero_mul]

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

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

Tactic:
Nat.cast_one,

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

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

Tactic:
Real.norm_of_nonneg pi_pos.le,

Goal state after:
case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * ‖I‖ * ‖↑n‖ * ‖ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2
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
⊢ ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀ =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀

Tactic:
integral_sub,

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
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ (∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) • P.f₀) - ∫ (a : ℝ) in Ioc 0 1, P.ε • ↑a ^ (s - ↑P.k - 1) • P.g₀ =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1)) • P.f₀ - P.ε • (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - ↑P.k - 1)) • P.g₀

case hf
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
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

case hg
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
⊢ Integrable (fun x ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_1
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : Summable u
n : ℤ
⊢ ContinuousOn (fun p ↦ jacobiTheta₂'_term n p.1 p.2) V

Tactic:
apply Continuous.continuousOn
    unfold jacobiTheta₂'_term jacobiTheta₂_term
    fun_prop

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

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Tactic:
change completedHurwitzZetaEven₀ a s - (1 / (s / 2)) • (if a = 0 then 1 else 0) / 2 =
      completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s
    rw [smul_eq_mul, mul_comm, mul_div_assoc, div_div, div_mul_cancel₀ _ two_ne_zero, mul_one_div]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ Summable fun n ↦ 1 / ↑n ^ s

Tactic:
Complex.summable_one_div_nat_cpow

Goal state after:
s : ℂ
hs : 1 < s.re
this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ 1 < s.re