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

Goal state before:
pp: n : ℕ
⊢ 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k =
    1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k

Tactic:
← Fin.sum_univ_eq_sum_range

Goal state after:
n : ℕ
⊢ 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k = 1 - ∑ i, ↑(n.choose ↑i) / (↑n - ↑↑i + 1) * bernoulli' ↑i
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n p : ℕ
⊢ (↑p + 1) * ∑ k ∈ range n, ↑k ^ p = eval (↑n) (bernoulli p.succ) - _root_.bernoulli p.succ

Tactic:
by
  rw [sum_range_pow, bernoulli_def, eval_finsetSum, ← sum_div, mul_div_cancel₀ _ _]
  · simp_rw [eval_monomial]
    symm
    rw [← sum_flip _, sum_range_succ]
    simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero,
      add_tsub_cancel_right]
    apply sum_congr rfl fun x hx => _
    intro x hx
    apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
    · rw [Nat.sub_sub_self (mem_range_le hx)]
    · rw [← choose_symm (mem_range_le hx)]
  · norm_cast

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m : ℕ
ihn : ∀ m_1 < m + m + 1, m_1 ≠ 0 → m_1# < 4 ^ m_1
hn : m + m + 1 ≠ 0
hm : m > 0
⊢ (m + m + 1)# = (m + 1 + m)#

Tactic:
by rw [add_right_comm]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
have : 2 ≤ ⌊b⌋₊ := Nat.le_floor hb

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

Goal state before:
pp: case e'_11
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
⊢ Set.Ioi 0.5 = ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1

Tactic:
ext x

Goal state after:
case e'_11
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✝
x : ℝ
⊢ x ∈ Set.Ioi 0.5 ↔ x ∈ ⇑(2 • LinearMap.id) ⁻¹' Set.Ioi 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℕ
hne : q ≠ p
left✝ : q < 2 * k + 2
hq_prime : Nat.Prime q
right✝ : q - 1 ∣ 2 * k
⊢ (1 / ↑q).den = q

Tactic:
simp [hq_prime.ne_zero]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2.inl
n p : ℕ
hp : Prime p
this✝ : 1 < p
h✝ : p ≤ n
this : p ^ log p n ≤ n
⊢ log p n ≤ (id (p ^ log p n)).factorization p

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
⊢ ∑ p ∈ primesLE 0, ↑(Nat.log p 0) * log ↑p ≤ ∑ _x ∈ primesLE 0, log ↑0

case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ p ∈ n.primesLE, ↑(Nat.log p n) * log ↑p ≤ ∑ _x ∈ n.primesLE, log ↑n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
⊢ ∃ y, ↑y = bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p

Tactic:
refine ⟨_, Rat.coe_int_num_of_den_eq_one ?_⟩

Goal state after:
case inr
k : ℕ
hk : k > 0
⊢ (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den = 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a + -↑b
⊢ ↑p ^ n ∣ a - b

Tactic:
← sub_eq_add_neg,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - ↑b
⊢ ↑p ^ n ∣ a - b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case hy₂
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ↑(n % p + p * (n / p)) - ↑(n % p) ∈ maximalIdeal ℤ_[p]

Tactic:
· simp [maximalIdeal_eq_span_p, Ideal.mem_span_singleton]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ RingHom.ker toZMod = maximalIdeal ℤ_[p]

Tactic:
ext x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
apply monotone_nat_of_le_succ
  intro n
  dsimp [appr]
  split_ifs; · rfl
  apply Nat.le_add_right

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (∫ (x : ℝ) in 2..√x, 1 / log x ^ 2) + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

pp: case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume 2 √x

pp: case hbc
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume (√x) x

Tactic:
· grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
      integral_1_div_log_sq_le sqrt_le_x (by linarith)]
    rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]
    norm_num
    gcongr <;> linarith

Goal state after:
case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume 2 √x

case hbc
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume (√x) x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}

Tactic:
ext x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) = RingHom.ker (toZModPow m)

Tactic:
ext x

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ x ∈ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) ↔ x ∈ RingHom.ker (toZModPow m)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ discr K ≠ 0

Tactic:
rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]
  exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: case e_a.inl
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
hunit : IsUnit r
hp : r = 1
⊢ (algebraMap ℤ ℚ) 1 = (algebraMap ℤ ℚ) r ^ 2

Tactic:
simp [hp]

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

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝) (zeta n K L) = μ

Tactic:
nth_rewrite 4 [← hζ.powerBasis_gen K]

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n
h : ∃ i < n, zeta n K L ^ i = μ
pf✝¹ : h.choose.Coprime n
hμ : IsPrimitiveRoot (zeta n K L ^ (↑(ZMod.unitOfCoprime h.choose pf✝¹)).val) n
pf✝ : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K hμ).gen
⊢ ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K hμ) pf✝)
      (IsPrimitiveRoot.powerBasis K hζ).gen =
    μ
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : (b'.toMatrix ⇑b).det ^ 2 = 1
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
rw [this, one_mul]

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

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

Tactic:
rwa [add_def]

Goal state after:
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)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (φ (p ^ 0) / 2) * ↑p ^ (p ^ (0 - 1) * ((p - 1) * 0 - 1))

Tactic:
simp only [coe_basis, _root_.pow_zero, powerBasis_gen _ hζ, totient_one, mul_zero,
      show 1 / 2 = 0 by rfl, discr, traceMatrix]
    have hζone : ζ = 1 := by simpa using hζ
    rw [hζ.powerBasis_dim _, hζone, ← (algebraMap K L).map_one,
      minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
    simp only [map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]
    rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
    simp

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
xn_succ_succ

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(2 * a * xn a1 (n + 1)) = ↑(2 * a * xn a1 (n + 1))
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:
← pow_one 2

Goal state after:
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 ^ 1
⊢ p = 2
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : 2 ^ (k + 1) = 2
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))

Tactic:
← pow_one 2

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
k : ℕ
hp : Fact (Nat.Prime 2)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hk : 2 ^ (k + 1) = 2 ^ 1
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (2 ^ (k + 1)) / 2) * ↑2 ^ (2 ^ (k + 1 - 1) * ((2 - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
rwa [add_def]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h1 : d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j = xn a1 n * xn a1 n * xn a1 j
h2 : d a1 * yn a1 n * yn a1 n + 1 = xn a1 n * xn a1 n
⊢ xn a1 n ∣ xn a1 n * (xn a1 n * xn a1 j)

Tactic:
exact dvd_mul_right _ _

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + d a1 * yn a1 0
⊢ a = 2 ∧ 0 = 0

Tactic:
simp at h

Goal state after:
case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case e_a
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
⊢ ((f v ::ₒ v) ∘ none :: some) = f v :: v

Tactic:
ext x

Goal state after:
case e_a
n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
f : Vector3 ℕ n → ℕ
df : DiophFn f
v : Fin2 n → ℕ
x : Fin2 (n + 1)
⊢ ((f v ::ₒ v) ∘ none :: some) x = (f v :: v) x
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∘ (id ⊗ elim0) = v ⊗ fun i ↦ f i v

Tactic:
ext x

Goal state after:
α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
x : α ⊕ Fin2 0
⊢ (v ∘ (id ⊗ elim0)) x = (v ⊗ fun i ↦ f i v) x
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
⊢ (f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr) = v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr

Tactic:
ext x

Goal state after:
α : Type
n : ℕ
S : Set (α ⊕ Fin2 n.succ → ℕ)
d : Dioph S
f✝ : Vector3 ((α → ℕ) → ℕ) n.succ
f : (α → ℕ) → ℕ
fl : Vector3 ((α → ℕ) → ℕ) n
df : DiophFn f
dfl : VectorAllP DiophFn fl
v : α ⊕ Fin2 n → ℕ
x : α ⊕ Fin2 (n + 1)
⊢ ((f (v ∘ inl) ::ₒ v) ∘ (some ∘ inl ⊗ none :: some ∘ inr)) x = (v ∘ inl ⊗ f (v ∘ inl) :: v ∘ inr) x
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow

Tactic:
mem_factoredNumbers'

Goal state after:
n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow
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 : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ

Tactic:
refine LE.le.trans ?_ h.le

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑ p ∈ divisorsAntidiagonal 0, term f s p.1 * term g s p.2

case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p ↦ p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
f g : ℕ → ℂ
s : ℂ
⊢ term (f ⍟ g) s 0 = ∑' (b : ↑((fun p ↦ p.1 * p.2) ⁻¹' {0})), term f s (↑b).1 * term g s (↑b).2

case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑((fun p ↦ p.1 * p.2) ⁻¹' {n})), term f s (↑b).1 * term g s (↑b).2
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
s : ℂ
⊢ HasDerivAt (fun z ↦ term f z n) (-term (logMul f) s n) s

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
f : ℕ → ℂ
s : ℂ
⊢ HasDerivAt (fun z ↦ term f z 0) (-term (logMul f) s 0) s

case inr
f : ℕ → ℂ
n : ℕ
s : ℂ
hn : n ≠ 0
⊢ HasDerivAt (fun z ↦ term f z n) (-term (logMul f) s n) s
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_eq_add_neg,

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₁ : ↑u - 1 / 2 < ↑u - 1
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
this : Tendsto (fun n ↦ ‖jacobiTheta₂_term (↑n) z τ‖) atTop atTop
⊢ False

Tactic:
replace h := (h.comp_injective (fun a b ↦ Int.ofNat_inj.mp)).tendsto_atTop_zero.norm
        exact atTop_neBot.ne (disjoint_self.mp <| h.disjoint (disjoint_nhds_atTop _) this)

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

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 - s - ↑P.k)
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

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

Tactic:
by
  refine tsum_of_norm_bounded ?_ (f_le_g_nat 1 ha ht)
  unfold g_nat
  simp_rw [pow_one, add_mul]
  apply HasSum.add
  · have h0' : ‖rexp (-π * t)‖ < 1 := by
      simpa only [norm_eq_abs, abs_exp] using exp_lt_aux ht
    convert! (hasSum_coe_mul_geometric_of_norm_lt_one h0').mul_left (exp (-π * a ^ 2 * t)) using 1
    · ext1 n
      rw [mul_comm (exp _), ← Real.exp_nat_mul, mul_assoc (n : ℝ), ← Real.exp_add]
      ring_nf
    · rw [mul_add, add_mul, mul_one, exp_add, mul_div_assoc]
  · convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1
    ext1 n
    rw [← Real.exp_nat_mul, mul_assoc _ (exp _), ← Real.exp_add]
    ring_nf

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

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

Tactic:
· intro hτ
    refine ((summable_pow_mul_jacobiTheta₂_term_bound
      |z.im| hτ 2).mul_left (3 * π)).of_norm_bounded (fun n ↦ ?_)
    refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)
    simp_rw [mul_assoc (3 * π)]
    refine mul_le_mul_of_nonneg_left ?_ (mul_pos (by simp : 0 < (3 : ℝ)) pi_pos).le
    refine mul_le_mul_of_nonneg_left ?_ (pow_nonneg (Int.cast_nonneg (abs_nonneg _)) _)
    exact norm_jacobiTheta₂_term_le hτ le_rfl le_rfl n

Goal state after:
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
⊢ -1 < (s - ↑P.k - 1).re

Tactic:
simpa using hs

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

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

pp: case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖

Tactic:
· simp only [f_int, f_nat, Int.ofNat_eq_natCast, Int.cast_natCast, norm_mul, norm_eq_abs, abs_pow,
      abs_abs]

Goal state after:
case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖
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 : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - 1 + -↑P.k) • P.g₀ = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
← sub_eq_add_neg,

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
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - 1 - ↑P.k) • P.g₀ = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
div_add' _ _ _ two_pi_I_ne_zero,

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