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

Goal state before:
pp: 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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ discr K ⇑B.basis • (B.basis.repr z) i • B.basis i ∈ R[B.gen]

Tactic:
← smul_assoc,

Goal state after:
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)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ (discr K ⇑B.basis • (B.basis.repr z) i) • B.basis i ∈ R[B.gen]
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
rw [heven.neg_one_pow]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ χ ∈
      OrderDual.ofDual
        (OrderDual.toDual
          (Subgroup.map mulEquivToUnitHom.symm.toMonoidHom
            (OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H)))) ↔
    ∀ m ∈ H, χ ↑m = 1

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
χ : MulChar M R
⊢ χ ∈
      Subgroup.map mulEquivToUnitHom.symm.toMonoidHom
        (OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H)) ↔
    ∀ m ∈ H, χ ↑m = 1
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card
      ↥(OrderDual.ofDual
          (OrderDual.toDual
            (mulEquivToUnitHom.symm.mapSubgroup
              (OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H))))) =
    Nat.card (Mˣ ⧸ H)

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
H : Subgroup Mˣ
⊢ Nat.card
      ↥(mulEquivToUnitHom.symm.mapSubgroup (OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom Mˣ R) H))) =
    Nat.card (Mˣ ⧸ H)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
⊢ j + (4 * n - j) = 4 * n

Tactic:
add_tsub_cancel_of_le j4n

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
⊢ 4 * n = 4 * n
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
simp only [Poly.map_apply] at ht
              rwa [show (v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some) = t none ::ₒ v ⊗ t ∘ some from
                funext fun s => by rcases s with a | b <;> try { cases a <;> rfl }; rfl] at ht

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
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : ↑u * (2 * ↑v - 1) - ξ * ↑v * (2 * ↑v - 1) < 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
← sub_mul,

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) < 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
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, LSeriesSummable f ↑x

Tactic:
exact ⟨x, by simpa using hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩

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

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

Tactic:
· rw [hf] at huv_cop
      simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
      rcases huv_cop with huv_cop | huv_cop <;> linarith only [hv, huv_cop]

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

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

Tactic:
· rw [hf] at huv_cop
      simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
      rcases huv_cop with huv_cop | huv_cop <;> linarith only [hv, huv_cop]

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

Goal state before:
pp: f : ℕ → ℂ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C
⊢ abscissaOfAbsConv f ≤ 1

Tactic:
by
  simpa using abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) (by simpa using h)

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

Goal state before:
pp: 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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with Nat.Prime p, F p
⊢ dist (∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
rw [this, dist_eq_norm, prod_filter_prime_tsum_eq_tsum_factoredNumbers hf₁ hmul hsum,
    norm_sub_rev]

Goal state after:
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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with Nat.Prime p, F p
⊢ ‖∑'[{ filter := Filter.atTop }] (n : ℕ), f n - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
replace h := h.2.2
    simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul,
      cast_zero, inv_zero] at h
    exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)

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

Goal state before:
pp: a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) ↑x

Tactic:
rw [LSeries_iteratedDeriv _ h, LSeries, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨n, rfl⟩,
    one_mul]

Goal state after:
a : ℕ → ℂ
hn : 0 ≤ a
x : ℝ
h : abscissaOfAbsConv a < ↑x
n : ℕ
⊢ 0 ≤ ∑' (n_1 : ℕ), term (logMul^[n] a) (↑x) n_1
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ := { toFun := fun f ↦ f (1, 0), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0)) ((jacobiTheta₂_fderiv z τ) (1, 0))

Tactic:
apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)

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

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
n : ℤ
| cexp (-↑π * I * (τ + 2 * z)) *
    (2 * ↑π * I * ↑(n + 1) * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ) -
      2 * ↑π * I * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ))

Tactic:
← sub_mul,

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
n : ℤ
| cexp (-↑π * I * (τ + 2 * z)) *
    ((2 * ↑π * I * ↑(n + 1) - 2 * ↑π * I) * cexp (2 * ↑π * I * ↑(n + 1) * z + ↑π * I * ↑(n + 1) ^ 2 * τ))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
by
  rcases le_or_gt τ.im 0 with hτ | hτ
  · simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]
  have (n : ℤ) : jacobiTheta₂'_term n (z + τ) τ =
      cexp (-π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ -
      2 * π * I * jacobiTheta₂_term (n + 1) z τ) := by
    simp only [jacobiTheta₂'_term, jacobiTheta₂_term]
    conv_rhs => rw [← sub_mul, mul_comm, mul_assoc, ← Complex.exp_add, Int.cast_add, Int.cast_one,
      mul_add, mul_one, add_sub_cancel_right]
    congr 2
    ring
  rw [jacobiTheta₂', funext this, tsum_mul_left, ← (Equiv.subRight (1 : ℤ)).tsum_eq]
  simp only [jacobiTheta₂, jacobiTheta₂', Equiv.subRight_apply, sub_add_cancel,
    (hasSum_jacobiTheta₂'_term z hτ).summable.tsum_sub
    ((hasSum_jacobiTheta₂_term z hτ).summable.mul_left _), tsum_mul_left]

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

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

Tactic:
oddKernel_undef _ hx,

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 0 = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ 1 / (↑n + ↑a) ^ s) (hurwitzZeta (↑a) s)

Tactic:
by
  convert!
    (hasSum_nat_hurwitzZetaEven_of_mem_Icc ha hs).add (hasSum_nat_hurwitzZetaOdd_of_mem_Icc ha hs)
    using 1
  ext1 n
  -- plain `ring_nf` works here, but the following is faster:
  apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring

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

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

Tactic:
by
  rw [riemannZeta, hurwitzZetaEven_one_sub 0 hs (Or.inr hs'), cosZeta_zero, hurwitzZetaEven_zero]

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

Goal state before:
pp: case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ I * ↑n * (cexp (-(2 * ↑π * ↑a * ↑n * I)) - cexp (2 * ↑π * ↑a * ↑n * I)) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)

Tactic:
mul_sub

Goal state after:
case e_a
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ I * ↑n * cexp (-(2 * ↑π * ↑a * ↑n * I)) - I * ↑n * cexp (2 * ↑π * ↑a * ↑n * I) =
    I * ↑n * cexp (-(2 * ↑π * I * ↑a * ↑n)) - I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n)
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ (abscissaOfAbsConv fun n ↦ χ ↑n) < ↑s.re

Tactic:
rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]

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

Goal state before:
pp: a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedHurwitzZetaEven a (-2 * (↑n + 1)) / (-2 * (↑n + 1)).Gammaℝ = 0

Tactic:
Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,

Goal state after:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ completedHurwitzZetaEven a (-2 * (↑n + 1)) / 0 = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ 1 / ↑|↑n + a| ^ s / 2) (hurwitzZetaEven (↑a) s)

Tactic:
by
  rw [hurwitzZetaEven, Function.update_of_ne (ne_zero_of_one_lt_re hs)]
  have := (hasSum_int_completedHurwitzZetaEven a hs).div_const (Gammaℝ s)
  exact this.congr_fun fun n ↦ by simp only [div_right_comm _ _ (Gammaℝ _),
    div_self (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Goal state after:
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) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
⊢ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s =
    ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
          (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
        ↑n ^ s /
      2

Tactic:
rw [div_right_comm]

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

Tactic:
rw [← tsum_riemannZetaSummand hs]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ HasProd (fun p ↦ (1 - ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

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

Tactic:
rw [← tsum_riemannZetaSummand hs]

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case pos
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
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ 1 - χ ↑p * ↑p ^ (-s) ≠ 0

Tactic:
rw [sub_ne_zero, ne_comm]

Goal state after:
case pos
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
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ χ ↑p * ↑p ^ (-s) ≠ 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: y z : ℤ
h : PythagoreanTriple 0 y z
hc : Nat.gcd 0 y.natAbs = 1
⊢ h.IsPrimitiveClassified

Tactic:
rw [Nat.gcd_zero_left (Int.natAbs y)] at hc

Goal state after:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
⊢ h.IsPrimitiveClassified
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ wronskian 0 a = 0

Tactic:
rw [← wronskianBilin_apply 0 a, map_zero]; rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

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

Tactic:
exact Polynomial.degree_derivative_lt ha

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : radical a = radical b
⊢ primeFactors (radical b) = primeFactors b

Tactic:
exact primeFactors_radical

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ contract (ringChar k) a ≠ 0

pp: case refine_2
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ a.natDegree = (contract (ringChar k) a).natDegree * ringChar k

Tactic:
· intro h
    rw [h, map_zero] at heq
    exact ha heq

Goal state after:
case refine_2
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
⊢ a.natDegree = (contract (ringChar k) a).natDegree * ringChar k
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl.left
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m).gcd (-n) = 1

pp: case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
· delta Int.gcd
          rw [Int.natAbs_neg, Int.natAbs_neg]
          exact ht3

Goal state after:
case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ x ^ n = 1

Tactic:
ext; rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ IsOfFinOrder ζ

Tactic:
isOfFinOrder_iff_pow_eq_one

Goal state after:
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ IsOfFinOrder ζ

Tactic:
isOfFinOrder_iff_pow_eq_one

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
v : InfinitePlace ℚ
⊢ v.IsReal

Tactic:
by
    rw [Subsingleton.elim v Rat.infinitePlace]
    exact Rat.isReal_infinitePlace

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ ⨆ i, k i ≤ maximalRealSubfield K

Tactic:
iSup_le_iff

Goal state after:
case inr
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
i : ι
⊢ ∀ (i : ι), k i ≤ maximalRealSubfield K
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (w.comap (algebraMap k K)).mult ≤ w.mult ∧ w.mult ≤ (w.comap (algebraMap k K)).mult ↔
    w.mult ≤ (w.comap (algebraMap k K)).mult

Tactic:
and_iff_right

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ w.mult ≤ (w.comap (algebraMap k K)).mult ↔ w.mult ≤ (w.comap (algebraMap k K)).mult

k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (w.comap (algebraMap k K)).mult ≤ w.mult
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ mixedEmbedding.norm x = mixedEmbedding.norm y

Tactic:
by
  simp_rw [mixedEmbedding.norm_apply, h]

Goal state after: