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

Goal state before:
pp: p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q = -legendreSym p ↑q

pp: case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

pp: case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2

Tactic:
pow_mul,

Goal state after:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ ((-1) ^ (p / 2)) ^ (q / 2) * legendreSym p ↑q = -legendreSym p ↑q

case hp
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ p ≠ 2

case hq
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 3
hq : q % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ q ≠ 2
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ 3 ^ (2 ^ (2 ^ n - 1) * 2) = 1

Tactic:
pow_mul,

Goal state after:
case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ (3 ^ 2 ^ (2 ^ n - 1)) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ IsSquare ↑q ↔ IsSquare ↑p

Tactic:
· rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
      quadratic_reciprocity_one_mod_four hp1 hq1]

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ ↑a ^ (2 ^ n * 2) = 1

Tactic:
pow_mul,

Goal state after:
case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ (↑a ^ 2 ^ n) ^ 2 = 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ a ^ (2 * 2 ^ n) + 1 = 0

Tactic:
pow_mul,

Goal state after:
n p : ℕ
hn : 1 < n
hp : Prime p
this : Fact (Prime p)
hpdvd : ↑2 ^ 2 ^ n + 1 = 0
hp2 : p ≠ 2
hp8 : p % 8 = 1
a : ZMod p
ha : 2 = a * a
⊢ (a ^ 2) ^ 2 ^ n + 1 = 0
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.refine_1
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
⊢ S'.a ^ 3 + ↑η ^ (3 * 2) * S'.b ^ 3 = ↑S'.u * S'.c ^ 3

Tactic:
pow_mul,

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

Tactic:
rw [coe_eta, ← y_spec, ← pow_two] at 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 : λ ^ 2 ∣ S.a + ↑η * S.b
⊢ False
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.multiplicity * 3) * S.w ^ 3)

Tactic:
pow_mul,

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.u * ((λ ^ S.multiplicity) ^ 3 * S.w ^ 3)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight ![x, y] = mulHeight ![y, x]

Tactic:
show ![x, y] = ![y, x] ∘ e from List.ofFn_inj.mp rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
e : Fin 2 ≃ Fin 2 := Equiv.swap 0 1
⊢ mulHeight (![y, x] ∘ ⇑e) = mulHeight ![y, x]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x ↦ x ^ (s + 1)) x

pp: case refine_3
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ x ^ (s + 1) ≠ 0

Tactic:
· apply continuousAt_id.rpow_const (Or.inr <| by linarith)

Goal state after:
case refine_3
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ x ^ (s + 1) ≠ 0
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
i✝ : ι
hi : x i✝ ≠ 0 i✝
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
v : AbsoluteValue K ℝ
i : ι
⊢ v (Sum.elim x 0 (Sum.inl i)) ≤ ⨆ i, v (x i)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

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

Goal state before:
pp: case h₂
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
j : ι'
i : ι
x✝ : i ∈ Finset.univ
⊢ v (x i) ≤ ⨆ i, v (x i)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

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

Goal state before:
pp: case h₂
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 ι
h✝ : Nonempty ι'
j : ι'
this : ∀ (f : ι → ℝ), ⨆ i, f ↑i = ⨆ i, f i
i : ι
⊢ v (x i) ≤ ⨆ i, v (x i)

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Goal state after:
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, ∀ (x : Fin 3 → K), |(logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x| ≤ C

Tactic:
by
  obtain ⟨C₁, hC₁⟩ := logHeight_eval_le' <| isHomogeneous_addSubMap W
  obtain ⟨C₂, h⟩ := logHeight_eval_ge' (N := 2)
    fun ij ↦ (isHomogeneous_addSubMapCoeff W ij).C_mul ↑W.Δ'⁻¹
  have hC₂ := fun x ↦ h _ <| addSubMapCoeff_condition W x
  refine ⟨max C₁ (-C₂), fun x ↦ abs_sub_le_iff.mpr ⟨?_, ?_⟩⟩ <;> grind

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

Goal state before:
pp: case h₁
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)

pp: case h₂
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 ≤ ∏ i ∈ s, max (v (x i)) 1

Tactic:
· simp [hs]

Goal state after:
case h₂
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 ≤ ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ x.logHeight = log x.mulHeight

Tactic:
rw [← x.mk_rep, mulHeight_mk, logHeight_mk, Height.logHeight]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
enter [2, 2, 2]; rw [← card_range k]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
| (μ - 1) ^ #(range k)
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
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ ∏ᶠ (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:
finprod_pow F,

Goal state after:
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
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
      ∏ᶠ (i : ↑nonarchAbsVal), (⨆ i_1, ↑i (x i_1)) ^ N
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
this : ∑ x ∈ univ \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0
⊢ jacobiSum 1 χ = -1

Tactic:
simp only [jacobiSum_eq_aux, MulChar.sum_one_eq_card_units, MulChar.sum_eq_zero_of_ne_one hχ,
    add_zero, Fintype.card_eq_card_units_add_one (α := F), Nat.cast_add, Nat.cast_one,
    sub_add_cancel_left, this]

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ ∀ a ∈ {1}ᶜ, riemannZeta a = (a - 1)⁻¹ + riemannZeta₀ a

Tactic:
grind [riemannZeta_eq_inv_sub_add]

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 : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) * (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) *
      ⨆ i, v (![↑x, ↑n] i) ≤
    B

Tactic:
by
      rwa [mul_assoc, pow_sub_one_mul v.mult_ne_zero, prod_erase_mul _ _ (mem_univ v)]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = h'.map z

Tactic:
← h.algEquiv_map h'

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
h' : IsAdjoinRoot T f
z : R[X]
⊢ (h.algEquiv h') (h.map z) = ((↑(h.algEquiv h')).comp h.map) z
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
hn' : ↑n ≠ 0
a : 𝓞 K
x✝¹ : a ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
b : 𝓞 K
x✝ : b ∈ {a | mulHeight ![↑a, ↑n] ≤ B}
h : ↑a / ↑n = ↑b / ↑n
⊢ a = b

Tactic:
rwa [div_left_inj' hn', RingOfIntegers.eq_iff] at h

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
obtain ⟨f, hf⟩ := Finset.gcd_eq_sum_mul .univ x

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
hf : Finset.univ.gcd x = ∑ a, x a * f a
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ Function.Injective Fin.val

pp: case hl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ ↑(h.modByMonicHom x).toFinsupp.coeff.support ⊆ Set.range Fin.val

Tactic:
· exact Fin.val_injective

Goal state after:
case hl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
⊢ ↑(h.modByMonicHom x).toFinsupp.coeff.support ⊆ Set.range Fin.val
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case refine_1
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ Ideal.map (algebraMap R S) I ≠ ⊥

pp: case refine_2
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)} ≠ ⊥

pp: case refine_3
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑{M | M ∈ normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})} ≃
    ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}

Tactic:
· rwa [Ne, map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S), ← Ne]

Goal state after:
case refine_2
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)} ≠ ⊥

case refine_3
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑{M | M ∈ normalizedFactors (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})} ≃
    ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
ih : n < orderOf χ → gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hn₂ : n + 1 < orderOf χ
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)

Tactic:
specialize ih <| lt_trans (Nat.lt_succ_self n) hn₂

Goal state after:
case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
ih : gaussSum χ ψ ^ n = gaussSum (χ ^ n) ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
hn₂ : n + 1 < orderOf χ
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
| 1 - (↑p)⁻¹

Tactic:
rw [← cpow_neg_one]

Goal state after:
N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
| 1 - ↑p ^ (-1)
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
⊢ ZMod.completedLFunction (⇑χ) (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
completedLFunction_one_sub_odd h.to_fun,

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 ^ 1 * ZMod.completedLFunction (𝓕 ⇑χ) s
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 : ℝ) in ↑0 / ↑m..↑m / ↑m, bernoulliFun (k + 1) x = 0

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
⊢ ∀ k_1 < m, IntervalIntegrable (bernoulliFun (k + 1)) volume (↑k_1 / ↑m) (↑(k_1 + 1) / ↑m)

Tactic:
· simp [div_self m0', integral_bernoulliFun_eq_zero]

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
⊢ ∀ k_1 < m, IntervalIntegrable (bernoulliFun (k + 1)) volume (↑k_1 / ↑m) (↑(k_1 + 1) / ↑m)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)

Tactic:
by
  unfold bernoulliFourierCoeff
  rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn
      (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
      ((continuous_ofReal.comp <|
            continuous_const.mul <| Polynomial.continuous _).intervalIntegrable
        _ _)]
  simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]
  rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one,
    add_sub_cancel_left]
  congr 2
  · split_ifs <;> simp only [ofReal_one, ofReal_zero]
  · simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]

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

Goal state before:
pp: case inl
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n)) =
    -1 / (↑(2 * n) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))

Tactic:
exact_mod_cast hurwitzZeta_neg_two_mul_nat (by lia : n ≠ 0) hx

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
by
  suffices ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0 by
    rw [completedLFunction, this, mul_zero, zero_add]
  refine (hΦ.mul_even fun j ↦ ?_).sum_eq_zero
  rw [map_neg, completedHurwitzZetaEven_neg]

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

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

Tactic:
· 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 : s ≠ 0 ∨ Φ 0 = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * hurwitzZetaEven (toAddCircle j) s =
    ↑N ^ (-s) * ∑ x, Φ x * (completedHurwitzZetaEven (toAddCircle x) s / s.Gammaℝ)

Tactic:
congr 2 with i

Goal state after:
case e_a.e_f
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
i : ZMod N
⊢ Φ i * hurwitzZetaEven (toAddCircle i) s = Φ i * (completedHurwitzZetaEven (toAddCircle i) s / s.Gammaℝ)