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

Goal state before:
pp: case inl
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

Tactic:
by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n

Goal state after:
case pos
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∃ q, Nat.Prime q ∧ ∃ t, q ^ t = n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s

case neg
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp : ↑p ∣ (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h✝ : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 < n
h : ∀ (q : ℕ), Nat.Prime q → ∀ (t : ℕ), q ^ t ≠ n
⊢ ∃ q, Nat.Prime q ∧ ∃ t s, t ≠ 0 ∧ n = q ^ t ∧ ↑p ∣ ↑q ^ s
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp : ↑p ∣ (-2) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K

Tactic:
neg_eq_neg_one_mul,

Goal state after:
case inr
n : ℕ
hn✝ : 2 ≤ n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension {2} ℚ ↥ℚ⟮ζ⟯
hμ✝ : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp : ↑p ∣ (-1 * 2) ^ Module.finrank (↥ℚ⟮ζ⟯) K
h : (Algebra.norm ℤ) (hζ.toInteger - 1) = (Algebra.norm ℤ) (hμ✝.toInteger - 1) ^ Module.finrank (↥ℚ⟮ζ⟯) K
hn : 2 = n
⊢ ↑p ∣ ↑2 ^ Module.finrank (↥ℚ⟮ζ⟯) K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: case inr
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
if_neg (Nat.not_even_iff_odd.mpr hn)

Goal state after:
case inr
n : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : NeZero n
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
μ : ↥(torsion K)
hμ : IsPrimitiveRoot ((algebraMap (𝓞 K) K) ↑↑μ) (torsionOrder K)
h :
  IsPrimitiveRoot
    (zeta n ℚ K ^ (n / n.factorizationLCMLeft (torsionOrder K)) *
      (algebraMap (𝓞 K) K) ↑↑μ ^ (torsionOrder K / n.factorizationLCMRight (torsionOrder K)))
    (n.lcm (torsionOrder K))
this✝ : NeZero (n.lcm (torsionOrder K))
this : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K
h_main : φ n = φ (n.lcm (torsionOrder K))
hn : Odd n
⊢ torsionOrder K = 2 * n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ ∏ i, fundSystem K i ^ (x, e).2 i = 1

Tactic:
rw [← Finset.prod_empty]

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ ∏ i, fundSystem K i ^ (x, e).2 i = ∏ x ∈ ∅, ?m.196 x

K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ Type ?u.84

K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑(x, e).1 * ∏ i, fundSystem K i ^ (x, e).2 i
⊢ ?m.194 → (𝓞 K)ˣ
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ Additive.ofMul ↑(fundSystem K i) = (basisModTorsion K) i

Tactic:
simp_rw [fundSystem, ← Equiv.eq_symm_apply, Additive.ofMul_symm_eq, Quotient.out_eq']

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: n : ℤ
h : ¬3 ∣ n
⊢ ¬↑n = 0

Tactic:
ZMod.intCast_zmod_eq_zero_iff_dvd

Goal state after:
n : ℤ
h : ¬3 ∣ n
⊢ ¬↑3 ∣ n
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
⊢ legendreSym p (-a) = χ₄ ↑p * legendreSym p a

Tactic:
neg_eq_neg_one_mul,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℤ
⊢ legendreSym p (-1 * a) = χ₄ ↑p * legendreSym p a
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ χ₄ ↑(Fintype.card F) * χ₈ ↑(Fintype.card F) = χ₄ (↑(Fintype.card F)).cast * χ₈ ↑(Fintype.card F)

Tactic:
@cast_natCast _ (ZMod 4) _ _ _ (by decide : 4 ∣ 8)

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ χ₄ ↑(Fintype.card F) * χ₈ ↑(Fintype.card F) = χ₄ ↑(Fintype.card F) * χ₈ ↑(Fintype.card F)
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
⊢ legendreSym q ↑p = -legendreSym p ↑q

Tactic:
let nop := @neg_one_pow_div_two_of_three_mod_four

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
⊢ legendreSym q ↑p = -legendreSym p ↑q
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
eq_neg_iff_add_eq_zero

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

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)

Tactic:
nth_rw 2 [← one_mul (b ^ 2 - 1)] at AB_id

Goal state after:
b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
AB_id : A * B * (b ^ 2 - 1) - 1 * (b ^ 2 - 1) = b ^ (2 * p) - 1 - (b ^ 2 - 1)
⊢ (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case pos
s : Set ℕ
h0 : setGcd s = 0
⊢ ∃ t n, ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ span ↑t

Tactic:
refine ⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

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

Tactic:
let P n := n ∉ AddSubmonoid.closure s

Goal state after:
s : Set ℕ
h : setGcd s = 1 ∧ 1 ∉ s
n : ℕ
hn : ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
P : ℕ → Prop := fun n ↦ n ∉ AddSubmonoid.closure s
⊢ ∃ n, FrobeniusNumber n s
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
p : 𝓞 K
hp : Prime p
hpaηb : p ∣ 1 * S.a + ↑η * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
⊢ p ∣ λ

Tactic:
have := dvd_mul_sub_mul_mul_gcd_of_dvd hpaηb hpaηsqb

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpaηb : p ∣ 1 * S.a + ↑η * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ (1 * ↑η ^ 2 - ↑η * 1) * gcd S.a S.b
⊢ p ∣ λ
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

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

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) := ⋯
⊢ IsUnramifiedAt A P → ¬P ∣ differentIdeal A B

Tactic:
· intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count _ _ hp',
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm

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

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ((↑n + 1) ^ (-2 + 1) / (-2 + 1) - ↑n ^ (-2 + 1) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
(by norm_num : (-2 : ℝ) + 1 = -1),

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * ((↑n + 1) ^ (-1) / -1 - ↑n ^ (-1) / -1) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))
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)
i : ↑(support x) ⊕ ↑(support x)ᶜ
⊢ x (e i) = Sum.elim (fun i ↦ x ↑i) 0 i

Tactic:
cases i with
    | inl val => simp [e]
    | inr val => exact notMem_support.mp <| (Set.mem_compl_iff _ _).mp val.prop

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

Goal state before:
pp: ⊢ Tendsto (fun N ↦ termSum 1 N) atTop (𝓝 (1 - γ))

Tactic:
termSum_one,

Goal state after:
⊢ Tendsto (fun N ↦ log (↑N + 1) - ↑(harmonic (N + 1)) + 1) atTop (𝓝 (1 - γ))
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
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (mulHeight fun a ↦ x a.1 * y a.2) = mulHeight x * mulHeight y

Tactic:
rw [mulHeight_eq hx, mulHeight_eq hy, mulHeight_eq hxy, mul_mul_mul_comm, ← Multiset.prod_map_mul,
    ← finprod_mul_distrib
        (hasFiniteMulSupport_iSup_nonarchAbsVal hx) (hasFiniteMulSupport_iSup_nonarchAbsVal hy)]

Goal state after:
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
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (x i.1 * y i.2)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i.1 * y i.2) =
    (Multiset.map (fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (y i_1)) archAbsVal).prod *
      ∏ᶠ (i : ↑nonarchAbsVal), (⨆ i_1, ↑i (x i_1)) * ⨆ i_1, ↑i (y i_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
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ (mulHeight fun j ↦ constantCoeff (p j)) ≤ mulHeightBound p

Tactic:
simp only [mulHeight_eq h, mulHeightBound_eq]

Goal state after:
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_cont
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ ContinuousOn (fun x_1 ↦ (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)

Goal state after:
case h_cont.refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ ContinuousAt (fun x_1 ↦ x ^ (x_1 + 1)) s

case h_cont.refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ x ^ (s + 1) ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2.refine_2.hg
f : ℂ → ℂ := ⋯
⊢ Tendsto (fun x ↦ f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * (1 - 1)))

Tactic:
· exact ((tendsto_id.sub tendsto_const_nhds).mono_left nhdsWithin_le_nhds).const_mul _

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

Goal state before:
pp: ⊢ deriv riemannZeta 0 = -log (2 * ↑π) / 2

Tactic:
funext riemannZeta_eq_mul_completedRiemannZeta₀

Goal state after:
⊢ deriv (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1))) 0 =
    -log (2 * ↑π) / 2
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ≤ mulHeight ![↑a, ↑n]

Tactic:
mulHeight_eq (by simp [hn])

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ≤ (∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] 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 : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)

Tactic:
by
  obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)
  -- Obtain primitive additive character `ψ : F → FF'`.
  let ψ := FiniteField.primitiveChar F F' h
  -- the target field of `ψ`
  let FF' := CyclotomicField ψ.n F'
  -- Consider `χ` and `φ` as characters `F → FF'`.
  let χ' := χ.ringHomComp (algebraMap F' FF')
  let φ' := φ.ringHomComp (algebraMap F' FF')
  have hinj := (algebraMap F' FF').injective
  apply hinj
  rw [map_mul, ← jacobiSum_ringHomComp, ← jacobiSum_ringHomComp]
  have Hχφ : χ' * φ' ≠ 1 := by
    rw [← ringHomComp_mul]
    exact (MulChar.ringHomComp_ne_one_iff hinj).mpr hχφ
  have Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1 := by
    rwa [← mul_inv, inv_ne_one]
  have Hχ : χ' ≠ 1 := (MulChar.ringHomComp_ne_one_iff hinj).mpr hχ
  have Hφ : φ' ≠ 1 := (MulChar.ringHomComp_ne_one_iff hinj).mpr hφ
  have Hcard : (Fintype.card F : FF') ≠ 0 := by
    intro H
    simp only [hc, Nat.cast_pow, ne_eq, PNat.ne_zero, not_false_eq_true, pow_eq_zero_iff] at H
    exact h <| (Algebra.ringChar_eq F' FF').trans <| CharP.ringChar_of_prime_eq_zero hp H
  have H := (gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim).trans_ne Hcard
  apply_fun (gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * ·)
    using mul_right_injective₀ H
  simp only
  rw [mul_mul_mul_comm, jacobiSum_mul_nontrivial Hχφ, mul_inv, ← ringHomComp_inv,
    ← ringHomComp_inv, jacobiSum_mul_nontrivial Hχφ', map_natCast, ← mul_mul_mul_comm,
    gaussSum_mul_gaussSum_eq_card Hχ ψ.prim, gaussSum_mul_gaussSum_eq_card Hφ ψ.prim,
    ← mul_inv, gaussSum_mul_gaussSum_eq_card Hχφ ψ.prim]

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
a : S
⊢ h.adjoinRootAlgEquiv.symm a = (AdjoinRoot.mk f) (h.repr a)

Tactic:
by
  rw (occs := [1]) [AlgEquiv.symm_apply_eq, ← h.map_repr a, adjoinRootAlgEquiv_apply_mk]

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
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : S
w y : R[X]
hy : h.repr z - w = f * y
⊢ eval₂ i x (h.repr z) = eval₂ i x w

Tactic:
rw [← sub_eq_zero, ← eval₂_sub, hy, eval₂_mul, hx, zero_mul]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x ↦ χ ↑x

Tactic:
have h : {z | 1 < z.re} ∈ nhds s :=
    (isOpen_lt continuous_const continuous_re).mem_nhds hs

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : {z | 1 < z.re} ∈ 𝓝 s
⊢ LFunction χ =ᶠ[𝓝 s] LSeries fun x ↦ χ ↑x
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ℂ
hs : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun s ↦ (s - 1) * LFunctionTrivChar n s) x✝

Tactic:
by fun_prop (disch := simp_all)

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

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ ↑(-1) ^ k * (-1) ^ (k + 1) = -1

Tactic:
ofReal_neg,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ (-↑1) ^ k * (-1) ^ (k + 1) = -1
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') ⋯ ⋯).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})

Tactic:
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.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(-1) ^ k * (-↑1) ^ (k + 1) = -↑1

Tactic:
ofReal_neg,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ (-↑1) ^ k * (-↑1) ^ (k + 1) = -↑1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

pp: 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)

Tactic:
· rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]

Goal state after:
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.ZMod

Goal state before:
pp: case e_a.e_f.inr.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hΦ' : Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
simp only [hΦ', map_zero, zero_mul]

Goal state after: