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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ HasFiniteMulSupport fun v ↦ max (↑v x) 1

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ HasFiniteMulSupport fun v ↦ max (↑v 0) 1

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ max (↑v x) 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
c : K
hc : c ≠ 0
⊢ mulHeight (c • x) = mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
c : K
hc : c ≠ 0
⊢ mulHeight (c • 0) = mulHeight 0

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
c : K
hc : c ≠ 0
hx : x ≠ 0
⊢ mulHeight (c • x) = mulHeight x
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
⊢ 1 ≤ mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
⊢ 1 ≤ mulHeight 0

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
⊢ 1 ≤ mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inr.inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
h₀ : 0 ∘ f ≠ 0
⊢ mulHeight (0 ∘ f) ≤ mulHeight 0

case inr.inr
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
h₀ : x ∘ f ≠ 0
hx : x ≠ 0
⊢ mulHeight (x ∘ f) ≤ mulHeight x
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
⊢ mulHeight (Sum.elim x 0) = mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
⊢ mulHeight (Sum.elim 0 0) = mulHeight 0

case inr
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
⊢ mulHeight (Sum.elim x 0) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
⊢ mulHeight x = 1

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
⊢ mulHeight 0 = 1

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr.inr
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
⊢ (mulHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inr.inr.inr.inl
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
hι' : Nonempty ι'
hA : A ≠ 0
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight 0
h : (fun j ↦ ∑ i, A (j, i) * 0 i) ≠ 0
⊢ (mulHeight fun j ↦ ∑ i, A (j, i) * 0 i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight 0

case inr.inr.inr.inr
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
⊢ (mulHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
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
n : ℕ
⊢ mulHeight (x ^ n) = mulHeight x ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
n : ℕ
⊢ mulHeight (0 ^ n) = mulHeight 0 ^ n

case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
n : ℕ
hx : x ≠ 0
⊢ mulHeight (x ^ n) = mulHeight x ^ n
Module: Mathlib.NumberTheory.Height.Basic

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

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ mulHeight ![0⁻¹, 1] = mulHeight ![0, 1]

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
calc term n s
    _ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ (s + 1) := by rfl
    _ = ∫ x : ℝ in n..(n + 1), (x ^ (-s) - n * x ^ (-(s + 1))) := by
      refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
      rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
    _ = (∫ x : ℝ in n..(n + 1), x ^ (-s)) - n * (∫ x : ℝ in n..(n + 1), x ^ (-(s + 1))) := by
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_const_mul] <;>
      [skip; apply IntervalIntegrable.const_mul] <;>
      · refine intervalIntegral.intervalIntegrable_rpow (Or.inr <| notMem_uIcc_of_lt ?_ ?_)
        · exact_mod_cast hn
        · linarith
    _ = 1 / (s - 1) * (1 / n ^ (s - 1) - 1 / (n + 1) ^ (s - 1))
          - n / s * (1 / n ^ s - 1 / (n + 1) ^ s) := by
      have : 0 ∉ uIcc (n : ℝ) (n + 1) := (lt_irrefl _ <| hv _ ·)
      rw [integral_rpow (Or.inr ⟨by linarith, this⟩), integral_rpow (Or.inr ⟨by linarith, this⟩)]
      congr 1
      · rw [show -s + 1 = -(s - 1) by ring, div_neg, ← neg_div, mul_comm, mul_one_div, neg_sub,
          rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]
      · rw [show -(s + 1) + 1 = -s by ring, div_neg, ← neg_div, neg_sub, div_mul_eq_mul_div,
          mul_div_assoc, rpow_neg (Nat.cast_nonneg _), one_div, rpow_neg (by linarith), one_div]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
⊢ mulHeight (-x) = mulHeight x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
⊢ mulHeight (-0) = mulHeight 0

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
hx : x ≠ 0
⊢ mulHeight (-x) = mulHeight x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
y : ι → K
hι : Nonempty ι
⊢ mulHeight (0 * y) ≤ mulHeight 0 * mulHeight y

case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommSemiring S
inst✝¹ : LinearOrder S
inst✝ : IsOrderedRing S
v : AbsoluteValue R S
hv : IsNonarchimedean ⇑v
ι : Type u_3
s : Finset ι
x : ι → R
⊢ max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 1

Tactic:
by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · simp
  refine sup_le ?_ <| s.one_le_prod fun _ _ ↦ le_max_right ..
  grw [hv.apply_sum_le_sup hs]
  exact sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)

Goal state after:
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 ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Goal state after:
case inl
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
⊢ (mulHeight fun j ↦ (eval 0) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight 0 ^ N

case inr
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1.hy
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 := ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ ℤ[μ]

Tactic:
· refine Subalgebra.prod_mem _ fun _ _ ↦ ?_
      apply Subalgebra.sub_mem
      · exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _
      · exact Subalgebra.one_mem _

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

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
ha : 0 < a.re
a✝ : a ∈ {1}ᶜ
⊢ (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)

Tactic:
← sub_div,

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
ha : 0 < a.re
a✝ : a ∈ {1}ᶜ
⊢ (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹ - ↑γ) =O[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
by
  suffices (fun s ↦ (deriv riemannZeta₁ s) / (riemannZeta₁ s) - γ) =O[𝓝 1] (· - 1) by
    refine (this.mono nhdsWithin_le_nhds).congr' ?_ .rfl
    filter_upwards [log_deriv_riemannZeta_eq_neg_inv_sub_add]
    simp +contextual
  suffices DifferentiableAt ℂ (fun s ↦ (deriv riemannZeta₁ s) / (riemannZeta₁ s)) 1 by
    simpa using this.isBigO_sub
  fun_prop (disch := simp)

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
f : ι → ℤ
hf : 1 ≤ ⨆ i, v (↑(x i) * ↑(f i))
i : ι
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
← hi,

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 : ι → ℤ
i : ι
hf : 1 ≤ v (↑(x i) * ↑(f i))
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
⊢ mulHeight₁ q = ↑(max q.num.natAbs q.den)

Tactic:
rw [mulHeight₁_eq_mulHeight, mulHeight_self_one_eq_mulHeight_num_den, ← intCast_natCast q.den]
  have : (.univ : Finset (Fin 2)).gcd ![q.num, q.den] = 1 := by
    simpa [Finset.univ_fin2, Int.normalize_coe_nat, ← Int.coe_gcd q.num q.den] using
      Int.isCoprime_iff_gcd_eq_one.mp <| isCoprime_num_den q
  convert! mulHeight_eq_max_abs_of_gcd_eq_one this
  · ext i; fin_cases i <;> simp
  · rw [← Int.cast_natCast, Int.cast_inj]
    push_cast
    refine le_antisymm (max_le ?_ ?_) <| ciSup_le fun i ↦ ?_
    · exact Finite.le_ciSup_of_le 0 <| by simp
    · exact Finite.le_ciSup_of_le 1 <| by simp
    · fin_cases i <;> simp

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case h
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))
⊢ Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
    {↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
          ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩)}

Tactic:
Multiset.map_eq_singleton

Goal state after:
case h
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))
⊢ ∃ a,
    (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {a} ∧
      ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm a) =
        ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
            ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
⊢ LFunction Φ 0 = -Φ 0 / 2

Tactic:
simp only [LFunction_def_even hΦ, neg_zero, cpow_zero, hurwitzZetaEven_apply_zero,
    toAddCircle_eq_zero, mul_ite, mul_div, mul_neg_one, mul_zero, sum_ite_eq', Finset.mem_univ,
    ↓reduceIte, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inr.refine_2
k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ bernoulliFourierCoeff (k + 1) n = -↑(k + 1)! / (2 * ↑π * I * ↑n) ^ (k + 1)

Tactic:
· rw [bernoulliFourierCoeff_recurrence (k + 1) hn, if_neg (by grind), Nat.add_sub_cancel k 1, h'k,
      Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add]
    ring

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
⊢ ↑n ^ x ≤ 0 ∨ 1 < ↑n ^ x

Tactic:
exact .inr <| Real.one_lt_rpow (mod_cast one_lt_two.trans_le hn) <| zero_lt_one.trans hx

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

Goal state before:
pp: S : Set ℂ
hS : IsCompact S
⊢ (S ∩ riemannZetaZeros).Finite

Tactic:
by
  apply (hS.inter_right isClosed_riemannZetaZeros).finite
  exact isDiscrete_riemannZetaZeros.mono Set.inter_subset_right

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ ∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a

pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)

Tactic:
· exact fun p hp =>
      (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList

Goal state after:
a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b₁.primeFactorsList ⋯).prod *
      (List.pmap (fun p pp ↦ legendreSym p a) b₂.primeFactorsList ⋯).prod =
    J(a | b₁) * J(a | b₂)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb : Odd b
⊢ J(4 | b) = 1

Tactic:
have : J((4 : ℤ) | b) = J((4 : ℤ) / 4 | b) :=
    (div_four_left (by decide) (Nat.odd_iff.mp hb)).symm
  simpa [one_left]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ 𝓂[K]

Tactic:
rw [Valued.maximalIdeal, hp.maximalIdeal_eq, ← SetLike.mem_coe,
      (Valuation.integer.integers _).coe_span_singleton_eq_setOfPred_le_v_algebraMap]

Goal state after:
case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist x y < ‖p‖
⊢ y - x ∈ {y | v ((algebraMap (↥v.integer) K) y) ≤ v ((algebraMap (↥v.integer) K) p)}
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ MulArchimedean (↥(MonoidHom.mrange v))ˣ

Tactic:
obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange v))ˣ
⊢ MulArchimedean (↥(MonoidHom.mrange v))ˣ
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : CompactSpace ↥𝒪[K]
hi : v.Integers ↥𝒪[K]
hc : IsCompact ↑𝒪[K]
⊢ IsPrincipalIdealRing ↥𝒪[K]

Tactic:
obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : CompactSpace ↥𝒪[K]
hi : v.Integers ↥𝒪[K]
hc : IsCompact ↑𝒪[K]
val✝ : LocallyFiniteOrder (↥(MonoidHom.mrange v))ˣ
⊢ IsPrincipalIdealRing ↥𝒪[K]
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x, v ↑x < 1 ∧ ¬x = 0

Tactic:
exact ⟨fun ⟨x, hx0, hx1⟩ ↦ ⟨⟨x, hx1.le⟩, by simp [Subtype.ext_iff, *]⟩,
  fun ⟨x, hx1, hx0⟩ ↦ ⟨x, by simp [*]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : p ≠ 0
i : ℕ
⊢ 0 ≤ sMod p i

Tactic:
cases i

Goal state after:
case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ sMod p 0

case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ sMod p (n✝ + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p i : ℕ
⊢ sMod p i % (2 ^ p - 1) = sMod p i

Tactic:
cases i

Goal state after:
case zero
p : ℕ
⊢ sMod p 0 % (2 ^ p - 1) = sMod p 0

case succ
p n✝ : ℕ
⊢ sMod p (n✝ + 1) % (2 ^ p - 1) = sMod p (n✝ + 1)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

pp: case refine_3
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖

Tactic:
· refine le_of_forall_pos_le_add fun ε hε ↦ ?_
    rw [zero_add]
    obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε
    refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq
    exact isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)

Goal state after:
case refine_3
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) (𝓝[>] 1) fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖