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

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsPrincipalIdealRing (𝓞 K)

Tactic:
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
  rw [discr_prime 3 K, IsCyclotomicExtension.finrank (n := 3) K
    (irreducible_rat (by simp)), nrComplexPlaces_eq_totient_div_two 3, totient_prime
      Nat.prime_three]
  simp only [Int.reduceNeg, succ_sub_succ_eq_sub, tsub_zero, zero_lt_two, Nat.div_self, pow_one,
    cast_ofNat, neg_mul, one_mul, abs_neg, Int.cast_abs, Int.cast_ofNat,
    abs_of_pos (zero_lt_three' ℝ), factorial_two]
  suffices (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2 from
    lt_trans (by norm_num) this
  gcongr
  exact pi_gt_three

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

Goal state before:
pp: case isIntegral_iff
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x✝ : K
this :
  Subalgebra.map (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ℤ[hζ.toInteger] =
    Subalgebra.map (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ⊤
⊢ IsIntegral ℤ x✝ ↔ ∃ y, (algebraMap (↥ℤ[ζ]) K) y = x✝

Tactic:
simp only [AlgHom.map_adjoin_singleton, IsScalarTower.coe_toAlgHom', RingOfIntegers.map_mk,
      Algebra.map_top] at this

Goal state after:
case isIntegral_iff
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x✝ : K
this : ℤ[ζ] = (IsScalarTower.toAlgHom ℤ (𝓞 K) K).range
⊢ IsIntegral ℤ x✝ ↔ ∃ y, (algebraMap (↥ℤ[ζ]) K) y = x✝
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case isIntegral_iff
n : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x✝ : K
this : ℤ[ζ] = (IsScalarTower.toAlgHom ℤ (𝓞 K) K).range
⊢ IsIntegral ℤ x✝ ↔ ∃ y, (algebraMap (↥ℤ[ζ]) K) y = x✝

Tactic:
simp [IsIntegralClosure.isIntegral_iff (A := 𝓞 K), this, ← SetLike.mem_coe]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := ⋯
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := ⋯
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x

Tactic:
exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
right; left
    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
    rw [RingHom.map_sub, h, RingHom.map_one, sub_self]

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

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
subst hc

Goal state after:
case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
subst hc
    simp only [eq_iff_true_of_subsingleton, exists_const]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) = (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * quadraticCharFun F b

Tactic:
quadraticCharFun_eq_pow_of_char_ne_two hF hb,

Goal state after:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
ha : ¬a = 0
hb : ¬b = 0
hab : a * b ≠ 0
hF : ¬ringChar F = 2
⊢ quadraticCharFun F (a * b) =
    (if a ^ (Fintype.card F / 2) = 1 then 1 else -1) * if b ^ (Fintype.card F / 2) = 1 then 1 else -1
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) ≠ 2
⊢ ↑(legendreSym p a) = ↑a ^ (p / 2)

Tactic:
convert! quadraticChar_eq_pow_of_char_ne_two' hc (a : ZMod p)
    exact (card p).symm

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
⊢ (quadraticChar (ZMod p)) (↑a ^ 2) = 1

Tactic:
exact quadraticChar_sq_one' ha

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

Goal state before:
pp: case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
⊢ n ∈ P

Tactic:
have prime : p.Prime := Nat.prime_iff_not_exists_mul_eq.mpr <| .intro (by lia)
    fun ⟨m, n, hm, hn, eq⟩ ↦ have := mul_ne_zero_iff.mp (eq ▸ hp0)
    (h.mem_or_mem (eq ▸ hp)).elim (Nat.find_min h0 hm ⟨·, this.1⟩) (Nat.find_min h0 hn ⟨·, this.2⟩)

Goal state after:
case refine_2
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ p, Nat.Prime p ∧ P = span {p}
n : ℕ
hn : n ∈ maximalIdeal ℕ
p : ℕ := Nat.find h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
⊢ n ∈ P
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1
s✝ : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s✝.length
s : RelSeries {(a, b) | a < b} := RelSeries.take s✝ ⟨3, ⋯⟩
this : NeZero s.length
⊢ False

Tactic:
have h1 : ⊥ < (s 1).asIdeal := bot_le.trans_lt (s.step 0)

Goal state after:
case refine_1
s✝ : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s✝.length
s : RelSeries {(a, b) | a < b} := RelSeries.take s✝ ⟨3, ⋯⟩
this : NeZero s.length
h1 : ⊥ < (s.toFun 1).asIdeal
⊢ False
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
b : ℕ
h✝ : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
h : ∃ p, b * (b ^ 2 - 1) + 1 + m ≤ p ∧ Prime p
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
obtain ⟨p, ⟨hp₁, hp₂⟩⟩ := 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
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
Module: Mathlib.NumberTheory.HeckeRing.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
Δ : Submonoid G
H₁ H₂ : Subgroup G
h : IsHeckeTriple Δ H₁ H₂
⊢ Δ ≤ (commensurator H₂).toSubmonoid

Tactic:
exact h.le_commensurator_right

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr.mpr
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 ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ :
  Ideal.map (algebraMap A B) (Ideal.under A P) =
    P ^ Multiset.count P (UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap A B) (Ideal.under A P))) *
      Q
⊢ ¬P ∣ differentIdeal A B

Tactic:
← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count _ _ hp',

Goal state after:
case inr.mpr
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 ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
H : IsUnramifiedAt A P
Q : Ideal B
h₁ : P ⊔ Q = ⊤
h₂ : Ideal.map (algebraMap A B) (Ideal.under A P) = P ^ P.ramificationIdx A * Q
⊢ ¬P ∣ differentIdeal A B
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime S.y (S.Z ^ 3 * ↑S.u₃)

Tactic:
Z_u₃_spec

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime S.y S.z
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.x * λ ^ (3 * S.multiplicity - 2) + S.y * λ * ↑η + S.z * λ * ↑η ^ 2 = 0

Tactic:
mul_comm S.x,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ^ (3 * S.multiplicity - 2) * S.x + S.y * λ * ↑η + S.z * λ * ↑η ^ 2 = 0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
a b : 𝓞 K
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b ≠ 0

Tactic:
exact mul_ne_zero ha hb

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
⊢ ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0

Tactic:
intro a ha

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal
⊢ a ≠ 0
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ log ((Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)

Tactic:
rw [log_mul (left_ne_zero_of_mul H) (right_ne_zero_of_mul H), log_multiset_prod this,
    Multiset.map_map, log_finprod (fun _ ↦ by positivity)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ (Multiset.map ((fun x ↦ log x) ∘ fun v ↦ max (v x) 1) archAbsVal).sum + ∑ᶠ (a : ↑nonarchAbsVal), log (max (↑a x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
⊢ logHeight (x ∘ ⇑e) = logHeight x

Tactic:
simp only [logHeight_eq_log_mulHeight, mulHeight_comp_equiv]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
rcases isEmpty_or_nonempty ι

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : IsEmpty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) n = (fun N ↦ -↑(harmonic (N + 1)) + log (↑N + 1)) n

Tactic:
simp_rw [Function.comp_apply, eulerMascheroniSeq', reduceCtorEq, if_false]

Goal state after:
this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(↑(harmonic (n + 1)) - log ↑(n + 1)) = -↑(harmonic (n + 1)) + log (↑n + 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
⊢ max (mulHeightBound 0) 1 = 1

Tactic:
by
  simp only [mulHeightBound_eq, Pi.zero_apply, support_zero, coeff_zero, AbsoluteValue.map_zero,
    Real.iSup_of_isEmpty, zero_le_one, sup_of_le_right, AddMonoidAlgebra.coeff_zero,
    Finsupp.sum_zero_index, Real.iSup_const_zero, Multiset.map_const', Multiset.prod_replicate,
    sup_eq_right, zero_pow_eq]
  rcases isEmpty_or_nonempty ι'
  · split_ifs
    · simpa using finprod_zero_le_one
    · simp
  · simp
    grind

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

Goal state before:
pp: case c0
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1

Tactic:
exact finprod_nonneg fun _ ↦ by positivity

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

Goal state before:
pp: case refine_2
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ IntegrableOn (fun x ↦ (x - ↑(n + 1)) / x ^ (1 + 1)) (Ioc (↑(n + 1)) (↑(n + 1) + 1)) volume

pp: case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
· exact (term_welldef n.succ_pos zero_lt_one).1

Goal state after:
case refine_3
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ (x - ↑(n + 1)) / x ^ (s + 1) ≤ (x - ↑(n + 1)) / x ^ (1 + 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ (↑n).arg ≠ π

Tactic:
rw [natCast_arg]

Goal state after:
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ 0 ≠ π
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ x * χ⁻¹ (1 - x)

Tactic:
MulChar.inv_apply',

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ x * χ (1 - x)⁻¹
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, (∑ y, χ (x * y) * φ (x - x * y)) * ψ x

Tactic:
← mul_one_sub,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, (∑ x_1, χ (x * x_1) * φ (x * (1 - x_1))) * ψ x
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
p : R[X]
⊢ p ∈ RingHom.ker h.map ↔ f ∣ p

Tactic:
rw [h.ker_map, Ideal.mem_span_singleton]

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

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum 1 ψ = -1 + z * (μ - 1) ^ 2

Tactic:
hψ₀,

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum 1 1 = -1 + z * (μ - 1) ^ 2
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✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : z - h.map w = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
← h.map_repr z,

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✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w : R[X]
hzw : h.map (h.repr z) - h.map w = 0
⊢ eval₂ i x (h.repr z) = eval₂ i x w
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ψ = 1
⊢ jacobiSum ψ χ = -1 + 0 * (μ - 1) ^ 2

Tactic:
hψ₀,

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ψ = 1
⊢ jacobiSum 1 χ = -1 + 0 * (μ - 1) ^ 2
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
x y : S
⊢ h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f

Tactic:
conv_lhs =>
      rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 2 * ↑k = ↑(2 * k - 1) + 1

Tactic:
{ norm_cast; lia }

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
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)⁻¹, ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) = 0

Tactic:
intervalIntegral.integral_finsetSum

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
⊢ ∑ i ∈ Finset.range m, ∫ (x : ℝ) in 0..(↑m)⁻¹, bernoulliFun (k + 1) (x + ↑i / ↑m) = 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
⊢ ∀ i ∈ Finset.range m, IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0 (↑m)⁻¹
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ ∑ i, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) +
      ∑ i, ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    ∑ i, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s)) +
      ∑ i, a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))

Tactic:
congr with i

Goal state after:
case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaEven (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaEven (toAddCircle i) s))

case e_a.e_f
N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
i : ZMod N
⊢ ↑N ^ (-s) * (a * Φ i * completedHurwitzZetaOdd (toAddCircle i) s) =
    a * (↑N ^ (-s) * (Φ i * completedHurwitzZetaOdd (toAddCircle i) s))
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
⊢ 0 ≤ χ.zetaMul 0

Tactic:
simp only [ArithmeticFunction.map_zero, le_refl]

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ ((↑n + 1) ^ ↑x * term f (↑x) (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) n_1) =
    f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
pow_mul_term_eq f x n

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ (f (n + 1) + ∑' (n_1 : ℕ), if n_1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) n_1) = f (n + 1) + ∑' (m : ℕ), F x m
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0

Tactic:
· exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * I * completedLFunction (𝓕 Φ) t
hF : Differentiable ℂ F
hG : Differentiable ℂ G
this : {z | 1 < z.re} ∈ 𝓝 2
⊢ F =ᶠ[𝓝 2] G

Tactic:
filter_upwards [this] with t ht
    using completedLFunction_one_sub_of_one_lt_odd hΦ ht

Goal state after: