mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a b : F
⊢ quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b

Tactic:
by
  by_cases ha : a = 0
  · rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
  -- now `a ≠ 0`
  by_cases hb : b = 0
  · rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
  -- now `a ≠ 0` and `b ≠ 0`
  have hab := mul_ne_zero ha hb
  by_cases hF : ringChar F = 2
  · -- case `ringChar F = 2`
    rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
      quadraticCharFun_eq_one_of_char_two hF hab, mul_one]
  · -- case of odd characteristic
    rw [quadraticCharFun_eq_pow_of_char_ne_two hF ha, quadraticCharFun_eq_pow_of_char_ne_two hF hb,
      quadraticCharFun_eq_pow_of_char_ne_two hF hab, mul_pow]
    rcases FiniteField.pow_dichotomy hF hb with hb' | hb'
    · simp only [hb', mul_one, if_true]
    · have h := Ring.neg_one_ne_one_of_char_ne_two hF
      -- `-1 ≠ 1`
      simp only [hb', mul_neg, mul_one, h, if_false]
      rcases FiniteField.pow_dichotomy hF ha with ha' | ha' <;>
        simp only [ha', h, neg_neg, if_true, if_false]

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

Goal state before:
pp: 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 A
inst✝³ : p.IsMaximal
P Q : Ideal B
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
inst✝ : Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
this✝ : IsScalarTower A (A ⧸ p) (B ⧸ Q)
this : Module.Finite (A ⧸ p) (B ⧸ Q)
e : (B ⧸ Ideal.map (algebraMap A B) p) ≃ₐ[A ⧸ p] (B ⧸ P) × B ⧸ Q :=
  let __spread.0 := (Ideal.quotEquivOfEq ⋯).trans (P.quotientMulEquivQuotientProd Q hPQ);
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ x, (Algebra.trace (A ⧸ p) (B ⧸ P)) x ≠ 0

Tactic:
simpa [LinearMap.ext_iff] using Algebra.trace_ne_zero (A ⧸ p) (B ⧸ P)

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

Goal state before:
pp: case pos
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 A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : P ∣ a
⊢ P ∣ differentIdeal A B

Tactic:
simpa using pow_sub_one_dvd_differentIdeal A P 2 hp
      (by rw [pow_two, ha]; exact mul_dvd_mul_left _ hPa)

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case mpr
n b : ℕ
h : 1 ≤ b
this : 1 ≤ b ^ (n - 1)
⊢ 1 ≡ b ^ (n - 1) [MOD n] → n.ProbablePrime b

Tactic:
intro h₁
    exact mod_cast Nat.ModEq.dvd h₁

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

Goal state before:
pp: case h₂.calc_4
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ∫ (x : ℝ) in 1..↑n, x⁻¹ = Real.log ↑n

Tactic:
convert! integral_inv _

Goal state after:
case e'_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑n / 1

case h₂.calc_4.convert_3
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 0 ∉ Set.uIcc 1 ↑n
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case e_a
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 = Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal

Tactic:
simp [max_comm, posLog_eq_log_max_one]

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

Goal state before:
pp: case e_a
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
⊢ (fun a ↦ log (max (↑a x) 1)) = fun v ↦ log⁺ (↑v x)

Tactic:
simp [max_comm, posLog_eq_log_max_one]

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
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)

Tactic:
by
  simp [mulHeight, hx]

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

Goal state before:
pp: α : 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
s : Finset α
⊢ v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    rw [Finset.sum_insert ha]
    grw [hv .., ih]
    refine max_le ?_ ?_
    · exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl
    · rcases isEmpty_or_nonempty s with hs | hs
      · simpa using Real.iSup_nonneg_of_nonnegHomClass v _
      exact ciSup_le fun i ↦ Finite.le_ciSup_of_le (⟨i.val, Finset.mem_insert_of_mem i.prop⟩) le_rfl

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
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
⊢ x ∘ ⇑e = Sum.elim (fun i ↦ x ↑i) 0

Tactic:
ext1 i

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
i : ↑(support x) ⊕ ↑(support x)ᶜ
⊢ (x ∘ ⇑e) i = Sum.elim (fun i ↦ x ↑i) 0 i
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x

Tactic:
mulHeight₁_eq_mulHeight

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ x • ![x⁻¹, 1] = ![1, x]

Tactic:
ext1 i

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
i : Fin (Nat.succ 0).succ
⊢ (x • ![x⁻¹, 1]) i = ![1, x] i
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] = ![x, 1] ^ n

Tactic:
ext1 i

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
i : Fin (Nat.succ 0).succ
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i
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 ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
have := (Function.ne_iff.mp h).nonempty
    refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_
    refine fun v ↦ Finite.ciSup_mono fun j ↦ ?_
    rw [show constantCoeff (p j) = coeff 0 (p j) from rfl]
    rcases eq_or_ne (coeff 0 (p j)) 0 with h₀ | h₀
    · simp [h₀]
    · exact le_sup_of_le_left <| Finite.le_ciSup_of_le ⟨0, by simp [h₀]⟩ le_rfl

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0

Tactic:
apply sum_eq_zero

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∀ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0
Module: Mathlib.NumberTheory.Height.NumberField

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

Tactic:
InfinitePlace.sum_mult_eq

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Module.finrank ℚ K = Module.finrank ℚ K
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
let p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
  have hom i : (p i).IsHomogeneous 1 := by
    fin_cases i <;> simp [p, isHomogeneous_X, IsHomogeneous.add]
  obtain ⟨C, hC₀, hC⟩ := mulHeight_eval_le' hom
  simp only [pow_one] at hC
  refine ⟨max C 1, by grind, fun a b c d ↦ ?_⟩
  by_cases hab : ![a, b] = 0
  · rw [hab, mulHeight_zero, mul_one, show a = 0 from congrFun hab 0,
      show b = 0 from congrFun hab 1,
      show ![0 * c, 0 * d + 0 * c, 0 * d] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
    grw [← one_le_mulHeight]
    grind
  by_cases hcd : ![c, d] = 0
  · rw [hcd, mulHeight_zero, mul_one, show c = 0 from congrFun hcd 0,
      show d = 0 from congrFun hcd 1,
      show ![a * 0, a * 0 + b * 0, b * 0] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
    grw [← one_le_mulHeight]
    grind
  rw [mul_assoc, mulHeight_mul_mulHeight hab hcd]
  grw [← le_max_left C 1]
  convert! hC _ with i
  fin_cases i <;> simp [p]

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

Goal state before:
pp: case inr.inl
F : Type u_1
R : Type u_2
inst✝⁴ : Field F
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Finite F
n : ℕ
inst✝ : NeZero n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
hx₀ : 1 ≠ 0
⊢ ∃ z ∈ ℤ[μ], (χ 1 - 1) * (ψ (1 - 1) - 1) = z * (μ - 1) ^ 2

Tactic:
exact ⟨0, Subalgebra.zero_mem _, by rw [χ.map_one, sub_self, zero_mul, zero_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
T : Type u_1
inst✝¹ : CommRing T
x : T
inst✝ : Algebra R T
hx' : (aeval x) f = 0
⊢ (h.liftHom x hx') h.root = x

Tactic:
rw [← lift_algebraMap_apply, lift_root]

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
hf : f ≠ 0
⊢ f ≠ 0 ∧ (aeval h.root) f = 0

Tactic:
simp [hf]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
z : S
i : ℕ
hi : i < f.natDegree
⊢ h.coeff z i = (h.basis.repr z) ⟨i, hi⟩

Tactic:
exact h.coeff_apply_lt z i hi

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ sinZeta (↑x) (2 * ↑k + 1) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
by
  rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]
  · refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_
    · rw [ofReal_tsum]
      refine tsum_congr fun n ↦ ?_
      norm_cast
      ring_nf
    · push_cast
      congr 1
      have : (Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
      rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
      apply Polynomial.map_aeval_eq_aeval_map (by simp)
  · norm_cast
    lia

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:
Nat.sub_add_cancel (by lia)

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(2 * k)! = ↑(2 * k)!
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case succ
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
⊢ ∀ (x : ℝ), f (k + 1) x = 0

Tactic:
| succ k h =>

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
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
⊢ ↑(((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx') ⋯ ⋯).trans
            (Equiv.ofBijective (fun d ↦ ⟨span {↑d}, ⋯⟩) ⋯).symm).symm
        ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
rw [Equiv.symm_trans_apply, IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_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
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
⊢ ↑((IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx').symm ⋯ ⋯)
        ((Equiv.ofBijective (fun d ↦ ⟨span {↑d}, ⋯⟩) ⋯).symm.symm ⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ 1 / -(2 * ↑π * I * ↑n) * (1 - bernoulliFourierCoeff 0 n) = -1 / (2 * ↑π * I * ↑n)

Tactic:
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑1) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1))

Tactic:
convert! this (left_mem_Ico.mpr zero_lt_one) using 1

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑1) = fun n ↦ 1 / ↑n ^ k * (fourier n) ↑0

case e'_6
k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 1) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k 0)
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case pos
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : n + 1 < m
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

pp: case neg
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : m ≤ n + 1
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m

Tactic:
· simp [hF, hm, hm.ne']

Goal state after:
case neg
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
m : ℕ
hm : m ≤ n + 1
⊢ {m | n + 1 < m}.indicator (fun m ↦ (↑n + 1) ^ ↑y * term f (↑y) m) m = F y m
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y ↦ (↑↑p)⁻¹ ^ y * (↑↑p)⁻¹ ^ (3 / 2)

Tactic:
exact Summable.mul_right _ <| summable_geometric_of_lt_one (hp₀ p).le (hp₁ p)

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

Goal state before:
pp: case pos
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 = 1 ∧ s = 1
⊢ LFunction χ s ≠ 0

Tactic:
exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2

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

Goal state before:
pp: case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), ¬n = 0 → f n = 0

Tactic:
suffices ∀ n, F n = 0 from fun n hn ↦ (hF hn).symm.trans (this n)

Goal state after:
case neg.refine_1
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
⊢ ∀ (n : ℕ), F n = 0
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

Tactic:
simp [hf]

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

Goal state before:
pp: case e'_5
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1))) =
    0 - ∫ (t : ℝ) in Set.Ioi 1, deriv (fun x ↦ ↑x ^ (-s)) t * ∑ k ∈ Icc 0 ⌊t⌋₊, f k

Tactic:
rw [zero_sub, ← integral_neg]

Goal state after:
case e'_5
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1))) =
    ∫ (a : ℝ) in Set.Ioi 1, -(deriv (fun x ↦ ↑x ^ (-s)) a * ∑ k ∈ Icc 0 ⌊a⌋₊, f k)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
rw [← LSeriesSummable_congr' s (f := fun n ↦ if n = 0 then 0 else f n)
    (by filter_upwards [eventually_ne_atTop 0] with n h using if_neg h)] at hS

Goal state after:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - ↑t * l‖ / ‖↑t‖ < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t

Tactic:
norm_real,

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
ε : ℝ
hε : 0 < ε
h_lim' : Tendsto (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) / ↑t) atTop (𝓝 l)
t : ℝ
ht₁ : 0 < t
ht₂ : ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - ↑t * l‖ / ‖t‖ < ε
⊢ ‖∑ k ∈ Icc 1 ⌊t⌋₊, f k - l * ↑t‖ < ε * t
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t ^ 1) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t ^ 1) - l * ↑t * (↑t ^ (-↑s) / ↑t ^ 1)

Tactic:
cpow_one,

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : ↑t ≠ 0
⊢ S t * (↑t ^ (-↑s) / ↑t) - l * ↑t ^ (-↑s) = S t * (↑t ^ (-↑s) / ↑t) - l * ↑t * (↑t ^ (-↑s) / ↑t)