mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a
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
⊢ traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = fun i ↦ (trace K L) (z * B.basis i)

Tactic:
exact traceMatrix_of_basis_mulVec _ _

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case proj
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
i✝ : α
⊢ C ⟨fun x ↦ ↑(x i✝), ⋯⟩

Tactic:
apply H1

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

Goal state before:
pp: case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : d * (z.im * z.im) = 0
⊢ z.im * z.im = 0

Tactic:
mul_eq_zero

Goal state after:
case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : d = 0 ∨ z.im * z.im = 0
⊢ z.im * z.im = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]

Tactic:
exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

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

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ (↑↑x + sqrtd * ↑↑y) * a = ↑x * a + sqrtd * (↑y * a)

Tactic:
right_distrib,

Goal state after:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ ↑↑x * a + sqrtd * ↑↑y * a = ↑x * a + sqrtd * (↑y * a)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) = 0

Tactic:
rw [← Nat.lt_one_iff]

Goal state after:
case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) < 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α β : Type u
f : (α → ℕ) → ℕ
g : α → β
d : DiophFn f
⊢ DiophFn fun v ↦ f (v ∘ g)

Tactic:
by convert! reindex_dioph (Option β) (Option.map g) d

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N

Tactic:
rwa [Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
hs : abscissaOfAbsConv f < ↑s.re
x : ℝ
hx₁ : abscissaOfAbsConv f < ↑x
hx₂ : ↑x < ↑s.re
⊢ x < s.re

Tactic:
by simpa using hx₂

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

Goal state before:
pp: case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ (Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))) → False

Tactic:
simpa only [hz, mul_zero, neg_zero, Real.exp_zero, summable_const_iff] using one_ne_zero

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

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

Tactic:
f_modif,

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : 1 < x
this : 1 / x < 1
⊢ (((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₀)
      (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

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

Tactic:
f_modif,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
x : ℝ
hx : 0 < x
hx' : x < 1
this : 1 < 1 / 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₀)
      (1 / x) =
    (P.ε * ↑(x ^ P.k)) • P.g_modif x
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 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:
f_modif,

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₀) + (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
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this✝ : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : ¬p i = 0
this : 0 ≤ p i
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re

Tactic:
rw [norm_of_nonneg (by positivity)]

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

Goal state before:
pp: case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I *
      (cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (jacobiTheta₂' (-(z / τ)) (-1 / τ) + z * jacobiTheta₂ (-(z / τ)) (-1 / τ) * (2 * ↑π * I)))

Tactic:
jacobiTheta₂_neg_left,

Goal state after:
case inr.e_a
z τ : ℂ
hτ : τ ≠ 0
aux1 : -2 * ↑π / (2 * ↑π * I) = I
⊢ -I *
      (cexp (-↑π * I * z ^ 2 / τ) * (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))) =
    I *
      (cexp (↑π * I * z ^ 2 * (-1 / τ)) *
        (jacobiTheta₂' (-(z / τ)) (-1 / τ) + z * jacobiTheta₂ (z / τ) (-1 / τ) * (2 * ↑π * I)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * I * s / 2) * (cosZeta a s + I * -sinZeta a s))

Tactic:
show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * cosZeta a s +
      2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
        sinZeta a s =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (-↑π * I * s / 2) * (cosZeta a s + I * sinZeta a s) +
        cexp (↑π * s / 2 * I) * (cosZeta a s + I * -sinZeta a s))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inr
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
calc
  _ = deriv (jacobiTheta₂ · τ) z := (hasDerivAt_jacobiTheta₂_fst z hτ).deriv.symm
  _ = deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    rw [funext (jacobiTheta₂_functional_equation · τ)]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z := by
    simp_rw [mul_assoc, deriv_const_mul_field]
  _ = 1 / (-I * τ) ^ (1 / 2 : ℂ) *
        (deriv (fun z ↦ cexp (-π * I * z ^ 2 / τ)) z * jacobiTheta₂ (z / τ) (-1 / τ)
         + cexp (-π * I * z ^ 2 / τ) * deriv (fun z ↦ jacobiTheta₂ (z / τ) (-1 / τ)) z) := by
    rw [deriv_fun_mul _ hj.differentiableAt]
    exact (((differentiableAt_pow 2).const_mul _).mul_const _).cexp
  _ = _ := by
    rw [hj.deriv]
    simp only [div_eq_mul_inv _ τ]
    rw [deriv_cexp (((differentiableAt_pow _).const_mul _).mul_const _), mul_comm,
      deriv_mul_const_field, deriv_const_mul_field, deriv_pow_field]
    ring_nf

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

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

Tactic:
show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
have h1 : Tendsto (fun s : ℂ ↦ (s - ↑(1 / 2 : ℝ)) * _) (𝓝[≠] ↑(1 / 2 : ℝ))
    (𝓝 ((1 : ℂ) * (1 : ℂ))) := (hurwitzEvenFEPair a).Λ_residue_k

Goal state after:
a : UnitAddCircle
h1 : Tendsto (fun s ↦ (s - ↑(1 / 2)) * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] ↑(1 / 2)) (𝓝 (1 * 1))
⊢ Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 1
⊢ (fun x ↦ χ ↑x) = 1

Tactic:
by
  ext
  rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]

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

Goal state before:
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

pp: case hf
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 ({p | Nat.Prime p}.mulIndicator fun p ↦ (1 - χ ↑p * ↑p ^ (-s))⁻¹)

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))

Tactic:
rotate_left

Goal state after:
case hf
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 ({p | Nat.Prime p}.mulIndicator fun p ↦ (1 - χ ↑p * ↑p ^ (-s))⁻¹)

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))

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: 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

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

Tactic:
· exact right_ne_zero_of_mul f42.1

Goal state after:
case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ ↑i ^ (-s.re)

Tactic:
filter_upwards [eventually_gt_atTop 1] with n hn

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
⊢ ‖f n‖ ≤ ↑n ^ (-s.re)
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Goal state after:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * derivative b).degree ≤ ?b

case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ ?b < a.degree + b.degree

case b
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ WithBot ℕ
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Goal state after:
case hab
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (derivative a * b).degree ≤ ?b

case hbc
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ ?b < a.degree + b.degree

case b
R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ WithBot ℕ
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (n : { n // IsPrimePow n }), f ↑n = ∑' (n : ℕ), χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) / ↑n ^ s

Tactic:
simp only [div_eq_mul_inv _ (_ ^ _), ← cpow_neg]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (n : { n // IsPrimePow n }), f ↑n = ∑' (n : ℕ), χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ False

Tactic:
apply @not_fermat_42 _ _ (c ^ 2) ha hb

Goal state after:
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
a✝ : c ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 4
⊢ a ^ 4 + b ^ 4 = (c ^ 2) ^ 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt ((m ^ 2 - n ^ 2) / 2 * 2) (m ^ 2 + n ^ 2)

Tactic:
Int.ediv_mul_cancel h1.2.1,

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ w = Rat.divInt (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = w x

Tactic:
nth_rewrite 2 [← mk_embedding w]

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = (mk w.embedding) x
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _
  exact map_zpow _ x n

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (∀ (x_1 : InfinitePlace K), x_1.IsReal ∨ ¬x_1.IsReal → ‖x_1.embedding x‖ < ↑(f x_1)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
em,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (∀ (x_1 : InfinitePlace K), True → ‖x_1.embedding x‖ < ↑(f x_1)) ↔ ∀ (w : InfinitePlace K), w x < ↑(f w)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
h : maximalRealSubfield K = ⊤
⊢ IsTotallyReal K

Tactic:
by
    have : Algebra.IsIntegral (⊤ : Subfield K) K := Algebra.IsIntegral.tower_top ℚ
    rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]

Goal state after: