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

Goal state before:
pp: case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₆ : ¬p ∣ b * (b ^ 2 - 1) := Nat.not_dvd_of_pos_of_lt h₄ h₅

Goal state after:
case pos
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ ↑n ≤ ↑n + 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 ≤ s + 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n / x ^ 2 =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
← mul_one_div (n : ℝ)

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -s ≠ -1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ -(s + 1) ≠ -1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ 0 ≤ ↑n + 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ ∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖ = |↑((Algebra.norm ℤ) x)|⁻¹

Tactic:
refine (inv_eq_of_mul_eq_one_left ?_).symm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) * |↑((Algebra.norm ℤ) x)| = 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ ∑ x ∈ Finset.range (N + 1), 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑(N + 1) + 1) ^ (s - 1))

Tactic:
rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
      ring_nf

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

Tactic:
← mul_one 1

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 * 1 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

Tactic:
· nth_rewrite 1 [← mul_one 1]
    gcongr
    · simp [hs]
    · exact s.one_le_prod fun _ _ ↦ le_max_right ..

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 0 < s - 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 0 ≤ s - 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
by linarith

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
⊢ logHeight₁ (∑ a ∈ s, x a) ≤ ↑(totalWeight K) * log ↑(#s) + ∑ a ∈ s, logHeight₁ (x a)

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  simp only [logHeight₁_eq_log_mulHeight₁]
  have : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0 := fun _ _ ↦ by positivity
  have : (#s : ℝ) ^ totalWeight K ≠ 0 := by simp [hs.ne_empty]
  pull (disch := first | assumption | positivity) log
  exact (log_le_log <| by positivity) <| mulHeight₁_sum_le hs x

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_bound
n : ℕ
⊢ ∀ x ∈ Ici 1,
    ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2

Tactic:
intro s (hs : 1 ≤ s)
    rw [ae_restrict_iff' measurableSet_Ioc]
    filter_upwards with x hx
    have : 1 < x := lt_of_le_of_lt (by simp) hx.1
    rw [norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)), Nat.cast_add_one]
    gcongr
    · exact_mod_cast sub_nonneg.mpr hx.1.le
    · exact this.le
    · linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < s + 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ↑(n + 1) ≤ ↑(n + 1) + 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∏ m ∈ (multisetInfinitePlace K).toFinset, f m ^ Multiset.count m (multisetInfinitePlace K) = ∏ v, f ↑v ^ v.mult

Tactic:
exact Finset.prod_bij' (fun w hw ↦ ⟨w, mem_multisetInfinitePlace.mp <| Multiset.mem_dedup.mp hw⟩)
    (fun v _ ↦ v.val) (fun _ _ ↦ Finset.mem_univ _) (fun v _ ↦ by simp [v.isInfinitePlace])
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) fun w hw ↦ by rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_1
⊢ γ < 1

Tactic:
exact Real.eulerMascheroniConstant_lt_two_thirds.trans (by norm_num)

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
f : R[X]
inst✝⁴ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝³ : Ring T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ a = e (h.map ⋯.choose)

Tactic:
← adjoinRootAlgEquiv_apply_eq_map,

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Ring S
f : R[X]
inst✝⁴ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝³ : Ring T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ a = e (h.adjoinRootAlgEquiv (h.adjoinRootAlgEquiv.symm (e.symm a)))
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
⊢ (AdjoinRoot.isAdjoinRoot f).root = root f

Tactic:
by
  simp [AdjoinRoot.isAdjoinRoot, IsAdjoinRoot.root]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((quotEquivOfEq ⋯).symm
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
            (Polynomial.map (Ideal.Quotient.mk I) Q)))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
quotEquivOfEq_symm,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))
      (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.symm
        ((quotEquivOfEq ⋯)
          ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
            (Polynomial.map (Ideal.Quotient.mk I) Q)))) =
    (⇑(((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)) ∘
        ⇑(quotAdjoinEquivQuotMap hx ⋯).symm)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ LFunction Φ s = Φ 0 * riemannZeta s

Tactic:
by
  simp only [LFunction, Nat.cast_one, one_cpow, ← singleton_eq_univ (0 : ZMod 1), sum_singleton,
    map_zero, hurwitzZeta_zero, one_mul]

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

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x ↦ Φ ↑x) s (j.val + N * m)

Tactic:
rw [toAddCircle_apply, ← (hasSum_hurwitzZeta_of_one_lt_re this hs).tsum_eq, ← mul_assoc,
    ← tsum_mul_left]

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ∑' (x : ℕ), ↑N ^ (-s) * Φ j * (1 / (↑x + ↑(↑j.val / ↑N)) ^ s) =
    ∑' (m : ℕ), LSeries.term (fun x ↦ Φ ↑x) s (j.val + N * m)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1 ∨ s ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
rcases h with h | h

Goal state after:
case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

case inr
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : s ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
by
    simp only [ε]
    split_ifs with h
    · rw [pow_zero, div_one, h, mul_one, completedLFunction,
        completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]
    · replace h : χ.Odd := χ.even_or_odd.resolve_left h
      rw [completedLFunction, completedLFunction_one_sub_odd h.to_fun,
        pow_one, h, div_I, mul_neg_one, ← neg_mul, neg_neg]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

Tactic:
rw [H, deriv_fun_mul (by fun_prop) (differentiableAt_LFunction _ s (.inl hs)), deriv_sub_const,
    deriv_id'', one_mul, add_comm]

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

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ Complex.cos ↑(π * ↑k) * (-1) ^ (k + 1) = -1

Tactic:
← ofReal_cos,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ ↑(Real.cos (π * ↑k)) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : ↑(bernoulli k) = 2 ^ k / 2 * (bernoulliFun k (1 / 2) + ↑(bernoulli k))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
rw [← inv_mul_eq_iff_eq_mul₀ (by positivity), ← sub_eq_iff_eq_add, ← sub_one_mul, inv_div] at m

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : (2 / 2 ^ k - 1) * ↑(bernoulli k) = bernoulliFun k (1 / 2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
⊢ Uc.Countable

Tactic:
apply Countable.union

Goal state after:
case hs
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if ∑ j, Φ j = 0 then ∅ else {0}).Countable

case ht
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := ⋯
G : ℂ → ℂ := ⋯
U : Set ℂ := ⋯
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := ⋯
⊢ (if Φ 0 = 0 then ∅ else {1}).Countable
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
⊢ IsPreconnected U

Tactic:
convert! (this.isConnected_compl_of_one_lt_rank ?_).isPreconnected using 1

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
⊢ U = Ucᶜ

N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
this : Uc.Countable
⊢ 1 < Module.rank ℝ ℂ
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2

Tactic:
rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]

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

Goal state before:
pp: case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * ↑s.im
h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0

Tactic:
exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s * 1 / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
mul_comm _ 1,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + 1 * LFunction 1 s / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + 1 * LFunction 1 s / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
mul_div_mul_right _ _ <| LFunction_ne_zero_of_one_le_re 1 (.inr hs₁) hs.le

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1) = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
t : ℝ
ht : 0 < t
⊢ deriv (fun t ↦ ‖↑t ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))

Tactic:
deriv_norm_ofReal_cpow _ ht,

Goal state after:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
t : ℝ
ht : 0 < t
⊢ (-s).re * t ^ ((-s).re - 1) = -s.re * t ^ (-(s.re + 1))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: r : ℝ
s : ℂ
f : ℕ → ℝ
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
hr : 0 ≤ r
hs : r < s.re
⊢ (fun n ↦ ∑ k ∈ Icc 1 n, ‖↑(f k)‖) =O[atTop] fun n ↦ ↑n ^ r

Tactic:
by simpa [abs_of_nonneg (hf _)]

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

Goal state before:
pp: case inr
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
ξ : ℝ
hξ₁ : ξ ∈ Set.Ioc 1 2
hξ₂ : (C + C') * (ξ - 1) < (↑q.totient)⁻¹
⊢ False

Tactic:
exact ((H₁ hξ₁).trans_lt hξ₂).false

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ 1 + (-s - 1) ≤ -s

Tactic:
by linarith

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤

Tactic:
have hI : I = Ideal.span {ϖ} := h.principal.choose_spec

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
⊢ (R ⧸ I) ≃ₗ[R] ↥(I ^ n) ⧸ I • ⊤
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b : ℕ
⊢ J(1 | b) = 1

Tactic:
one_left

Goal state after:
a : ℤ
e b : ℕ
⊢ 1 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
rw [_root_.pow_succ, _root_.pow_succ, mul_right, ih]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
⊢ (Set.Icc z 1).Finite

Tactic:
have := hc.elim_finite_subcover U

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
⊢ (Set.Icc z 1).Finite
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ v.restrict w ≠ 0

Tactic:
rw [← map_zero v.restrict, ne_eq, v.restrict_inj]

Goal state after:
case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ↑↑z < v w
⊢ ¬v w = v 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sZMod p i = ↑(sMod p i)

Tactic:
by
  induction i <;> push_cast [← Int.coe_nat_two_pow_pred p, sMod, sZMod, *] <;> rfl

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) ^ (q + 1) = -2

Tactic:
rw [pow_succ, one_add_α_pow_q odd leg3, mul_comm, ← _root_.sq_sub_sq, α_sq]

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ 1 ^ 2 - 3 = -2