mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
⊢ (logEmbedding K) (Additive.ofMul x) = 0

Tactic:
ext w

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1
w : { w // w ≠ w₀ }
⊢ (logEmbedding K) (Additive.ofMul x) w = 0 w
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R < 3
⊢ #univ ≤ #{0, 1, -1}

pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ #univ ≤ #{0, 1, -1}

Tactic:
· apply card_le_card
    rw [Finset.univ_of_card_le_two (Nat.lt_succ_iff.1 h)]
    simp

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
⊢ #univ ≤ #{0, 1, -1}
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case succ.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih : n < m → w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))
h : n < m + 1
hr : n = m
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB (m + 1))) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))

Tactic:
rw [hr]

Goal state after:
case succ.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
w : InfinitePlace K
hw : w ≠ w₁
m : ℕ
m_ih : n < m → w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB n))
h : n < m + 1
hr : n = m
⊢ w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB (m + 1))) < w ((algebraMap (𝓞 K) K) ↑(seq K w₁ hB m))
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n : ℕ
⊢ ((Algebra.norm ℤ) ↑(seq K w₁ hB n)).natAbs ≤ B

Tactic:
exact seq_norm_le K w₁ hB n

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
⊢ quadraticCharFun F a = 0 ↔ a = 0

Tactic:
by
  simp only [quadraticCharFun]
  grind

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1

Tactic:
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]

Goal state after:
case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
Module: Mathlib.NumberTheory.Harmonic.Int

Goal state before:
pp: case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ min (-↑(Nat.log 2 n)) (-↑(padicValNat 2 n.succ)) = -↑(Nat.log 2 (n + 1))

Tactic:
min_neg_neg,

Goal state after:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ -max ↑(Nat.log 2 n) ↑(padicValNat 2 n.succ) = -↑(Nat.log 2 (n + 1))
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
h : (λ ^ S.multiplicity) ^ 3 ∣ ↑S.u * S.c ^ 3
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.b

Tactic:
← S.H,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : (λ ^ S.multiplicity) ^ 3 ∣ S.a ^ 3 + S.b ^ 3
⊢ λ ^ (3 * S.multiplicity - 2) ∣ S.a + S.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
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * S.c ^ 3

Tactic:
← S.H,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = S.a ^ 3 + S.b ^ 3
Module: Mathlib.NumberTheory.Height.EllipticCurve

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
⊢ ∃ C, ∀ (x : Fin 3 → K), |(logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x| ≤ C

Tactic:
refine ⟨max C₁ (-C₂), fun x ↦ abs_sub_le_iff.mpr ⟨?_, ?_⟩⟩ <;> grind

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
⊢ ∏ᶠ (w : FinitePlace K), w ↑x = |↑((Algebra.norm ℤ) x)|⁻¹

Tactic:
simp only [← finprod_comp_equiv equivHeightOneSpectrum.symm, equivHeightOneSpectrum_symm_apply]

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)|⁻¹
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
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
⊢ t₀.Finite

Tactic:
simp only [← dvd_span_singleton, finite_factors h_span_nezero, t₀]

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

Goal state before:
pp: 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
⊢ v ((eval x) p) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N

Tactic:
by
  rcases eq_or_ne p 0 with rfl | hp₀
  · simp_all
  rw [eval_eq]
  obtain ⟨s, hs₁, hs₂⟩ :=
    hv.finset_image_add_of_nonempty (fun d ↦ coeff d p * ∏ i ∈ d.support, x i ^ d i)
      (support_nonempty.mpr hp₀)
  grw [hs₂]
  simp_rw [v.map_mul, v.map_prod, v.map_pow]
  gcongr
  · exact Real.iSup_nonneg_of_nonnegHomClass v _
  · exact Finite.le_ciSup_of_le (⟨s, hs₁⟩ : p.support) le_rfl
  · rw [hp.degree_eq_sum_deg_support hs₁, ← Finset.prod_pow_eq_pow_sum]
    gcongr with i
    exact Finite.le_ciSup (fun j ↦ v (x j)) i

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
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs,
    finprod_div_distrib (hasFiniteMulSupport_int ha) (hasFiniteMulSupport_int hb),
    prod_eq_inv_abs_norm_int ha, prod_eq_inv_abs_norm_int hb]

Goal state after:
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
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / |↑((Algebra.norm ℤ) b)|⁻¹ =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: 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

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:
· rw [← nsmul_eq_mul, ← sum_const]
    grw [v.sum_le s x]
    gcongr with i hi
    exact le_prod_max_one hi fun i ↦ v (x i)

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 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inl
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
grw [← le_max_right]
    simpa [h₀, mulHeight_zero] using one_le_pow₀ <| one_le_mulHeight x

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
⊢ t ∈ {1}ᶜ → (t - 1)⁻¹ = 0 → f t - f 1 = 0

Tactic:
ht

Goal state after:
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
⊢ (t - 1)⁻¹ = 0 → f t - f 1 = 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
ψ : AddChar F R
x : F
| χ x * φ (-x) * ψ 0

Tactic:
neg_eq_neg_one_mul x,

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
x : F
| χ x * φ (-1 * x) * ψ 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
ψ : AddChar F R
t : F
⊢ t ∈ univ \ {0} → (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t

Tactic:
ht

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
t : F
ht : t ∈ univ \ {0}
⊢ (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
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 χ φ = ∑ t ∈ univ \ {0}, (∑ x, χ t * (φ t * χ x * φ (1 - x))) * ψ t

Tactic:
simp_rw [← mul_assoc, ← MulChar.mul_apply, mul_assoc, ← mul_sum, mul_right_comm]

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 * ψ x * ∑ i, χ i * φ (1 - i)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
exact jacobiSum_mul_nontrivial hχφ ψ

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

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
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]

Goal state after:
case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ 1 ≤ max C 1 * mulHeight ![a, b]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case left
⊢ DifferentiableOn ℂ riemannZeta₀ {1}ᶜ

Tactic:
refine .congr (f := fun s ↦ riemannZeta s - (s - 1)⁻¹) ?_ (by simp +contextual [riemannZeta₀])
    exact differentiableOn_riemannZeta.fun_sub (by fun_prop (disch := grind))

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 : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
⊢ Set.BijOn RingOfIntegers.val {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}

Tactic:
refine .mk (fun x hx ↦ ?_) (fun _ _ _ _ ↦ RingOfIntegers.ext) fun a ha ↦ ?_

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
x : 𝓞 K
hx : x ∈ {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
⊢ ↑x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : a ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ B'}
⊢ a ∈ RingOfIntegers.val '' {x | ∀ (v : InfinitePlace K), v ↑x ≤ B'}
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
⊢ ((h.ofAlgEquiv e).algEquiv h'') a = (e.symm.trans (h.algEquiv h'')) a

Tactic:
algEquiv_def,

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
⊢ ((h.ofAlgEquiv e).adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv) a =
    (e.symm.trans (h.adjoinRootAlgEquiv.symm.trans h''.adjoinRootAlgEquiv)) a
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),
    Finsupp.comapDomain Fin.val (h.modByMonicHom (x + y)).toFinsupp.coeff ⋯ =
      Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp.coeff ⋯ +
        Finsupp.comapDomain Fin.val (h.modByMonicHom y).toFinsupp.coeff ⋯

Tactic:
by simp [Finsupp.comapDomain_add_of_injective Fin.val_injective]

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

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst✝ : NeZero n
⊢ LFunction χ (-(2 * ↑n)) = 0

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)

Goal state after:
N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
m : ℕ
inst✝ : NeZero m.succ
⊢ LFunction χ (-(2 * ↑m.succ)) = 0
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ.Odd
s : ℂ
⊢ χ.gammaFactor s = (s + 1).Gammaℝ

Tactic:
by
  simp [gammaFactor, hχ.not_even]

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

Goal state before:
pp: k : ℕ
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!

Tactic:
by
  rcases eq_or_ne k 0 with rfl | hk
  · simp [riemannZeta_zero]
    norm_num
  · convert riemannZeta_two_mul_nat hk
    grind [zpow_natCast]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hs₀ : s ≠ 0 := ne_zero_of_one_lt_re hs
  have hs₁ : s ≠ 1 := (lt_irrefl _ <| one_re ▸ · ▸ hs)
  -- strip down to the key equality:
  suffices ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s by
    simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]
  -- reduce to equality with un-completed L-functions:
  suffices ∑ x, Φ x * cosZeta (toAddCircle x) s = LFunction (𝓕 Φ) s by
    simpa only [cosZeta, Function.update_of_ne hs₀, ← mul_div_assoc, ← sum_div,
      LFunction_eq_completed_div_gammaFactor_even (dft_even_iff.mpr hΦ) _ (.inl hs₀),
      div_left_inj' (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]
  -- expand out `LFunction (𝓕 Φ)` and use parity:
  simp only [cosZeta_eq, ← mul_div_assoc _ _ (2 : ℂ), mul_add, ← sum_div, sum_add_distrib,
    LFunction_dft Φ (.inr hs₁), map_neg, div_eq_iff (two_ne_zero' ℂ), mul_two, add_left_inj]
  exact Fintype.sum_equiv (.neg _) _ _ (by simp [hΦ _])

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
t : ℂ
⊢ t ≠ 1 → B.F t = (riemannZeta * LFunction B.χ) t

Tactic:
ht

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : s ≠ 1
t : ℂ
ht : t ≠ 1
⊢ B.F t = (riemannZeta * LFunction B.χ) t
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
t : ℂ
⊢ t ∈ {1}ᶜ → DifferentiableAt ℂ B.F t

Tactic:
ht

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
t : ℂ
ht : t ∈ {1}ᶜ
⊢ DifferentiableAt ℂ B.F t
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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
| Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))

Tactic:
enter [3, 1]; rw [← add_zero (f _)]

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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
| f (n + 1) + 0
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
t : ℂ
⊢ 1 < t.re → F t = G t

Tactic:
ht

Goal state after:
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
t : ℂ
ht : 1 < t.re
⊢ F t = G t
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_ofPred_eq] at hs

Goal state after:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_ofPred_eq] at hs

Goal state after:
case refine_2
q : ℕ
a : ZMod q
inst✝ : NeZero q
χ : DirichletCharacter ℂ q
hχ : χ ≠ 1
s : ℂ
hs : s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), ¬LFunction χ s = 0
⊢ s ∈ {s | LFunction χ s ≠ 0}
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 : ℝ
⊢ 0 < t → deriv (fun t ↦ ‖↑t ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))

Tactic:
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
⊢ deriv (fun t ↦ ‖↑t ^ (-s)‖) t = -s.re * t ^ (-(s.re + 1))
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ∏ x ∈ Ico 1 (p / 2).succ, ↑x)

Tactic:
← prod_natCast,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ↑(∏ i ∈ Ico 1 (p / 2).succ, i))
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!

Tactic:
← prod_natCast,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) *
      ↑(∏ i ∈ Ico 1 (p / 2).succ, (↑a * ↑i).valMinAbs.natAbs) =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
⊢ T ≤ t → 0 < t → ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Tactic:
ht

Goal state after:
s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
⊢ 0 < t → ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖