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

Goal state before:
pp: case hg.hf
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := ⋯
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
⊢ ConvexOn ℝ (Set.Ioi 0.5) fun x ↦ x

Tactic:
· exact convexOn_id (convex_Ioi (0.5 : ℝ))

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ (vonStaudtPrimes k).erase p, 1 / ↑q

Tactic:
Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2

Goal state after:
case neg
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ vonStaudtPrimes k, 1 / ↑q
Module: Mathlib.NumberTheory.Chebyshev

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

pp: case refine_2.inr
n p : ℕ
hp : Prime p
this : 1 < p
h : n < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p

Tactic:
· have := pow_log_le_self p (x := n) (by linarith)
    grw [← le_sup (b := p ^ p.log n) (by grind)]
    simp [hp]

Goal state after:
case refine_2.inr
n p : ℕ
hp : Prime p
this : 1 < p
h : n < p
⊢ log p n ≤ (Icc 1 n).sup fun a ↦ (id a).factorization p
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ψ ↑n = ∑ m ∈ Icc 1 n, Λ m

Tactic:
simp [psi, ← Icc_add_one_left_eq_Ioc]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
let a : ℕ → ℝ := Set.indicator (Set.ofPred Nat.Prime) (fun n ↦ log n)

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
⊢ χ₀ n (g * h) = χ₀ n g * χ₀ n h

Tactic:
refine (toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm
  change g (h (ζ : Lˣ)) = _
  rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul,
    ← Subgroup.coe_pow]
  congr 2
  norm_cast
  simp only [pow_eq_pow_iff_modEq, ← ZMod.natCast_eq_natCast_iff,
    ZMod.natCast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) (orderOf_dvd_natCard _)]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log ↑p + if ↑p ≤ √x then log √x else 0) ≤ log 4 * x + √x * log √x

Tactic:
← theta_le_log4_mul_x (by positivity)

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log ↑p + if ↑p ≤ √x then log √x else 0) ≤ θ x + √x * log √x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
i : ℕ
hik : k + i ≥ k
⊢ ↑(p ^ k) ∣ f (k + i) - f k

Tactic:
clear hik

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
i : ℕ
⊢ ↑(p ^ k) ∣ f (k + i) - f k
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_3.e'_5
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ (-1) ^ ((p - 1) / 2) = (-1) ^ (φ p / 2)

Tactic:
totient_prime hp.out

Goal state after:
case e'_3.e'_5
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (cyclotomic p K)
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} K L
hζ' : IsPrimitiveRoot ζ (p ^ (0 + 1))
⊢ (-1) ^ ((p - 1) / 2) = (-1) ^ ((p - 1) / 2)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ x ::ₒ v ∈ {v | (v ∘ none :: some) ∈ S} ↔ (x :: v) ∈ S

Tactic:
dsimp
      rw [show Option.elim' x v ∘ cons none some = x :: v from
          funext fun s => by rcases s with a | b <;> rfl]

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

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

Tactic:
refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_mul_le ..) ?_

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

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

Tactic:
by
  obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
    simpa [abscissaOfAbsConv, sInf_lt_iff] using hs
  exact hy.of_re_le_re <| ofReal_re y ▸ hys.le

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

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ (x + 1 - 1)
H : ↑x + 1 < abscissaOfAbsConv f
y : ℝ
hy₁ : ↑x + 1 < ↑y
hy₂ : ↑y < abscissaOfAbsConv f
⊢ False

Tactic:
exact (LSeriesSummable_of_isBigO_rpow (s := y) (EReal.coe_lt_coe_iff.mp hy₁) h
    |>.abscissaOfAbsConv_le.trans_lt hy₂).false

Goal state after:
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
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]
ky : k ≤ 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])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
this : i % (4 * yn a1 i) = k % (4 * yn a1 i)
⊢ i = k

Tactic:
Nat.mod_eq_of_lt (lt_of_le_of_lt (Nat.le_add_left _ _) ki),

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
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]
ky : k ≤ 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])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
this : i = k % (4 * yn a1 i)
⊢ i = k
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 * ↑u' - (1 + ↑u') / ↑v

Tactic:
rw [sub_le_sub_iff_left, div_le_one Hv, add_comm]

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
⊢ ↑u' + 1 ≤ ↑v
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_3
t : ℝ
ht : 0 < t
⊢ ∑' (b : ℕ), f_nat 0 0 t (b + 1) = F_nat 0 1 t

Tactic:
simp_rw [F_nat, f_nat, Nat.cast_add, Nat.cast_one, add_zero]

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

Goal state before:
pp: case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ ∃ p, 0 < p ∧ (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-p * t)

Tactic:
refine ⟨_, pi_pos, this.trans ?_⟩

Goal state after:
case pos
a : ℝ
ha : 0 ≤ a
h : a = 0
this : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))
⊢ (fun t ↦ rexp (-π * t) / (1 - rexp (-π * t))) =O[atTop] fun t ↦ rexp (-π * t)
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
⊢ (((Ioi 1).indicator fun x ↦ P.f x - P.f₀) + (Ioo 0 1).indicator fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (((Ioo 0 1).indicator fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) + {1}.indicator fun x ↦ P.f₀ - P.f 1) x

Tactic:
Pi.add_apply

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
⊢ (Ioi 1).indicator (fun x ↦ P.f x - P.f₀) x + (Ioo 0 1).indicator (fun x ↦ P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x -
        P.f x +
      P.f₀ =
    (Ioo 0 1).indicator (fun x ↦ P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀) x + {1}.indicator (fun x ↦ P.f₀ - P.f 1) x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term_fderiv n z τ‖ ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))

Tactic:
refine (norm_jacobiTheta₂_term_fderiv_le n z τ).trans
      (?_ : 3 * π * |n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ _)

Goal state after:
case mpr
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
⊢ 3 * π * ↑|n| ^ 2 * ‖jacobiTheta₂_term n z τ‖ ≤ 3 * π * (↑|n| ^ 2 * rexp (-π * (τ.im * ↑n ^ 2 - 2 * |z.im| * ↑|n|)))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ f_int k a t (Int.ofNat n) = f_nat k a t n

Tactic:
f_int,

Goal state after:
k : ℕ
a : ℝ
ha : 0 ≤ a
t : ℝ
n : ℕ
⊢ |↑(Int.ofNat n) + a| ^ k * rexp (-π * (↑(Int.ofNat n) + a) ^ 2 * t) = f_nat k a t n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ f_int k a t (Int.negSucc n) = f_nat k (1 - a) t n

Tactic:
f_int,

Goal state after:
k : ℕ
a : ℝ
ha : a ≤ 1
t : ℝ
n : ℕ
this : ↑(Int.negSucc n) + a = -(↑n + (1 - a))
⊢ |↑(Int.negSucc n) + a| ^ k * rexp (-π * (↑(Int.negSucc n) + a) ^ 2 * t) = f_nat k (1 - a) t n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl.hx
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx

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
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (1 / s) • P.f₀) (𝓝 ↑P.k) (𝓝 0)

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] ↑P.k) (𝓝 (-P.ε • P.g₀))

Tactic:
· rw [(by simp : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • P.f₀))]
    refine (continuous_sub_right _).continuousAt.smul (ContinuousAt.smul ?_ continuousAt_const)
    have := ofReal_ne_zero.mpr P.hk.ne'
    fun_prop

Goal state after:
case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ (s - ↑P.k) • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] ↑P.k) (𝓝 (-P.ε • P.g₀))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂ z τ) = jacobiTheta₂ ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
by
  rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]
  congr 2 with n
  simp only [jacobiTheta₂_term, mul_neg, ← exp_conj, map_add, map_neg, map_mul, map_ofNat,
    conj_ofReal, conj_I, map_intCast, neg_mul, neg_neg, map_pow]

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

Goal state before:
pp: s : ℂ
⊢ I = 0 ∨ sinZeta 0 s = 0

Tactic:
eq_false_intro I_ne_zero,

Goal state after:
s : ℂ
⊢ False ∨ sinZeta 0 s = 0
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n : ℕ
χ : DirichletCharacter ℂ n
⊢ (fun n_1 ↦ χ ↑n_1) ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ

Tactic:
have : (1 : ℕ → ℂ) ⍟ (μ ·) = δ := by
    rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
    simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
  nth_rewrite 1 [← mul_one ↗χ]
  simpa only [mul_convolution_distrib χ 1 ↗μ, this] using mul_delta _

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (completedCosZeta (↑a) s)

Tactic:
have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by
    rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)]
  have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg
  rw [aux, div_zero, zero_div, add_zero] at hint
  refine hint.congr_fun fun n ↦ ?_
  split_ifs with h
  · simp only [h, Nat.cast_zero, aux, div_zero, zero_div, neg_zero, zero_add]
  · simp only [ofReal_cos, ofReal_mul, ofReal_ofNat, ofReal_natCast, Complex.cos,
      show 2 * π * a * n * I = 2 * π * I * a * n by ring, neg_mul, mul_div_assoc,
      div_right_comm _ (2 : ℂ), Int.cast_natCast, Nat.abs_cast, Int.cast_neg, mul_neg, abs_neg, ←
      mul_add, ← add_div]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0

Tactic:
exact right_ne_zero_of_mul f42.1

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 < c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

pp: case inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

pp: case inr.inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
· use a0, b0, c0

Goal state after:
case inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

case inr.inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
⊢ ¬m = -i ^ 2

Tactic:
by_contra h1

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
h1 : m = -i ^ 2
⊢ False
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
⊢ ¬r * s = -d ^ 2

Tactic:
by_contra h1

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Real.log (cexp (∑' (n : ℕ), ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ ↑s)).re = ∑' (n : ℕ), Λ n / (↑n ^ s * Real.log ↑n)

Tactic:
convert Real.log_exp _

Goal state after:
case e'_2
s : ℝ
hs : 1 < s
⊢ (cexp (∑' (n : ℕ), ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ ↑s)).re = rexp (∑' (n : ℕ), Λ n / (↑n ^ s * Real.log ↑n))
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
⊢ (↑↑ψ).toFun = ⇑K.subtype

Tactic:
let ψ₁ := RingHom.comp extψ (RingHom.comp j.symm.toRingHom ofRealHom.rangeRestrictField)

Goal state after:
case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
⊢ (↑↑ψ).toFun = ⇑K.subtype
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(algebraMap ℤ ℚ) (b.toMatrix (Subtype.val ∘ ⇑bI.num)).det| / |↑((Algebra.norm ℤ) ↑I.den)|

Tactic:
rw [RingHom.map_det, show RingHom.mapMatrix (algebraMap ℤ ℚ) (b.toMatrix ((↑) ∘ bI.num)) =
      b₀.toMatrix ((algebraMap R K (den I : R)) • ((↑) ∘ bI)) by
    ext : 2
    simp_rw [bI.num, RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
      ← Basis.localizationLocalization_repr_algebraMap ℚ ℤ⁰ K, Function.comp_apply,
      Basis.map_apply, LinearEquiv.restrictScalars_apply, equivNum_apply, Submonoid.smul_def,
      Algebra.smul_def]
    rfl]

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(b₀.toMatrix ((algebraMap R K) ↑I.den • Subtype.val ∘ ⇑bI)).det| / |↑((Algebra.norm ℤ) ↑I.den)|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖

Tactic:
· rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]

Goal state after: