mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ 1 + ↑u' ≤ ↑v

Tactic:
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.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto ((fun x ↦ -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x ↦ -1 * ↑x) atTop atBot

Tactic:
← tendsto_neg_atTop_iff,

Goal state after:
S T : ℝ
hT : 0 < T
k : ℕ
⊢ Tendsto (fun x ↦ -((fun x ↦ -π * (T * ↑x ^ 2 - 2 * S * ↑x)) - fun x ↦ -1 * ↑x) x) atTop atTop
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 (t ^ (-1))) (-s) = |(-1)|⁻¹ • mellin P.g (-s / ↑(-1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s

Tactic:
abs_neg,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (t ^ (-1))) (-s) = |1|⁻¹ • mellin P.g (-s / ↑(-1))
⊢ mellin P.f (↑P.k - s) = P.ε • mellin P.g s
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ∫ (x : ℝ) in Ioi 0, ‖↑x ^ (s - 1) * ↑(rexp (-p i * x))‖ ∂volume = Real.Gamma s.re / p i ^ s.re

Tactic:
← this

Goal state after:
case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
⊢ ∫ (x : ℝ) in Ioi 0, ‖↑x ^ (s - 1) * ↑(rexp (-p i * x))‖ ∂volume = ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)

Tactic:
have hp i : a i = 0 ∨ 0 < π * q i := by rcases hq i with h | h <;> simp [h, pi_pos]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
refine one_le_pi_div_two.trans (mul_le_mul_of_nonneg_left ?_ pi_pos.le)

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term_fderiv x z τ
this✝ : Summable fun x ↦ ‖jacobiTheta₂_term_fderiv x z τ‖
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 2⁻¹ ≤ ↑|n| ^ 2
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
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖jacobiTheta₂'_term n z τ‖

Tactic:
rw [jacobiTheta₂'_term, norm_mul, ← mul_assoc]

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂'_term x z τ
this : ∀ᶠ (n : ℤ) in cofinite, n ≠ 0
n : ℤ
hn : n ≠ 0
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ (2 * π)⁻¹ * ‖2 * ↑π * I * ↑n‖ * ‖jacobiTheta₂_term n z τ‖
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))
⊢ |(-(↑n + (1 - a)))| ^ k * rexp (-π * (-(↑n + (1 - a))) ^ 2 * t) =
    (↑n + (1 - a)) ^ k * rexp (-π * (↑n + (1 - a)) ^ 2 * t)

Tactic:
abs_neg,

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

Goal state before:
pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ ↑x ^ (s - 1) • P.f₀) (volume.restrict (Ioc 0 1))

pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))

Tactic:
· apply Integrable.smul_const
      rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
      exact intervalIntegral.intervalIntegrable_cpow' h_re1

Goal state after:
case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ Integrable (fun x ↦ P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀) (volume.restrict (Ioc 0 1))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

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

Goal state before:
pp: x : ℝ
hx : x ≤ 0
z✝ : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

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

Goal state before:
pp: a' x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < (I * ↑x).im

Tactic:
simpa

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t

Tactic:
add_comm

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
t : ℝ
ht₁ : t ≠ 1
ht₀ : 0 < t
ht : t < 1
⊢ ↑t ^ (s - 1) • (((Ioo 0 1).indicator fun x ↦ P.f x) + (Ioi 1).indicator fun x ↦ P.f x) t = ↑t ^ (s - 1) • P.f t
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ 0 < (I * ↑t).im

Tactic:
simpa

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ 0 < (I * ↑t).im

Tactic:
simpa

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

Goal state before:
pp: a x : ℝ
⊢ cexp (↑π * I * ↑a ^ 2 * (I * ↑x)) *
      (jacobiTheta₂' (↑a * (I * ↑x)) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * (I * ↑x)) (I * ↑x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
← mul_assoc ↑a I x,

Goal state after:
a x : ℝ
⊢ cexp (↑π * I * ↑a ^ 2 * (I * ↑x)) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H.hτ
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

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

Goal state before:
pp: x : ℝ
hx : x ≤ 0
a : ℝ
⊢ (I * ↑x).im ≤ 0

Tactic:
simpa

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 * ↑x * I⁻¹ = I * ↑x

Tactic:
inv_I,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 * ↑x * -I = I * ↑x
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

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

Tactic:
by
  have := zeta_eq_tsum_one_div_nat_cpow hs
  rw [Summable.tsum_eq_zero_add] at this
  · simpa [zero_cpow (Complex.ne_zero_of_one_lt_re hs)]
  · rwa [Complex.summable_one_div_nat_cpow]

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

Goal state before:
pp: case refine_2.refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
ha : a ≠ 0
⊢ (if a = 0 then 1 else 0) = 0

Tactic:
simpa

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

Goal state before:
pp: s : ℂ
H : LSeriesSummable (fun n ↦ ↑(μ n)) s
h : s.re ≤ 1
⊢ s.re ≤ re 1

Tactic:
simpa

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
h : L (fun n ↦ ↑(ζ n)) s = 0
⊢ False

Tactic:
by simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

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

Goal state before:
pp: a : UnitAddCircle
r : ℝ
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
let ⟨v, hv, hv'⟩ := isBigO_atTop_oddKernel a
    rw [← isBigO_norm_left] at hv' ⊢
    simpa using hv'.trans (isLittleO_exp_neg_mul_rpow_atTop hv _).isBigO

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

Goal state before:
pp: case hf₁
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑↑n| ^ s.re

Tactic:
simpa

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

Goal state before:
pp: case hf₂
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := ⋯
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun n ↦ 1 / |↑(-↑n)| ^ s.re

Tactic:
simpa

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
abs_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 + cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|↑n| ^ s / 2)
    (cosZeta (↑a) s + cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedSinZeta (↑a) s)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)

Tactic:
abs_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|↑n| ^ s / 2)
    (completedSinZeta (↑a) s)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) atTop (𝓝 (L (fun n ↦ χ ↑n) s))

Tactic:
by
  rw [← tsum_dirichletSummand χ hs]
  apply eulerProduct_completely_multiplicative <| summable_dirichletSummand χ hs

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

Goal state before:
pp: case hg
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ Multipliable ((↑N.primeFactors).mulIndicator fun p ↦ 1 - χ ↑p * ↑p ^ (-s))

pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) b

Tactic:
· exact multipliable_subtype_iff_mulIndicator.mp Multipliable.of_finite

Goal state after:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    ∏' (b : ℕ),
      {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - χ ↑p * ↑p ^ (-s))⁻¹) b *
        (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) b
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2

Tactic:
add_comm

Goal state after:
a b c : ℤ
⊢ a ≠ 0 ∧ b ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z

Tactic:
add_comm

Goal state after:
x y z : ℤ
⊢ y * y + x * x = z * z ↔ y * y + x * x = z * z
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
this : 0 < (s + 1).re
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 =
    (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 / (s + 1).Gammaℝ

Tactic:
simp [div_right_comm _ _ (Gammaℝ _), mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos this)]

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

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Tactic:
exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(-SignType.sign (↑n + 1 - a)) / ↑|(-(↑n + 1 - a))| ^ s / 2

Tactic:
abs_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
this : -(↑n + 1) + a = -(↑n + 1 - a)
⊢ ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + -(↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2) =
    ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2 + ↑(-SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s / 2
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (r ^ 2 + s ^ 2) s

Tactic:
add_comm

Goal state after:
r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
abs_neg,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|↑n| ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]

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✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
⊢ 2 = 1 + 1 ^ 2

Tactic:
rw [one_pow 2]

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
⊢ 2 = 1 + 1
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case right
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ derivative b = 0

Tactic:
rw [← dvd_derivative_iff]
      apply hc.symm.dvd_of_dvd_mul_left
      rw [hw]; exact dvd_mul_left _ _

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (m ^ 2 + n ^ 2).natAbs = 1

Tactic:
add_comm

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ (n ^ 2 - m ^ 2).natAbs.gcd (n ^ 2 + m ^ 2).natAbs = 1
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 : s.gcd r = 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
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ i.natAbs < c.natAbs

Tactic:
apply Int.ofNat_lt.mp

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 : s.gcd r = 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
hd : s * r = d ^ 2
j : ℤ
hj : r = j ^ 2 ∨ r = -j ^ 2
hj0 : j ≠ 0
k : ℤ
hk : s = k ^ 2 ∨ s = -k ^ 2
hk0 : k ≠ 0
hj2 : r ^ 2 = j ^ 4
hk2 : s ^ 2 = k ^ 4
hh : i ^ 2 = j ^ 4 + k ^ 4
hn : n ≠ 0
⊢ ↑i.natAbs < ↑c.natAbs
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ radical a = normalize a

Tactic:
by
  rw [radical, primeFactors]
  rw [normalizedFactors_irreducible ha.irreducible]
  simp only [Multiset.toFinset_singleton, id, Finset.prod_singleton]

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case a
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
⊢ ∀ i ∈ primeFactors a, id i ∣ p

Tactic:
intro i hi

Goal state after:
case a
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
p : M
ha : radical a ∣ p ^ n
i : M
hi : i ∈ primeFactors a
⊢ id i ∣ p
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ a.wronskian b
⊢ divRadical (a * b * c) ∣ w

Tactic:
have bdr_dvd_w := divRadical_dvd_wronskian_right a b

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
wca : w = c.wronskian a
adr_dvd_w : divRadical a ∣ a.wronskian b
bdr_dvd_w : divRadical b ∣ a.wronskian b
⊢ divRadical (a * b * c) ∣ w
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (insert i ↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ i ∉ ↑s

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ divRadical a * divRadical b = divRadical (a * b)

Tactic:
apply eq_divRadical

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a b : E
hab : IsCoprime a b
⊢ radical (a * b) * (divRadical a * divRadical b) = a * b