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

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i); swap
  · simp only [cyclotomicCharacter, cyclotomicCharacter.toFun, dif_neg H, MonoidHom.coe_comp]
    exact continuous_const (y := 1)
  have _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
  choose ζ hζ using H
  refine Continuous.of_coeHom_comp ?_
  apply continuous_of_continuousAt_one
  rw [ContinuousAt, map_one, (galGroupBasis K L).nhds_one_hasBasis.tendsto_iff
    (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))]
  intro ε hε
  obtain ⟨k, hk', hk⟩ : ∃ k : ℕ, k ≠ 0 ∧ p ^ (-k : ℤ) < ε := by
    obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
    exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩
  refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
  · exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top
  · intro σ hσ
    refine lt_of_le_of_lt ?_ hk
    dsimp
    rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow,
      RingHom.mem_ker, map_sub, map_one, cyclotomicCharacter.toZModPow,
      sub_eq_zero, eq_comm]
    apply modularCyclotomicCharacter.unique
    intro t ht
    obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht
    rw [ZMod.val_one'', pow_one]
    · exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩
    · exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'

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

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
key :
  zeta n K L ^
      (↑((IsPrimitiveRoot.autToPow K hζ)
            ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val =
    zeta n K L ^ (↑x).val
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x

Tactic:
nth_rw 1 5 [← hζ.val_toRootsOfUnity_coe] at key

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
key :
  ↑↑hζ.toRootsOfUnity ^
      (↑((IsPrimitiveRoot.autToPow K hζ)
            ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val =
    ↑↑hζ.toRootsOfUnity ^ (↑x).val
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  hζ.toRootsOfUnity ^
      (↑((IsPrimitiveRoot.autToPow K hζ)
            ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val =
    hζ.toRootsOfUnity ^ (↑x).val
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x

Tactic:
pow_eq_pow_iff_modEq,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h✝ : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
x : (ZMod n)ˣ
pf✝ : IsPrimitiveRoot (zeta n K L ^ (↑x).val) n
h : minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K pf✝).gen
this :
  ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h) (zeta n K L) =
    (IsPrimitiveRoot.powerBasis K ⋯).gen
key :
  (↑((IsPrimitiveRoot.autToPow K hζ)
          ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) h))).val ≡
    (↑x).val [MOD orderOf hζ.toRootsOfUnity]
⊢ (IsPrimitiveRoot.autToPow K hζ)
      ((IsPrimitiveRoot.powerBasis K hζ).equivOfMinpoly (IsPrimitiveRoot.powerBasis K pf✝) h) =
    x
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ d a1 + 1 = a * a

Tactic:
exact Nat.succ_pred_eq_of_pos (asq_pos a1)

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f - -g)

Tactic:
exact hf.sub hg.neg

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

Goal state before:
pp: case e_a.refine_1
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ↑p ^ (k + 1) ≠ 0
⊢ False

Tactic:
Ne,

Goal state after:
case e_a.refine_1
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * (k.succ * (p - 1)).pred) * ↑p ^ p ^ k
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this✝ : 0 < k.succ * (p - 1)
h : ↑p ^ p ^ k = 0
this : ¬↑p ^ (k + 1) = 0
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
exact
    ((dvd_mul_right _ _).mul_left _).modEq_zero_nat.add (xn_modEq_x2n_add_lem _ _ _).modEq_zero_nat

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']
    apply xn_modEq_x2n_add

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

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

Tactic:
← abs_of_pos hn,

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

Goal state before:
pp: case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - ↑(⌊ξ * ↑m⌋ + 1)) * (↑n + 1)| ≤ 1

Tactic:
cast_add,

Goal state after:
case pos
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - (↑⌊ξ * ↑m⌋ + ↑1)) * (↑n + 1)| ≤ 1
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]
⊢ n ≤ 2 * n

Tactic:
rw [two_mul]

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]
⊢ n ≤ n + n
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)
⊢ Filter.Tendsto (fun s ↦ ∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) { filter := Filter.atTop }.filter
    (𝓝 (∑'[{ filter := Filter.atTop }] (n : ℕ), f n))

Tactic:
Metric.tendsto_atTop

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)
⊢ ∀ ε > 0,
    ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ n ^ k = m

Tactic:
have : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t] := by
      apply modEq_of_dvd
      rw [te, Nat.cast_add, Nat.cast_mul, Int.ofNat_sub na]
      exact x_sub_y_dvd_pow a1 n k

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
this : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
⊢ n ^ k = m
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
N : ℕ
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ range N with Nat.Prime p, (1 - f p)⁻¹)

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
  have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
  have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
    prod_mulIndicator_eq_prod_filter
      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
  have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
  simpa only [← H, H'] using this

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

Goal state before:
pp: case convert_3.inr
ι : 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 : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ↑(p i) ^ (s - 1) ≠ 0

Tactic:
Ne,

Goal state after:
case convert_3.inr
ι : 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 : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ¬↑(p i) ^ (s - 1) = 0
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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
⊢ ∫ (a : ℝ) in Ioi 0 ∩ Ioo 0 1, ↑a ^ (s - 1) • (P.f₀ - (P.ε * ↑(a ^ (-P.k))) • P.g₀) =
    ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀)

Tactic:
inter_eq_right.mpr Ioo_subset_Ioi_self,

Goal state after:
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
⊢ ∫ (a : ℝ) in Ioo 0 1, ↑a ^ (s - 1) • (P.f₀ - (P.ε * ↑(a ^ (-P.k))) • P.g₀) =
    ∫ (x : ℝ) in Ioc 0 1, ↑x ^ (s - 1) • (P.f₀ - (P.ε * ↑(x ^ (-P.k))) • P.g₀)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: 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
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - P.ε • (↑x ^ (s - 1) * ↑x ^ (-↑P.k)) • P.g₀ =
    ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀

Tactic:
← cpow_add _ _ (ofReal_ne_zero.mpr hx.ne'),

Goal state after:
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
x : ℝ
x✝ : x ∈ Ioc 0 1
hx : 0 < x
right✝ : x ≤ 1
⊢ ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - 1 + -↑P.k) • P.g₀ = ↑x ^ (s - 1) • P.f₀ - P.ε • ↑x ^ (s - ↑P.k - 1) • P.g₀
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

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

Tactic:
if_false,

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

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ evenKernel (↑a) x = 1 / x ^ (1 / 2) * cosKernel (↑a) (1 / x)

Tactic:
rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
  have h1 : I * ↑(1 / x) = -1 / (I * x) := by
    push_cast
    rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
  have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
  have h2 : a * I * x / (I * x) = a := by
    rw [div_eq_iff hx']
    ring
  have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
    rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg, ofReal_cpow hx.le, ofReal_div,
      ofReal_one, ofReal_ofNat]
  have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
    rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
    ring
  rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]

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:
neg_div τ z,

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.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)

Tactic:
· rw [cpow_add _ _ (ofReal_ne_zero.mpr <| abs_ne_zero.mpr h), cpow_one]
      conv_rhs => enter [1]; rw [← sign_mul_abs (r i), ofReal_mul, ← ofRealHom_eq_coe,
        SignType.map_cast]
      field [h]

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

Goal state before:
pp: case H
a : ℝ
⊢ ContinuousOn (oddKernel ↑a) (Ioi 0)

Tactic:
suffices ContinuousOn (fun x ↦ (oddKernel a x : ℂ)) (Ioi 0) from
    (continuous_re.comp_continuousOn this).congr fun a _ ↦ (ofReal_re _).symm
  simp_rw [oddKernel_def' a]
  refine fun x hx ↦ ((Continuous.continuousAt ?_).mul ?_).continuousWithinAt
  · fun_prop
  · have hf : Continuous fun u : ℝ ↦ (a * I * u, I * u) := by fun_prop
    apply ContinuousAt.add
    · exact ((continuousAt_jacobiTheta₂' (a * I * x) (by rwa [I_mul_im, ofReal_re])).comp
        (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt).div_const _
    · exact continuousAt_const.mul <| (continuousAt_jacobiTheta₂ (a * I * x)
        (by rwa [I_mul_im, ofReal_re])).comp (f := fun u : ℝ ↦ (a * I * u, I * u)) hf.continuousAt

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

Goal state before:
pp: case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * I ^ 2 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + I ^ 4 * z ^ 2 * τ⁻¹ =
    ↑n * I ^ 2 * z * τ⁻¹ * 2 - ↑n ^ 2 * I ^ 2 * τ⁻¹ - I ^ 2 * z ^ 2 * τ⁻¹

Tactic:
simp_rw [I_sq, I_pow_four]

Goal state after:
case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * -1 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + 1 * z ^ 2 * τ⁻¹ = ↑n * -1 * z * τ⁻¹ * 2 - ↑n ^ 2 * -1 * τ⁻¹ - -1 * z ^ 2 * τ⁻¹
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ

Tactic:
by
  rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]

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

Goal state before:
pp: a b : UnitAddCircle
z : ℂ
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z

Tactic:
rcases ne_or_eq z 1 with hz | rfl

Goal state after:
case inl
a b : UnitAddCircle
z : ℂ
hz : z ≠ 1
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z

case inr
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inl
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ IsCoprime a b

Tactic:
simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(a.wronskian b).natDegree < ↑a.natDegree + ↑b.natDegree

Tactic:
convert! ← degree_wronskian_lt_add ha hb

Goal state after:
case e'_3
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree = ↑(a.wronskian b).natDegree

case e'_4.e'_5
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree = ↑a.natDegree

case e'_4.e'_6
R : Type u_1
inst✝ : CommRing R
a b : R[X]
hw : a.wronskian b ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ b.degree = ↑b.natDegree
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ radical a ∣ a

Tactic:
· rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le
    rw [primeFactors, Multiset.toFinset_val]
    apply Multiset.dedup_le

Goal state after: