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

Goal state before:
pp: case h
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b ∧ m ≤ b.psp_from_prime p

Tactic:
constructor

Goal state after:
case h.left
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ (b.psp_from_prime p).FermatPsp b

case h.right
b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
h₃ : 0 < b ^ 2 - 1
h₄ : 0 < b * (b ^ 2 - 1)
h₅ : b * (b ^ 2 - 1) < p
h₆ : ¬p ∣ b * (b ^ 2 - 1)
h₇ : b ≤ b * (b ^ 2 - 1)
h₈ : 2 ≤ b * (b ^ 2 - 1)
h₉ : 2 < p
h₁₀ : p < b.psp_from_prime p
⊢ m ≤ b.psp_from_prime p
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.y * λ * ↑η + S.z * λ * ↑η ^ 2 = 0

Tactic:
mul_comm S.y,

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.y * ↑η + S.z * λ * ↑η ^ 2 = 0
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
hx : x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| ne_iff.mp hx

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this : Nonempty { j // x j ≠ 0 }
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hg
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ IntervalIntegrable (fun x ↦ ↑n * (1 / x ^ 2)) volume (↑n) (↑n + 1)

Tactic:
exact (intervalIntegral.intervalIntegrable_one_div
          (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne') (by fun_prop)).const_mul _

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

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ((↑n ^ (s - 1))⁻¹ - (↑n + 1) ^ (-(s - 1))) / (s - 1) = ((↑n ^ (s - 1))⁻¹ - 1 / (↑n + 1) ^ (s - 1)) / (s - 1)

Tactic:
rpow_neg (by linarith),

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ((↑n ^ (s - 1))⁻¹ - ((↑n + 1) ^ (s - 1))⁻¹) / (s - 1) = ((↑n ^ (s - 1))⁻¹ - 1 / (↑n + 1) ^ (s - 1)) / (s - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n ^ s)⁻¹ - (↑n + 1) ^ (-s)) / s) = ↑n * (((↑n ^ s)⁻¹ - 1 / (↑n + 1) ^ s) / s)

Tactic:
rpow_neg (by linarith),

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n ^ s)⁻¹ - ((↑n + 1) ^ s)⁻¹) / s) = ↑n * (((↑n ^ s)⁻¹ - 1 / (↑n + 1) ^ s) / s)
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
⊢ jacobiSum 1 χ = -1

Tactic:
by
  classical
  have : ∑ x ∈ univ \ {0, 1}, ((1 : MulChar F R) x - 1) * (χ (1 - x) - 1) = 0 := by
    apply Finset.sum_eq_zero
    simp +contextual only [mem_sdiff, mem_univ, mem_insert, mem_singleton,
      not_or, ← isUnit_iff_ne_zero, true_and, MulChar.one_apply, sub_self, zero_mul,
      implies_true]
  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: 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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -(log (2 * ↑π) * 2) = ↑γ - log (2 * 2 * ↑π) + (-log ↑π + -↑γ)

Tactic:
rw [log_mul (by positivity) (by positivity) (by simp [arg, LT.lt.le, Real.pi_pos])]

Goal state after:
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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - log (2 * 2 * ↑π) + (-log ↑π + -↑γ)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ (fun v ↦ ⨆ i, v ↑(![a, ↑n] i)) = fun v ↦ ⨆ i, v (![↑a, ↑n] i)

Tactic:
ext

Goal state after:
case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ ⨆ i, x✝ ↑(![a, ↑n] i) = ⨆ i, x✝ (![↑a, ↑n] i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: 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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - log (2 * 2 * ↑π) + (-log ↑π + -↑γ)

Tactic:
rw [log_mul (by positivity) (by positivity) (by simp [arg, LT.lt.le, Real.pi_pos])]

Goal state after:
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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - (log (2 * 2) + log ↑π) + (-log ↑π + -↑γ)
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
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
rw [hab, mulHeight_zero, mul_one, show a = 0 from congrFun hab 0,
      show b = 0 from congrFun hab 1,
      show ![0 * c, 0 * d + 0 * c, 0 * d] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
    grw [← one_le_mulHeight]
    grind

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

Goal state before:
pp: 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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - (log (2 * 2) + log ↑π) + (-log ↑π + -↑γ)

Tactic:
rw [log_mul (by positivity) (by positivity) (by simp [arg, LT.lt.le, Real.pi_pos])]

Goal state after:
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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - (log 2 + log 2 + log ↑π) + (-log ↑π + -↑γ)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case neg
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:
mulHeight_mul_mulHeight hab hcd

Goal state after:
case neg
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 * c, a * d, b * c, b * d]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: 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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - (log 2 + log 2 + log ↑π) + (-log ↑π + -↑γ)

Tactic:
rw [log_mul (by positivity) (by positivity) (by simp [arg, LT.lt.le, Real.pi_pos])]

Goal state after:
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
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
⊢ -((log 2 + log ↑π) * 2) = ↑γ - (log 2 + log 2 + log ↑π) + (-log ↑π + -↑γ)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ DifferentiableOn ℂ riemannZeta₀ {1}ᶜ ∧ Tendsto riemannZeta₀ (𝓝[≠] 1) (𝓝 (riemannZeta₀ 1))

Tactic:
constructor

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

case right
⊢ Tendsto riemannZeta₀ (𝓝[≠] 1) (𝓝 (riemannZeta₀ 1))
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
⊢ aeval h.root = h.map

Tactic:
ext

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
⊢ (aeval h.root) X = h.map X
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
⊢ (↑(h.algEquiv h')).comp h.map = h'.map

Tactic:
ext

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
⊢ ((↑(h.algEquiv h')).comp h.map) X = h'.map X
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
⊢ h.algEquiv h = AlgEquiv.refl

Tactic:
ext

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
a✝ : S
⊢ (h.algEquiv h) a✝ = AlgEquiv.refl 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 : IsAdjoinRoot S f
T : Type u_1
inst✝³ : Ring T
inst✝² : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
⊢ (h.algEquiv h').trans (h'.algEquiv h'') = h.algEquiv h''

Tactic:
ext

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
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
a✝ : S
⊢ ((h.algEquiv h').trans (h'.algEquiv h'')) a✝ = (h.algEquiv h'') 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 : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
e : S ≃ₐ[R] T
⊢ RingHom.ker ((↑e).comp h.map) = Ideal.span {f}

Tactic:
ext

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
e : S ≃ₐ[R] T
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker ((↑e).comp h.map) ↔ x✝ ∈ Ideal.span {f}
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
H : {x | mulHeight₁ x ≤ B} = ⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}
⊢ (⋃ n, {x | IsIntegral ℤ ((↑↑n + 1) * x) ∧ mulHeight₁ x ≤ B}).Finite

Tactic:
exact Set.finite_iUnion fun n ↦
    mod_cast finite_setOfPred_isIntegral_nat_mul_and_mulHeight₁_le K (Nat.zero_ne_add_one n).symm B

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
⊢ RingHom.ker (mkₐ f) = Ideal.span {f}

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (mkₐ f) ↔ x✝ ∈ Ideal.span {f}
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f : R[X]
⊢ (AdjoinRoot.isAdjoinRoot f).root = root f

Tactic:
simp [AdjoinRoot.isAdjoinRoot, IsAdjoinRoot.root]

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

Goal state before:
pp: 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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ C * (mulHeight ![a✝, b✝] * mulHeight ![c✝, d✝]) ≤ mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]

Tactic:
mulHeight_mul_mulHeight hab hcd

Goal state after:
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]
q : Fin 4 × Fin 3 → MvPolynomial (Fin 4) K :=
  Function.uncurry ![![X 0, 0, 0], ![0, X 1, -X 0], ![0, X 2, -X 0], ![0, 0, X 3]]
hom : ∀ (a : Fin 4 × Fin 3), (q a).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC :
  ∀ (p : Fin 3 → MvPolynomial (Fin 4) K) {x : Fin 4 → K},
    (∀ (k : Fin 4), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (1 + 1)) →
      C * mulHeight x ≤ mulHeight fun j ↦ (eval x) (p j)
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ C * mulHeight ![a✝ * c✝, a✝ * d✝, b✝ * c✝, b✝ * d✝] ≤ mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ RingHom.ker (aeval α) = Ideal.span {minpoly R α}

Tactic:
ext

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (aeval α) ↔ x✝ ∈ Ideal.span {minpoly R α}
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ LFunction χ = riemannZeta

Tactic:
ext

Goal state after:
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ LFunction χ x✝ = riemannZeta x✝
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_1
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ AnalyticOnNhd ℂ (LFunction ((changeLevel hMN) χ)) {1}ᶜ

Tactic:
refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Goal state after:
case refine_1
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableWithinAt ℂ (LFunction ((changeLevel hMN) χ)) {1}ᶜ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
⊢ AnalyticOnNhd ℂ (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) {1}ᶜ

Tactic:
refine DifferentiableOn.analyticOnNhd (fun s hs ↦ ?_) isOpen_compl_singleton

Goal state after:
case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableWithinAt ℂ (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) {1}ᶜ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ completedLFunction χ = completedRiemannZeta

Tactic:
ext

Goal state after:
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ completedLFunction χ x✝ = completedRiemannZeta x✝
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
hj : j ≠ 0
⊢ Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
    Φ j *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))

Tactic:
rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : {y}.prod = Ideal.map (algebraMap R S) I
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
Multiset.prod_singleton

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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ Irreducible (Ideal.map (algebraMap R S) I)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ 1 - s ≠ 0

Tactic:
by rwa [sub_ne_zero, ne_comm]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1
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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s

Tactic:
have hG : Differentiable ℂ G := by
    apply (((differentiable_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul_const _).mul
    rw [← dft_odd_iff] at hΦ
    exact differentiable_completedLFunction hΦ.map_zero hΦ.sum_eq_zero

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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * I * completedLFunction (𝓕 Φ) s
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
⊢ LFunction χ s ≠ 0

Tactic:
by_cases h : χ ^ 2 = 1 ∧ s = 1
  · exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2
  · have hs' : s = 1 + I * s.im := by
      conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
    rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h
    replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 :=
      h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)
    exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h

Goal state after: