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

Goal state before:
pp: 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))
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
have : IsCyclotomicExtension {n.lcm (torsionOrder K)} ℚ K := by
    have := hK.union_of_isPrimitiveRoot _ _ _ h
    rwa [Set.union_comm, ← IsCyclotomicExtension.iff_union_of_dvd] at this
    exact ⟨n.lcm (torsionOrder K), by simp, NeZero.ne _, Nat.dvd_lcm_left _ _⟩

Goal state after:
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
⊢ torsionOrder K = if Even n then n else 2 * n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: 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
⊢ torsionOrder K = if Even n then n else 2 * n

Tactic:
have h_main := (IsCyclotomicExtension.Rat.finrank n K).symm.trans <|
    (IsCyclotomicExtension.Rat.finrank (n.lcm (torsionOrder K)) K)

Goal state after:
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))
⊢ torsionOrder K = if Even n then n else 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
hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n
⊢ u = 1 ∨ u = -1

Tactic:
by
  replace hcong : ∃ n : ℤ, (3 : 𝓞 K) ∣ (↑u - n : 𝓞 K) := by
    obtain ⟨n, x, hx⟩ := hcong
    exact ⟨n, -η * x, by rw [← mul_assoc, mul_neg, ← neg_mul, ← lambda_sq, hx]⟩
  have := Units.mem hζ u
  fin_cases this
  · left; rfl
  · right; rfl
  all_goals exfalso
  · exact hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide) hcong
  · apply hζ.not_exists_int_prime_dvd_sub_of_prime_ne_two' (by decide)
    obtain ⟨n, x, hx⟩ := hcong
    rw [sub_eq_iff_eq_add] at hx
    refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
    simp only [Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← hx, Units.val_neg,
      IsUnit.unit_spec, RingOfIntegers.neg_mk, neg_neg]
  · exact (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
      (by decide) hcong
  · apply (hζ.pow_of_coprime 2 (by decide)).not_exists_int_prime_dvd_sub_of_prime_ne_two'
      (by decide)
    obtain ⟨n, x, hx⟩ := hcong
    refine ⟨-n, -x, sub_eq_iff_eq_add.2 ?_⟩
    have : (hζ.pow_of_coprime 2 (by decide)).toInteger = hζ.toInteger ^ 2 := by ext; simp
    simp only [this, Nat.cast_ofNat, mul_neg, Int.cast_neg, ← neg_add, ← sub_eq_iff_eq_add.1 hx,
      Units.val_neg, val_pow_eq_pow_val, IsUnit.unit_spec, neg_neg]

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

Goal state before:
pp: case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b

Tactic:
rw [add_assoc, add_comm (b ^ 3), ← add_assoc] at HF

Goal state after:
case pos
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + c ^ 3 + b ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : 3 ∣ c
⊢ 3 ∣ b
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 + c ^ 3 = 0
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ (-b) ^ 3 + (-c) ^ 3 = a ^ 3

Tactic:
rw [add_eq_zero_iff_eq_neg, ← (show Odd 3 by decide).neg_pow] at HF

Goal state after:
case neg
a b c : ℤ
ha : a ≠ 0
Hgcd : {a, b, c}.gcd id = 1
h3a : 3 ∣ a
HF : a ^ 3 + b ^ 3 = (-c) ^ 3
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
hbc : IsCoprime (-b) (-c)
h3b : ¬3 ∣ b
h3c : ¬3 ∣ c
⊢ (-b) ^ 3 + (-c) ^ 3 = a ^ 3
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : (x / y) ^ 2 = -(y / y) ^ 2
⊢ (x / y) ^ 2 = -1

Tactic:
div_self hy,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : (x / y) ^ 2 = -1 ^ 2
⊢ (x / y) ^ 2 = -1
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b * b
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset

Tactic:
← pow_two

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset
Module: Mathlib.NumberTheory.Fermat

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

Tactic:
rw [fermatNumber] at hpdvd

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

Goal state before:
pp: case e'_3.e'_5
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 = 2 - 1

pp: case e'_3.e'_6
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑(n + 1) - 1

Tactic:
· norm_num

Goal state after:
case e'_3.e'_6
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑(n + 1) - 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.a + ↑η * S.b
⊢ False

Tactic:
← pow_two

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
h : λ * λ ∣ S.a + ↑η ^ 2 * S.b
⊢ False

Tactic:
← pow_two

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 + ↑η ^ 2 * S.b
⊢ False
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) ^ (-1) / 1) - -(↑n ^ (-1) / 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
div_one,

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (-(↑n + 1) ^ (-1) - -↑n ^ (-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
x y : K
⊢ log (mulHeight₁ (x / y)) = logHeight ![x, y]

Tactic:
logHeight_eq_log_mulHeight,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x / y)) = log (mulHeight ![x, y])
Module: Mathlib.NumberTheory.Height.Basic

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

Tactic:
have H : x • ![x⁻¹, 1] = ![1, x] := by ext1 i; fin_cases i <;> simp [hx]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
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 ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1) ≤ (⨆ i, ↑v (A i)) * ⨆ i, ↑v (x i)

Tactic:
exact (isNonarchimedean _ v.prop).iSup_abv_linearMap_apply_le A x

Goal state after:
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.multiplicity ≠ 0

Tactic:
have := S.two_le_multiplicity; lia

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

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
this : ↑(Nat.card ι) ^ totalWeight K ≠ 0
⊢ log (mulHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ log (↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x)

Tactic:
exact (log_le_log <| by positivity) <| mulHeight_linearMap_apply_le ..

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight ![x * y, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
show ![x * y, 1] = ![x, 1] * ![y, 1] by ext i; fin_cases i <;> simp

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight ![x * y, 1] ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
rw [show ![x * y, 1] = ![x, 1] * ![y, 1] by ext i; fin_cases i <;> simp]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = (1 / ↑(n + 1)) ^ s / 1 * ↑(n + 1)

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
div_one,

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = (1 / ↑(n + 1)) ^ s * ↑(n + 1)

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 0
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
div_one,

Goal state after:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 - 0
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
a b : 𝓞 K
h : ↑n * a = ↑m * b
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, a})) =
    (Submodule.toAddSubgroup (span {↑n})).relIndex (Submodule.toAddSubgroup (span {↑n, b}))

Tactic:
refine (relIndex_span_span_nat_mul m hn a).trans ?_
  rw [mul_comm, mul_comm n, h]
  exact (relIndex_span_span_nat_mul n hm b).symm

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

Goal state before:
pp: case refine_1
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
⊢ ∀ (m : ℕ), 0 / 2 + 1 ≠ -↑m

pp: case refine_2
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
⊢ HasDerivAt (fun x ↦ x / 2 + 1) (1 / 2 + 0) 0

Tactic:
· simp only [zero_div]
      norm_cast
      simp

Goal state after:
case refine_2
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
⊢ HasDerivAt (fun x ↦ x / 2 + 1) (1 / 2 + 0) 0
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
⊢ logHeight (Int.cast ∘ x) = log ↑(⨆ i, |x i|)

Tactic:
logHeight_eq_log_mulHeight,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
⊢ log (mulHeight (Int.cast ∘ x)) = log ↑(⨆ i, |x i|)
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
n : ℕ
hn : n < f.natDegree
i : ℕ
hi : i < f.natDegree
⊢ (h.basis.repr (h.root ^ n)) ⟨i, hi⟩ = Pi.single n 1 i

Tactic:
calc
      h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by
        rw [h.basis_apply, Fin.val_mk]
      _ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n)
        ↑(⟨i, _⟩ : Fin _) := by
        rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single,
          Finsupp.single_apply_left Fin.val_injective]
      _ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_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 : IsAdjoinRootMonic S f
inst✝ : Nontrivial S
x : R
i : ℕ
⊢ h.coeff ((algebraMap R S) x) i = Pi.single 0 x i

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRootMonic S f
inst✝ : Nontrivial S
x : R
i : ℕ
⊢ x * Pi.single 0 1 i = Pi.single 0 x i
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

Tactic:
refine ⟨log C', fun a b c d ↦ ?_⟩

Goal state after:
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
⊢ logHeight ![a * c, a * d + b * c, b * d] ≤ log C' + logHeight ![a, b] + logHeight ![c, d]
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case pos
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 : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / 1 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
div_one,

Goal state after:
case pos
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 : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * ZMod.completedLFunction (fun j ↦ χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j) s =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s * (χ (-1) * χ⁻¹ (-1))

Tactic:
completedLFunction_const_mul

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ ↑N ^ (s - 1) * χ (-1) / ε * (χ⁻¹ (-1) * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s) =
    ↑N ^ (s - 1) / ε * gaussSum χ stdAddChar * ZMod.completedLFunction (⇑χ⁻¹) s * (χ (-1) * χ⁻¹ (-1))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
by_cases k1 : k = 1

Goal state after:
case pos
k : ℕ
k1 : k = 1
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

case neg
k : ℕ
k1 : ¬k = 1
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : (2 / 2 ^ k - 1) * ↑(bernoulli k) = bernoulliFun k (1 / 2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
rw [m, one_div]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ (1 / 1) • ∫ (x : ℝ) in 0..1, 1 • ↑(bernoulliFun k x) = 0

Tactic:
div_one,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ 1 • ∫ (x : ℝ) in 0..1, 1 • ↑(bernoulliFun k x) = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaOdd (toAddCircle (-j)) s = -completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
rw [map_neg, completedHurwitzZetaOdd_neg]

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

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

Tactic:
convert! congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq
  · rw [← Nat.cast_two, ← Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one (by lia)]
    simp [push_cast]
  · norm_cast

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

Goal state before:
pp: case inl
⊢ -1 / 2 = -↑(bernoulli' 1) / 1

Tactic:
div_one,

Goal state after:
case inl
⊢ -1 / 2 = -↑(bernoulli' 1)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inl
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
H : ℂ → ℂ := Function.update (fun s ↦ (LFunction B.χ s - LFunction B.χ 1) / (s - 1)) 1 (deriv (LFunction B.χ) 1)
⊢ B.F 1 = (G * H) 1

Tactic:
simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑n * ↑x / 1) + cexp (2 * ↑π * I * ↑(-↑n) * ↑x / 1)) / 2 =
    (cexp (↑(2 * π * ↑n) * ↑x * I) + cexp (-(↑(2 * π * ↑n) * ↑x) * I)) / 2

Tactic:
div_one,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑n * ↑x) + cexp (2 * ↑π * I * ↑(-↑n) * ↑x / 1)) / 2 =
    (cexp (↑(2 * π * ↑n) * ↑x * I) + cexp (-(↑(2 * π * ↑n) * ↑x) * I)) / 2
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑n * ↑x) + cexp (2 * ↑π * I * ↑(-↑n) * ↑x / 1)) / 2 =
    (cexp (↑(2 * π * ↑n) * ↑x * I) + cexp (-(↑(2 * π * ↑n) * ↑x) * I)) / 2

Tactic:
div_one,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑n * ↑x) + cexp (2 * ↑π * I * ↑(-↑n) * ↑x)) / 2 =
    (cexp (↑(2 * π * ↑n) * ↑x * I) + cexp (-(↑(2 * π * ↑n) * ↑x) * I)) / 2
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| s

Tactic:
← re_add_im s,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| ↑s.re + ↑s.im * I
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑x✝ * ↑x / 1) - cexp (2 * ↑π * I * ↑(-↑x✝) * ↑x / 1)) / (2 * I) =
    (cexp (-(↑(2 * π * ↑x✝) * ↑x) * I) - cexp (↑(2 * π * ↑x✝) * ↑x * I)) * I / 2

Tactic:
div_one,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * ↑↑x✝ * ↑x) - cexp (2 * ↑π * I * ↑(-↑x✝) * ↑x / 1)) / (2 * I) =
    (cexp (-(↑(2 * π * ↑x✝) * ↑x) * I) - cexp (↑(2 * π * ↑x✝) * ↑x * I)) * I / 2