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

Goal state before:
pp: case inl
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
inst✝ : ⊥.IsPrime
⊢ ¬⊥ ∣ differentIdeal A B ↔ IsUnramifiedAt A ⊥

pp: case inr
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
· simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L

Goal state after:
case inr
A : Type u_1
B : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : IsDomain A
inst✝⁵ : IsDedekindDomain A
inst✝⁴ : IsDedekindDomain B
inst✝³ : IsTorsionFree A B
inst✝² : Module.Finite A B
inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
P : Ideal B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
P : ℕ → Prop := fun n ↦ n ∉ AddSubmonoid.closure s
⊢ ∃ n, FrobeniusNumber n s

Tactic:
have : P 1 := h.2 ∘ one_mem_closure_iff.mp

Goal state after:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
P : ℕ → Prop := fun n ↦ n ∉ AddSubmonoid.closure s
this : P 1
⊢ ∃ n, FrobeniusNumber n s
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)

Tactic:
h,

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j = 0
⊢ ↑v 0 ≤ ⨆ i, ↑v (x ↑i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case insert.refine_2.inl
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
hs : IsEmpty ↥s
⊢ ⨆ i, v (l ↑i) ≤ ⨆ i, v (l ↑i)

pp: case insert.refine_2.inr
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
hs : Nonempty ↥s
⊢ ⨆ i, v (l ↑i) ≤ ⨆ i, v (l ↑i)

Tactic:
· simpa using Real.iSup_nonneg_of_nonnegHomClass v _

Goal state after:
case insert.refine_2.inr
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
hs : Nonempty ↥s
⊢ ⨆ i, v (l ↑i) ≤ ⨆ i, v (l ↑i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
hp.degree_eq_sum_deg_support hs₁,

Goal state after:
case h₂
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ ∑ i ∈ s.support, s i
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases isEmpty_or_nonempty ι with hι | hι
  · simp
  rcases eq_or_ne x 0 with rfl | hx
  · simpa using one_le_mulHeight y
  rcases eq_or_ne y 0 with rfl | hy
  · simpa using one_le_mulHeight x
  rw [← mulHeight_fun_mul_eq hx hy,
    show x * y = (fun a ↦ x a.1 * y a.2) ∘ Function.diag by ext1; simp]
  exact mulHeight_comp_le ..

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) * ↑((Algebra.norm ℤ) b) = ↑((Algebra.norm ℤ) a)

Tactic:
rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]

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

Goal state before:
pp: 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
⊢ max (v (∑ i ∈ s, x i)) 1 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

Tactic:
refine sup_le ?_ ?_

Goal state after:
case refine_1
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
⊢ v (∑ i ∈ s, x i) ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

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
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ totalWeight K = ∑ v, v.mult

Tactic:
by
  simp only [totalWeight]
  convert! sum_archAbsVal_eq (fun _ ↦ (1 : ℕ))
  · rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]
  · simp

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

Goal state before:
pp: case inl
h : riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)
⊢ riemannZeta 1 = (starRingEnd ℂ) (riemannZeta 1)

Tactic:
h,

Goal state after:
case inl
h : riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)
⊢ ↑((γ - Real.log (4 * π)) / 2) = (starRingEnd ℂ) ↑((γ - Real.log (4 * π)) / 2)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N

Tactic:
· -- nonarchimedean part: reduce to "local" statement `eval_mvPolynomial_le`
    have := (Function.ne_iff.mp h₀).nonempty
    have F := hasFiniteMulSupport_iSup_nonarchAbsVal hx
    rw [finprod_pow F, ← finprod_mul_distrib (by fun_prop) (by fun_prop)]
    refine finprod_le_finprod (by fun_prop)
      (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
      (fun j ↦ ?_) ?_
    · grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
      gcongr
      · exact HH₁ v.val
      · grw [← HH₂, ← le_max_left]
    · exact mul_nonneg (iSup_nonneg fun _ ↦ by positivity) <| by simp only [HH₁]

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

Goal state before:
pp: ⊢ ∀ a ∈ {1}ᶜ,
    riemannZeta₁ a ≠ 0 → deriv riemannZeta a / riemannZeta a = -(a - 1)⁻¹ + deriv riemannZeta₁ a / riemannZeta₁ a

Tactic:
grind [deriv_riemannZeta_eq_neg_inv_sub_sq_mul_add, riemannZeta_eq_inv_sub_mul]

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
⊢ Function.Surjective ⇑h.map

Tactic:
exact h.map_surjective

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
⊢ {x | IsIntegral ℤ (↑n * x) ∧ mulHeight₁ x ≤ B}.Finite

Tactic:
have hn' : (n : K) ≠ 0 := mod_cast hn
  suffices Set.BijOn (fun a : 𝓞 K ↦ (a / n : K)) {a | mulHeight ![(a : K), n] ≤ B}
      {x | IsIntegral ℤ (n * x) ∧ mulHeight₁ x ≤ B} from
    this.finite_iff_finite.mp <| finite_setOfPred_mulHeight_nat_le hn B
  refine .mk (fun a ha ↦ ?_) (fun a _ b _ h ↦ ?_) fun x ⟨hx₁, hx₂⟩ ↦ ?_
  · simp only [Set.mem_ofPred_eq] at ha ⊢
    rw [mul_div_cancel₀ (a : K) hn', mulHeight₁_div_eq_mulHeight]
    exact ⟨a.isIntegral_coe, ha⟩
  · rwa [div_left_inj' hn', RingOfIntegers.eq_iff] at h
  · simp only [Set.mem_ofPred_eq, Set.mem_image]
    obtain ⟨a, ha⟩ : ∃ a : 𝓞 K, n * x = a := ⟨⟨_, hx₁⟩, rfl⟩
    refine ⟨a, ?_, (EuclideanDomain.eq_div_of_mul_eq_right hn' ha).symm⟩
    rwa [← ha, ← mulHeight₁_div_eq_mulHeight, mul_div_cancel_left₀ x hn']

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 : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree

Tactic:
· rw [Finsupp.mapDomain_apply Fin.val_injective]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j / ↑N))

Tactic:
rw [(by ring : Φ j / N = Φ j * (1 / N * 1)), one_div, ← cpow_neg_one]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (↑N ^ (-1) * 1)))
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.conductor = N
s : ℂ
hN : N ≠ 1
h : χ = 1
⊢ 1 = N

Tactic:
h,

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : conductor 1 = N
s : ℂ
hN : N ≠ 1
h : χ = 1
⊢ 1 = N
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

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

Tactic:
h,

Goal state after:
case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * 1 * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

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

Tactic:
h,

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

Goal state before:
pp: case pos
k : ℕ
h : k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 1

Tactic:
h,

Goal state after:
case pos
k : ℕ
h : k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' 1) = ↑(bernoulli 1) + 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x y : ℝ
⊢ bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, ↑(k + 1) * bernoulliFun k t

Tactic:
by
  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt, add_sub_cancel]
  · exact fun y _ ↦ hasDerivAt_bernoulliFun _ y
  · exact Continuous.intervalIntegrable (by fun_prop) _ _

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∑ x ∈ Finset.range m, ∫ (x : ℝ) in ↑x / ↑m..↑(x + 1) / ↑m, bernoulliFun (k + 1) x = 0

Tactic:
rw [intervalIntegral.sum_integral_adjacent_intervals]

Goal state after:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∫ (x : ℝ) in ↑0 / ↑m..↑m / ↑m, bernoulliFun (k + 1) x = 0

m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∀ k_1 < m, IntervalIntegrable (bernoulliFun (k + 1)) volume (↑k_1 / ↑m) (↑(k_1 + 1) / ↑m)
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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
by
  unfold normalizedFactorsMapEquivNormalizedFactorsMinPolyMk
    Ideal.normalizedFactorsEquivSpanNormalizedFactors
  rw [Equiv.symm_trans_apply, IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm]
  unfold IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv
  rw [Equiv.coe_fn_mk, Equiv.symm_symm, Equiv.ofBijective_apply]
  dsimp only
  unfold IsDedekindDomain.idealFactorsEquivOfQuotEquiv
  rw [OrderIso.ofHomInv_apply]
  erw [IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe]
  dsimp only
  rw [map_span, image_singleton, map_span, image_singleton, coe_coe,
    quotMapEquivQuotQuotMap_symm_apply, span_union, span_eq, sup_comm,
    ← image_singleton, ← map_span, Ideal.comap_map_of_surjective' _ Ideal.Quotient.mk_surjective,
    Ideal.mk_ker]

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (↑a ^ n / ↑n).re + 4 * ((↑a * z) ^ n / ↑n).re + ((↑a * z ^ 2) ^ n / ↑n).re

Tactic:
simp only [← ofReal_pow, div_natCast_re, ofReal_re, mul_pow, mul_re, ofReal_im, zero_mul,
    sub_zero]

Goal state after:
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable F''

Tactic:
suffices Summable fun (pk : Nat.Primes × ℕ) ↦ (pk.1 : ℝ)⁻¹ ^ (pk.2 + 3 / 2 : ℝ) by
    refine (Summable.mul_left 2 this).of_nonneg_of_le (fun pk ↦ ?_) (fun pk ↦ F''_le pk.1 pk.2)
    simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]
    positivity [vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))]

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))

Tactic:
have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha

Goal state after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ (s - 1) * ε * ∫ (a : ℝ) in Set.Ioi T, a ^ (-s) ≤ (s - 1) * ε * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)

Tactic:
refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)

Goal state after:
case refine_1
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ IntegrableOn (fun a ↦ a ^ (-s)) (Set.Ioi 1) volume

case refine_2
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ 0 ≤ᵐ[volume.restrict (Set.Ioi 1)] fun a ↦ a ^ (-s)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₁ % ↑b | b) = J(a₂ | b)

Tactic:
h,

Goal state after:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₂ % ↑b | b) = J(a₂ | b)
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
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ ϖ ≠ 0

Tactic:
contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y

Tactic:
h,

Goal state after:
case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * (qrSign m n * x)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y

Tactic:
h,

Goal state after:
case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * (qrSign m n * y) = y
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H K : Subgroup G
hHK : H ≤ K
inst✝ : H.IsFiniteRelIndex K
this : (H.subgroupOf K).FiniteIndex
⊢ DiscreteTopology ↥H ↔ DiscreteTopology ↥K

Tactic:
rw [← (subgroupOfContinuousMulEquivOfLe hHK).discreteTopology_iff,
    discreteTopology_iff_of_finiteIndex]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
rw [mul_add, ← pow_add ω, t, ← mul_pow ω ωb (2 ^ p'), ω_mul_ωb, one_pow] at h

Goal state after:
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ (p' + 1) + 1 = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p'
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
replace h := eq_sub_of_add_eq h

Goal state after:
case h
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
this :
  ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [inst_3 : TopologicalSpace G]
    [OrderTopology G] (g : G), 1 ≤ g → DiscreteTopology ↥(zpowers g)
ha : ¬1 ≤ g
⊢ DiscreteTopology ↥(zpowers g)

Tactic:
specialize this g⁻¹ (one_le_inv'.mpr (le_of_not_ge ha))
    rwa [zpowers_inv] at this

Goal state after: