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

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

Tactic:
cases n with | zero => simp | succ n =>
  suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn : Squarefree n
this : ∏ p ∈ n.primeFactors, p ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#

Tactic:
Nat.prod_primeFactors_of_squarefree hn

Goal state after:
n : ℕ
hn : Squarefree n
this : n ∣ ∏ p ∈ range (n + 1) with Nat.Prime p, p
⊢ n ∣ n#
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case e'_2.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

pp: case e'_3.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
m : ℕ
hf_diff : ∀ t ∈ Set.Icc 1 ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 ↑m) volume
⊢ m = ⌊↑m⌋₊

Tactic:
all_goals rw [Nat.floor_natCast]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
        ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))

Goal state after:
case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x ∈ range (n + 1),
      (PowerSeries.coeff x) (PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) *
        ((PowerSeries.coeff (n + 1 - x)) (exp A) - (PowerSeries.coeff (n + 1 - x)) 1) =
    t ^ n * (algebraMap ℚ A) (1 / ↑n !)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! * (↑n ^ (q - m + 1) * (↑(q - m + 1)!)⁻¹)

Tactic:
mul_comm ((n : ℚ) ^ (q - m + 1)),

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
m : ℕ
h✝ : m ∈ range q.succ
h : m < q + 1
⊢ bernoulli m * ↑((q + 1)! / (m ! * (q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / ↑m ! * ((↑(q - m + 1)!)⁻¹ * ↑n ^ (q - m + 1))
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ f ↑x✝ * ∑ k ∈ Icc 0 x✝, c k - ∫ (t : ℝ) in Set.Ioc 1 ↑x✝, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k =
    ∑ k ∈ Icc 0 x✝, f ↑k * c k

Tactic:
rw [sum_mul_eq_sub_integral_mul₀' _ hc _ (fun t ht ↦ hf_diff _ ht.1)]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 1) volume
l : 𝕜
h_lim : Tendsto (fun n ↦ f ↑n * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → ℝ
hg_dom : (fun t ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =O[atTop] g
hg_int : IntegrableAtFilter g atTop volume
h :
  (fun n ↦ ∫ (x : ℝ) in 1..↑n, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) =ᶠ[atTop] fun n ↦
    ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
h_lim' :
  Tendsto (fun n ↦ ∫ (t : ℝ) in Set.Ioc 1 ↑n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) atTop
    (𝓝 (∫ (t : ℝ) in Set.Ioi 1, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x✝ : ℕ
⊢ IntegrableOn (deriv f) (Set.Icc 1 ↑x✝) volume
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
i : ℕ
x✝ : i ∈ range p
⊢ bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)

Tactic:
by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]

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

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
⊢ (M ^ n).succ ≤ {x | t x = s}.toList.length

Tactic:
Finset.length_toList

Goal state after:
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
⊢ (M ^ n).succ ≤ {x | t x = s}.card
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
have hj : natDegree b - j.succ < d := by
    by_cases! hd : natDegree b < d
    · exact lt_of_le_of_lt tsub_le_self hd
    · have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
      rwa [tsub_lt_iff_tsub_lt hd hbj] at this

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

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

Tactic:
simpa using hbε

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℤ
hzn : 0 ≤ n
hnp : n < ↑p
hn : ‖⟨↑r, H⟩ - ↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1

Tactic:
lift n to ℕ using hzn

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖⟨↑r, H⟩ - ↑↑n‖ < 1
⊢ ∃ n < p, ‖x - ↑n‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
⊢ IntervalIntegrable (fun x ↦ 1 / log x ^ 2) volume a b

Tactic:
refine ContinuousOn.intervalIntegrable fun x hx ↦ ContinuousAt.continuousWithinAt ?_

Goal state after:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : x ∈ Set.uIcc a b
⊢ ContinuousAt (fun x ↦ 1 / log x ^ 2) x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2|

Tactic:
intervalIntegral.integral_const_mul,

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ log 4 * ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2|
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
· simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
      rw [unitCoeff_spec hc']
      exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _

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

Goal state before:
pp: case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}

pp: case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
· exact isClosed_closure

Goal state after:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ⊢ discr ℚ = 1

Tactic:
by
  let b : Basis (Fin 1) ℤ (𝓞 ℚ) :=
    Basis.map (Basis.singleton (Fin 1) ℤ) ringOfIntegersEquiv.toAddEquiv.toIntLinearEquiv.symm
  calc NumberField.discr ℚ
    _ = Algebra.discr ℤ b := by convert! (discr_eq_discr ℚ b).symm
    _ = Algebra.trace ℤ (𝓞 ℚ) (b default * b default) := by
      rw [Algebra.discr_def, Matrix.det_unique, Algebra.traceMatrix_apply, Algebra.traceForm_apply]
    _ = Algebra.trace ℤ (𝓞 ℚ) 1 := by
      rw [Basis.map_apply, RingEquiv.toAddEquiv_eq_coe, ← AddEquiv.toIntLinearEquiv_symm,
        AddEquiv.coe_toIntLinearEquiv, Basis.singleton_apply,
        show (AddEquiv.symm ↑ringOfIntegersEquiv) (1 : ℤ) = ringOfIntegersEquiv.symm 1 by rfl,
        map_one, mul_one]
    _ = 1 := by rw [Algebra.trace_eq_matrix_trace b]; simp

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

Goal state before:
pp: ι : 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)
⊢ 1 * discr ℚ ⇑b = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2 * discr ℚ (⇑b ∘ ⇑(b.indexEquiv b').symm)

Tactic:
discr_reindex

Goal state after:
ι : 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)
⊢ 1 * discr ℚ ⇑b = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det ^ 2 * discr ℚ ⇑b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

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

Tactic:
· dsimp only at h
      exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro y (by simp [add_comm, *])))

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

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ x) ⊗ t) s

Tactic:
by rcases s with a | b <;> try { cases a <;> rfl }; rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
s : (α ⊕ β) ⊕ γ
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) s = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) s

Tactic:
by rcases s with a | b <;> try { cases a <;> rfl }; rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
s : Option α ⊕ β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) s = (t none ::ₒ v ⊗ t ∘ some) s

Tactic:
by rcases s with a | b <;> try { cases a <;> rfl }; rfl

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
x : v ∈ f.Dom
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).Dom),
    (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).get h = ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).2

Tactic:
rw [show (f.fn v x ::ₒ v) ∘ some = v from funext fun s => rfl]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
x : v ∈ f.Dom
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p.Coprime n

Tactic:
rw [hp.coprime_iff_not_dvd, ← mem_primeFactorsList_iff_dvd hn.1 hp]
  exact fun H ↦ hs <| hn.2 p H

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ p ^ List.count p m.primeFactorsList * ↑⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩ = m

Tactic:
← prod_replicate,

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p).prod *
      ↑⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩ =
    m
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
p : ℕ
hp : Nat.Prime p
hsum : Summable fun x ↦ ‖f x‖
⊢ (1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e)

Tactic:
simp only [map_pow]
  refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm
  refine Summable.of_norm ?_
  simpa only [Function.comp_def, map_pow]
    using hsum.comp_injective <| Nat.pow_right_injective hp.one_lt

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

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ ↑v + -(1 / 2) < (fract ξ)⁻¹

Tactic:
(by ring : (v : ℝ) + -(1 / 2) = (2 * v - 1) / 2),

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ (2 * ↑v - 1) / 2 < (fract ξ)⁻¹
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hf : Multipliable fun n ↦ f ↑n
⊢ ∏' (p : Primes) (n : ℕ), f (↑p ^ (n + 1)) = ∏' (p : Primes × ℕ), f ↑(prodNatEquiv p)

Tactic:
by
    simpa using (hf.comp_injective prodNatEquiv.injective).tprod_prod.symm

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

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Tactic:
let f : ℂ × ℂ → ℂ := fun p ↦ 2 * π * I * n * p.1 + π * I * n ^ 2 * p.2
  suffices HasFDerivAt f ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ)
    + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ) from this.cexp
  exact (hasFDerivAt_fst.const_mul _).add (hasFDerivAt_snd.const_mul _)

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

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

Tactic:
refine IsBigO.of_bound ‖P.f₀‖ (eventually_nhdsWithin_iff.mpr ?_)
    filter_upwards [eventually_le_nhds zero_lt_one] with x hx' (hx : 0 < x)
    apply le_mul_of_one_le_right (norm_nonneg _)
    rw [norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_neg hx.le]
    exact (one_le_inv₀ (rpow_pos_of_pos hx _)).2 (rpow_le_one hx.le hx' P.hk.le)

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

Goal state before:
pp: n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖

Tactic:
rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, hns,
    mul_comm _ ‖cexp _‖, (by norm_num : (3 : ℝ) = 2 + 1), add_mul, add_mul]

Goal state after:
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ *
      ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤
    ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ * (2 * π * ↑|n| ^ 2 + 1 * π * ↑|n| ^ 2)
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:
norm_I,

Goal state after:
case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * 1 * ‖↑n‖ * ‖ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
norm_I,

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖↑π‖ * 1 * ‖↑n ^ 2‖ * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * ↑|n| ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = π * ‖I‖ * ‖↑n ^ 2‖

Tactic:
norm_I,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = π * 1 * ‖↑n ^ 2‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x

Tactic:
rcases lt_trichotomy 1 x with hx' | rfl | hx'
  · have : 1 / x < 1 := by rwa [one_div_lt hx one_pos, div_one]
    rw [f_modif, Pi.add_apply, indicator_of_notMem (notMem_Ioi.mpr this.le),
      zero_add, indicator_of_mem (mem_Ioo.mpr ⟨div_pos one_pos hx, this⟩), g_modif, Pi.add_apply,
      indicator_of_mem (mem_Ioi.mpr hx'), indicator_of_notMem
      (notMem_Ioo_of_ge hx'.le), add_zero, P.h_feq _ hx, smul_sub]
    simp_rw [rpow_neg (one_div_pos.mpr hx).le, one_div, inv_rpow hx.le, inv_inv]
  · simp [f_modif, g_modif]
  · have : 1 < 1 / x := by rwa [lt_one_div one_pos hx, div_one]
    rw [f_modif, Pi.add_apply, indicator_of_mem (mem_Ioi.mpr this),
      indicator_of_notMem (notMem_Ioo_of_ge this.le), g_modif, Pi.add_apply,
      indicator_of_notMem (notMem_Ioi.mpr hx'.le),
      indicator_of_mem (mem_Ioo.mpr ⟨hx, hx'⟩), P.h_feq _ hx]
    simp_rw [rpow_neg hx.le]
    match_scalars <;> field [(rpow_pos_of_pos hx P.k).ne', P.hε]

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

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * (‖2‖ * ‖↑π‖ * ‖I‖ * ‖↑n‖)

Tactic:
norm_I,

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 ≤ (2 * π)⁻¹ * (‖2‖ * ‖↑π‖ * 1 * ‖↑n‖)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ‖↑π‖ * ‖I‖ * ‖↑n‖ = 2 * π * ↑|n|

Tactic:
norm_I,

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 2 * ‖↑π‖ * 1 * ‖↑n‖ = 2 * π * ↑|n|