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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
⊢ ε > 0 → ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
⊢ ε > 0 →
    ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
⊢ ε > 0 → ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
⊢ 0 < ε → ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
rw [Ideal.mem_span_singleton]

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n ∣ ↑(nthHom f r (max n k)) - ↑((f n) r).val
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 :
  ↑↑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

Tactic:
simp only [← rootsOfUnity.coe_pow] 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
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
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
⊢ ε > 0 → dist ((lift f_compat) r) (g r) ≤ ε

Tactic:
hε

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), (toZModPow n).comp g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist ((lift f_compat) r) (g r) ≤ ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
⊢ ε > 0 → ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε

Tactic:
hε

Goal state after:
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p ((fun x ↦ ↑(f x)) j - (fun x ↦ ↑(f x)) i) < ε
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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
⊢ ∑ σ,
      Equiv.Perm.sign σ •
        ∏ i_1, (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ i_1) i_1 ∈
    ⊥

Tactic:
refine
    Subalgebra.sum_mem _ fun σ _ => Subalgebra.zsmul_mem _ (Subalgebra.prod_mem _ fun j _ => ?_) _

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)
i : Fin B.dim
cramer :
  ((traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • B.basis.equivFun z
σ : Equiv.Perm (Fin B.dim)
x✝¹ : σ ∈ univ
j : Fin B.dim
x✝ : j ∈ univ
⊢ (traceMatrix K ⇑B.basis).updateCol i (fun i ↦ (trace K L) (z * B.basis i)) (σ j) j ∈ ⊥
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ AddCommGroup (ℤ√d)

Tactic:
by
  refine
  { sub := fun a b => a + -b
    nsmul := @nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩
    zsmul := @zsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩ ⟨Neg.neg⟩ (@nsmulRec (ℤ√d) ⟨0⟩ ⟨(· + ·)⟩)
    add_assoc := ?_
    zero_add := ?_
    add_zero := ?_
    neg_add_cancel := ?_
    add_comm := ?_ } <;>
  intros <;>
  ext <;>
  simp [add_comm, add_left_comm]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 m ≤ yn a1 n

Tactic:
rw [e]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ xn a1 m ≤ xn a1 n

Tactic:
rw [e]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 n

Tactic:
rw [e]

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ yn a1 m ∣ yn a1 (m * k)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
⊢ ↑(-x).norm = ↑x.norm

Tactic:
by simp [norm_eq_mul_conj]

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

Goal state before:
pp: d : ℕ
a : ℤ√↑d
n : ℕ
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ { re := ↑n * ↑x, im := ↑n * -↑y }.Nonneg

Tactic:
simpa using! nonnegg_pos_neg.2 (sqLe_smul n <| nonnegg_pos_neg.1 ha)

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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Tactic:
exact nonnegg_pos_neg.2 (sqLe_mul.left (nonnegg_neg_pos.1 ha) (nonnegg_neg_pos.1 hb))

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

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
let t := le_antisymm yx xy

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : 1 * (x + 1) * (x + 1) = d * y.succ * y.succ := le_antisymm yx xy
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
S : Set (α ⊕ Fin2 0 → ℕ)
d : Dioph S
f : Vector3 ((α → ℕ) → ℕ) 0
x✝ : VectorAllP DiophFn f
v : α → ℕ
⊢ v ∈ {v | v ∘ (id ⊗ elim0) ∈ S} ↔ v ∈ {v | (v ⊗ fun i ↦ f i v) ∈ S}

Tactic:
by
      dsimp
      -- TODO: `congr! 1; ext` should be equivalent to `congr! 1 with x` but that does not work.
      congr! 1
      ext x; obtain _ | _ | _ := x; rfl

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | ⟨m, property⟩ => (m.factorization p, ⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩))
    fun x ↦
    match x with
    | (e, n) => ⟨p ^ e * ↑n, ⋯⟩

Tactic:
rintro ⟨e, m, hm₀, hm⟩

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ (fun x ↦
        match x with
        | ⟨m, property⟩ => (m.factorization p, ⟨(List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod, ⋯⟩))
      ((fun x ↦
          match x with
          | (e, n) => ⟨p ^ e * ↑n, ⋯⟩)
        (e, ⟨m, ⋯⟩)) =
    (e, ⟨m, ⋯⟩)
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
⊢ n ∈
    Finset.image
      (fun x ↦
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
obtain ⟨hn₁, hn₂⟩ := mem_smoothNumbersUpTo.mp hn

Goal state after:
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
⊢ n ∈
    Finset.image
      (fun x ↦
        match x with
        | (s, m) => m ^ 2 * s.prod id)
      (k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)
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)
ε : ℝ
⊢ ε > 0 →
    ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
hε

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, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f 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
⊢ HasProd (fun p ↦ ∑' (e : ℕ), f (↑p ^ e)) (∑' (n : ℕ), f n)

Tactic:
let F : ℕ → R := fun n ↦ ∑' e, f (n ^ e)
  change HasProd (F ∘ Subtype.val (p := (· ∈ {x | Nat.Prime x}))) _
  rw [hasProd_subtype_iff_mulIndicator, HasProd, SummationFilter.unconditional,
    Metric.tendsto_atTop]
  intro ε hε
  obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum.of_norm hf₀ hε
  refine ⟨range N₀, fun s hs ↦ ?_⟩
  have : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with p.Prime, F p :=
    prod_mulIndicator_eq_prod_filter s (fun _ ↦ F) _ id
  rw [this, dist_eq_norm, prod_filter_prime_tsum_eq_tsum_factoredNumbers hf₁ hmul hsum,
    norm_sub_rev]
  exact hN₀ s fun p hp ↦ hs <| mem_range.mpr <| lt_of_mem_primesBelow hp

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

Goal state before:
pp: case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑' (b : ↑↑n.divisorsAntidiagonal), term f s (↑b).1 * term g s (↑b).2

Tactic:
Finset.tsum_subtype' n.divisorsAntidiagonal fun p ↦ term f s p.1 * term g s p.2,

Goal state after:
case inr
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (f ⍟ g) s n = ∑ x ∈ n.divisorsAntidiagonal, term f s x.1 * term g s x.2
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 1))

Tactic:
tprod_primes_pow_eq (hfm.subtype _)

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = ∏' (n : { n // IsPrimePow n }), f ↑n
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

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

Tactic:
n

Goal state after:
S T : ℝ
hT : 0 < T
k n : ℕ
| -(-π * (T * ↑n ^ 2 - 2 * S * ↑n) - -1 * ↑n)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
| fun n ↦ rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Tactic:
n

Goal state after:
z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
n : ℕ
| rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

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

Tactic:
simp_rw [sub_zero]
    have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) := by
      apply Eventually.isBigO
      filter_upwards [eventually_gt_atTop 0] with t ht
      exact F_nat_zero_le ha ht
    refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
    simpa only [neg_mul π (a ^ 2), mul_one] using! (isBigO_refl _ _).mul isBigO_one_aux

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

Goal state before:
pp: case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ ‖(2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑|n| ^ 2

Tactic:
simp_rw [hns, norm_mul, ← ofReal_ofNat, ← ofReal_intCast,
      norm_real, norm_of_nonneg zero_le_two, Real.norm_of_nonneg pi_pos.le, norm_I, mul_one,
      Real.norm_eq_abs, ← Int.cast_abs, ← Int.cast_pow]

Goal state after:
case refine_1
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ 2 * π * ↑|n| * ‖ContinuousLinearMap.fst ℂ ℂ ℂ‖ ≤ 2 * π * ↑(|n| ^ 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
hVmem : (z, τ) ∈ V
⊢ Convex ℝ {u | |u.im| < S}

Tactic:
simpa only [abs_lt] using! (convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _)

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

Goal state before:
pp: z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ + ↑π * I * ↑n ^ 2 * 2) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)

Tactic:
Complex.exp_add,

Goal state after:
z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ cexp (2 * ↑π * I * ↑n * z) * (cexp (↑π * I * ↑n ^ 2 * τ) * cexp (↑π * I * ↑n ^ 2 * 2)) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z + 2 * ↑π * I * ↑n * 1 + ↑π * I * ↑n ^ 2 * τ) =
    cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
Complex.exp_add,

Goal state after:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (2 * ↑π * I * ↑n * 1) * cexp (↑π * I * ↑n ^ 2 * τ) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)
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:
| H a =>

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

Goal state before:
pp: z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ + ↑π * I * ↑n ^ 2 * 2)) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))

Tactic:
Complex.exp_add,

Goal state after:
z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * (cexp (↑π * I * ↑n ^ 2 * τ) * cexp (↑π * I * ↑n ^ 2 * 2))) =
    2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case H
x : ℝ
hx : x ≤ 0
a : ℝ
⊢ sinKernel (↑a) x = 0

Tactic:
| H a =>

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

Goal state before:
pp: case H
x a : ℝ
⊢ oddKernel (-↑a) x = -oddKernel (↑a) x

Tactic:
| H a =>

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

Goal state before:
pp: case H
x a : ℝ
⊢ sinKernel (-↑a) x = -sinKernel (↑a) x

Tactic:
| H a =>

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

Goal state before:
pp: z τ : ℂ
hτ : τ.im ≤ 0
⊢ -(-τ.im / normSq τ) ≤ 0

Tactic:
neg_nonpos

Goal state after:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
| H a =>

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

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

Tactic:
| H a =>

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

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

Tactic:
sinKernel_undef _ (one_div_nonpos.mpr hx),

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

Goal state before:
pp: case H
a : ℝ
⊢ ∃ p, 0 < p ∧ (fun x ↦ cosKernel (↑a) x - 1) =O[atTop] fun x ↦ rexp (-p * x)

Tactic:
| H a =>

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

Goal state before:
pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ -(-τ.im / normSq τ) ≤ 0

Tactic:
neg_nonpos

Goal state after:
case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
| H a =>

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ↑N * ∑ p ∈ N.succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
Finset.mul_sum,

Goal state after:
N k : ℕ
⊢ ↑(N.roughNumbersUpTo k).card ≤ ∑ i ∈ N.succ.primesBelow \ k.primesBelow, ↑N * (1 / ↑i)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: k : ℕ
⊢ 1 / 2 ≤ ∑ p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow, 1 / ↑p

Tactic:
by
  set m : ℕ := 2 ^ k.primesBelow.card
  set N₀ : ℕ := 2 * m ^ 2 with hN₀
  let S : ℝ := ((2 * N₀).succ.primesBelow \ k.primesBelow).sum (fun p ↦ (1 / p : ℝ))
  suffices 1 / 2 ≤ S by
    convert! this using 5
    rw [show 4 = 2 ^ 2 by simp, pow_right_comm]
    ring
  suffices 2 * N₀ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S by
    rwa [hN₀, ← mul_assoc, ← pow_two 2, ← mul_pow, sqrt_eq', ← sub_le_iff_le_add',
      cast_mul, cast_mul, cast_pow, cast_two,
      show (2 * (2 * m ^ 2) - m * (2 * m) : ℝ) = 2 * (2 * m ^ 2) * (1 / 2) by ring,
      mul_le_mul_iff_right₀ <| by positivity] at this
  calc (2 * N₀ : ℝ)
    _ = ((2 * N₀).smoothNumbersUpTo k).card + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast ((2 * N₀).smoothNumbersUpTo_card_add_roughNumbersUpTo_card k).symm
    _ ≤ m * (2 * N₀).sqrt + ((2 * N₀).roughNumbersUpTo k).card := by
        exact_mod_cast Nat.add_le_add_right ((2 * N₀).smoothNumbersUpTo_card_le k) _
    _ ≤ m * (2 * N₀).sqrt + 2 * N₀ * S := by grw [roughNumbersUpTo_card_le']; norm_cast

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

Goal state before:
pp: case neg
N : ℕ
hN : N ≠ 0
χ : DirichletCharacter ℂ N
h : LSeriesSummable (fun n ↦ χ ↑n) 1
n : ℕ
h₁ : ↑n = 1
h₂ : ¬n = 0
⊢ 1 / ↑n ≤ ‖χ ↑n‖ / ↑n ^ re 1

Tactic:
simp [h₁, χ.map_one]

Goal state after: