mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * (↑p * u) * (↑p * v) ∣ ↑p ^ p * u ^ p

Tactic:
simp only [← mul_assoc]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * ↑p * u * ↑p * v ∣ ↑p ^ p * u ^ p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ IsCyclic (ZMod n)ˣ ↔
    (∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1) ∨ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1

Tactic:
rw [isCyclic_units_iff_of_odd hn, or_iff_left]

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1

case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ ¬∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = 2 * x ^ x_1
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: m n : ℕ
h : n ≤ m
p : ℕ
hp : p ∈ Ico (m + 1) (m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m

Tactic:
mem_Ico

Goal state after:
m n : ℕ
h : n ≤ m
p : ℕ
hp : (m + 1 ≤ p ∧ p < m + n + 1) ∧ Nat.Prime p
⊢ p ∣ (m + n).choose m
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
n : ℕ
⊢ ∑ k ∈ range (n + 1 + 1), ↑((n + 1 + 1).choose k) * bernoulli k = if n + 1 + 1 = 1 then 1 else 0

Tactic:
suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring

Goal state after:
case succ.succ
n : ℕ
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) +
        ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1) +
      ↑(n.succ.succ.choose 0) * bernoulli' 0 =
    ↑n + 1 + 1
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2

Tactic:
← eq_sub_iff_add_eq

Goal state after:
case succ.succ
n : ℕ
f :
  ∑ k ∈ range n, ↑(n.succ.succ.choose (k + 1 + 1)) * bernoulli' (k + 1 + 1) =
    ↑n + 1 + 1 - ↑(n.succ.succ.choose 0) * bernoulli' 0 - ↑(n.succ.succ.choose (0 + 1)) * bernoulli' (0 + 1)
⊢ ∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = ↑n / 2
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
⊢ 512 ≤ ↑n

Tactic:
by exact_mod_cast n_large

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (2 * ↑n) ^ ↑(2 * n).sqrt * 4 ^ ↑(2 * n / 3) ≤ 4 ^ ↑n

Tactic:
refine _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))

Goal state after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (2 * ↑n) ^ ↑(2 * n).sqrt * 4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ √(2 * ↑n) * 4 ^ (2 * ↑n / 3)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)

Tactic:
rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia), mul_right_comm _ x, mul_right_comm _ x]

Goal state after:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ↑((2 * k + 1).choose (2 * m)) * (2 * ↑k - 2 * ↑m + 1) * x = ↑((2 * k).choose (2 * m)) * (2 * ↑k + 1) * x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 ≤ ↑x✝¹

Tactic:
aesop

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
h₀ : θ x = 0
contra : 2 ∈ Ioc 0 ⌊x⌋₊
p : ℕ
hp : p ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 ≤ ↑p

Tactic:
aesop

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
rw [theta_eq_log_primorial]
  trans log (4 ^ ⌊x⌋₊)
  · gcongr <;> norm_cast
    exacts [primorial_pos _, primorial_le_four_pow _]
  rw [Real.log_pow, mul_comm]
  gcongr
  exact floor_le hx

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto ∣ n !

Tactic:
by
  simp +contextual [lcmUpto, dvd_factorial, Order.one_le_iff_pos]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n p : ℕ
hp : p ∈ n.primesLE
⊢ ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q = ∑ k ∈ Icc 1 (Nat.log p n), Λ (p ^ k)

Tactic:
exact sum_image fun a _ b _ hab ↦ Nat.pow_right_injective (two_le_of_mem_primesLE hp) hab

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑(⌊log x / log 2⌋₊ - 1) ≤ log x / log 2

Tactic:
rw [cast_sub]

Goal state after:
case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑⌊log x / log 2⌋₊ - ↑1 ≤ log x / log 2

case hbc
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log ↑n)⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
rw [sum_mul_eq_sub_integral_mul₁ a (f := fun n ↦ (log n)⁻¹) (by simp [a]) (by simp [a]),
    ← intervalIntegral.integral_of_le hx]

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv (fun n ↦ (log n)⁻¹) x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
rw [cast_add]

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

Goal state before:
pp: a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / log x ^ 2 ≤ ∫ (x : ℝ) in a..b, 1 / log a ^ 2

Tactic:
by
      refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound
      apply intervalIntegrable_one_div_log_sq <;> linarith

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

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑(↑t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))

Tactic:
← Subgroup.coe_zpow

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0

Tactic:
simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = 0 ↔ (toZModPow m) x = 0
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ g ↑t = ↑t ^ ((ZMod.ringEquivCongr ⋯) c).val

Tactic:
hc t ht,

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Nat.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ ↑t ^ c.val = ↑t ^ ((ZMod.ringEquivCongr ⋯) c).val
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1

Tactic:
refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Goal state after:
case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n✝ : ℕ
inst✝¹ : NeZero n✝
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (cyclotomicCharacter.toFun p 1) = (PadicInt.toZModPow n) 1
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_

Goal state after:
case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n✝ : ℕ
inst✝¹ : NeZero n✝
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
n : ℕ
⊢ (PadicInt.toZModPow n) (cyclotomicCharacter.toFun p (f * g)) =
    (PadicInt.toZModPow n) (cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g)
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ Algebra.discr ℚ ⇑(integralBasis K) = ↑(discr L)

Tactic:
Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = ↑(discr L)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖(lift f_compat) r - g r‖ ≤ ↑p ^ (-↑n)

Tactic:
norm_le_pow_iff_mem_span_pow,

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ (lift f_compat) r - g r ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯) z = z

Tactic:
change _ = RingHom.id _ z
  rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
  intro; rw [RingHom.comp_id]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case neg
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
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
hji : ¬j = i
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥

Tactic:
simp only [updateCol_apply, hji, PowerBasis.coe_basis]
    exact mem_bot.2
      (IsIntegrallyClosed.isIntegral_iff.1 <| isIntegral_trace <| (hint.pow _).mul (hint.pow _))

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

Goal state before:
pp: d : ℤ
x : ℤ√d
h : x.norm.natAbs = 1
hx : x.norm ≤ 0
⊢ 1 = x * -star x

Tactic:
by
            rwa [← Int.natCast_inj, Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
              Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h

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

Goal state before:
pp: ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
let D := Icc (0 : ℤ) n

Goal state after:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : a ≠ 1
⊢ ∑ χ, χ a = 0

Tactic:
by
  obtain ⟨χ, hχ⟩ := exists_apply_ne_one_of_hasEnoughRootsOfUnity R ha
  refine eq_zero_of_mul_eq_self_left hχ ?_
  simp only [Finset.mul_sum, ← MulChar.mul_apply]
  exact Fintype.sum_bijective _ (Group.mulLeft_bijective χ) _ _ fun χ' ↦ rfl

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

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

Tactic:
lt_div_iff₀ (mul_pos hv₀ hv₀'),

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

Goal state before:
pp: p n : ℕ
hp : Prime p
hn : n ∈ p.smoothNumbers
⊢ p.Coprime n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers] at hn

Goal state after:
p n : ℕ
hp : Prime p
hn : n ∈ factoredNumbers (Finset.range p)
⊢ p.Coprime n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) < 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
← add_lt_add_iff_right (v * (2 * v - 1) : ℝ),

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < 1 + ↑v * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
⊢ ∀ (p : ↑((fun p ↦ p.1 * p.2) ⁻¹' {0})), term f s (↑p).1 * term g s (↑p).2 = 0

Tactic:
rintro ⟨⟨_, _⟩, hp⟩

Goal state after:
f g : ℕ → ℂ
s : ℂ
hS : (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}
fst✝ snd✝ : ℕ
hp : (fst✝, snd✝) ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0}
⊢ term f s (↑⟨(fst✝, snd✝), hp⟩).1 * term g s (↑⟨(fst✝, snd✝), hp⟩).2 = 0
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v

Tactic:
exact h.1

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₀ : Summable (fun n ↦ ‖term f x n‖) := summable_norm_iff.mpr hf

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h
    have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'
    have huv₁' : (u - ⌊ξ⌋ * v).toNat < v := by zify; rwa [toNat_of_nonneg huv₀.le]
    have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
      (toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h
    obtain ⟨n, hn⟩ := ih (u - ⌊ξ⌋ * v).toNat huv₁' inv
    use n + 1
    rw [convergent_succ, ← hn,
      (mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
      cast_natCast, inv_div, sub_div, mul_div_cancel_right₀ _ Hv, add_sub_cancel]

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

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

Tactic:
unfold g_nat

Goal state after:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ (↑n + a) ^ 1 * rexp (-π * (↑n + a ^ 2) * t))
    (rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))
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 * π * ↑|n|)

Tactic:
← mul_assoc _ (2 * π),

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 * π) * ↑|n|
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
eq_false_intro (by linarith [ha.2] : 1 - a ≠ 0),

Goal state after:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t ↦ F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t ↦ F_nat 0 (1 - a) t - if False then 1 else 0) =O[atTop] fun t ↦ rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)

Tactic:
have hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n := by
    refine fun n p hp ↦ (norm_jacobiTheta₂_term_fderiv_le n p.1 p.2).trans ?_
    refine mul_le_mul_of_nonneg_left ?_ (by positivity)
    exact norm_jacobiTheta₂_term_le hT (le_of_lt hp.1) (le_of_lt hp.2) n

Goal state after:
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
hVmem : (z, τ) ∈ V
hVp : IsPreconnected V
f : ℤ → ℂ × ℂ → ℂ := fun n p ↦ jacobiTheta₂_term n p.1 p.2
f' : ℤ → ℂ × ℂ → ℂ × ℂ →L[ℂ] ℂ := fun n p ↦ jacobiTheta₂_term_fderiv n p.1 p.2
hf : ∀ (n : ℤ), ∀ p ∈ V, HasFDerivAt (f n) (f' n p) p
u : ℤ → ℝ := fun n ↦ 3 * π * ↑|n| ^ 2 * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
hu : ∀ (n : ℤ), ∀ x ∈ V, ‖f' n x‖ ≤ u n
⊢ HasFDerivAt (fun p ↦ jacobiTheta₂ p.1 p.2) (jacobiTheta₂_fderiv z τ) (z, τ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1)

Tactic:
simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]

Goal state after:
a : UnitAddCircle
⊢ Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s + (s - 1) * hurwitzZetaOdd a s) (𝓝[≠] 1)
    (𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rw [jacobiTheta₂'_undef z hτ, jacobiTheta₂'_undef, jacobiTheta₂_undef, mul_zero,
      sub_zero, mul_zero] <;>
    rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Goal state after:
case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * riemannZeta s =
    2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * hurwitzZetaEven 0 s

Tactic:
hurwitzZetaEven_zero

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * riemannZeta s =
    2 * (2 * ↑π) ^ (-s) * Gamma s * cos (↑π * s / 2) * riemannZeta s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
this : DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ - 1 / (s - 1) / s.Gammaℝ) 1
x : ℂ
hx : x ≠ 0
⊢ hurwitzZetaEven a x - 1 / (x - 1) / x.Gammaℝ = completedHurwitzZetaEven a x / x.Gammaℝ - 1 / (x - 1) / x.Gammaℝ

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne hx]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
⊢ (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)).1 ^ 2 + (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)).2 ^ 2 = 1

Tactic:
field [hk x]

Goal state after: