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

Goal state before:
pp: case pos
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
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n

Tactic:
have h₁₀ := psp_from_prime_gt_p b_ge_two h₉

Goal state after:
case pos
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
⊢ ∃ n, n.FermatPsp b ∧ m ≤ n
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 : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
⊢ 1 ≤ mulHeight x

Tactic:
have hx' : (x i)⁻¹ • x ≠ 0 := by simp [hi, hx]

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
i : ι
hi : x i ≠ 0
hx' : (x i)⁻¹ • x ≠ 0
⊢ 1 ≤ mulHeight x
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / ∏ᶠ (i : FinitePlace K), i ↑b =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹

Tactic:
prod_eq_inv_abs_norm_int hb

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ |↑((Algebra.norm ℤ) a)|⁻¹ / |↑((Algebra.norm ℤ) b)|⁻¹ =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|⁻¹
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.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
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) = 0
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
← le_max_right

Goal state after:
case inr.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
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) = 0
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ 1 * mulHeight x ^ N
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
have := X_pow_sub_C_eq_prod hμ n.zero_lt_succ (one_pow (n + 1))
  rw [C_1, ← mul_geom_sum, prod_range_succ', pow_zero, mul_one, mul_comm, eq_comm] at this
  replace this := mul_right_cancel₀ (Polynomial.X_sub_C_ne_zero 1) this
  apply_fun Polynomial.eval 1 at this
  simpa only [mul_one, map_pow, eval_prod, eval_sub, eval_X, eval_pow, eval_C, eval_geom_sum,
    one_pow, sum_const, card_range, nsmul_eq_mul, Nat.cast_add, Nat.cast_one] using this

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ v, f ↑v ^ v.mult

Tactic:
classical
  rw [Finset.prod_multiset_map_count]
  exact Finset.prod_bij' (fun w hw ↦ ⟨w, mem_multisetInfinitePlace.mp <| Multiset.mem_dedup.mp hw⟩)
    (fun v _ ↦ v.val) (fun _ _ ↦ Finset.mem_univ _) (fun v _ ↦ by simp [v.isInfinitePlace])
    (fun _ _ ↦ rfl) (fun _ _ ↦ rfl) fun w hw ↦ by rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]

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

Tactic:
simp only [zero_div]

Goal state after:
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 + 1 ≠ -↑m
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
ψ : AddChar F R
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x

Tactic:
have sum_eq : ∀ t ∈ univ \ {0}, (∑ x : F, χ x * φ (t - x)) * ψ t =
      (∑ y : F, χ (t * y) * φ (t - (t * y))) * ψ t := by
    intro t ht
    simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht
    exact congrArg (· * ψ t) (Equiv.sum_comp (Equiv.mulLeft₀ t ht) _).symm

Goal state after:
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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x
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
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      (algebraMap F' FF') (jacobiSum χ⁻¹ φ⁻¹) =
    (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
← jacobiSum_ringHomComp

Goal state after:
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
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
⊢ jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF')) =
    (algebraMap F' FF') ↑(Fintype.card F)
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:
rw [mul_assoc, 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: ⊢ (fun s ↦ (riemannZeta s)⁻¹ - (s - 1)) =O[𝓝[≠] 1] fun s ↦ (s - 1) ^ 2

Tactic:
by
  suffices (fun s ↦ (s - 1) * ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] (fun s ↦ (s - 1) ^ 2) by
    refine (this.mono nhdsWithin_le_nhds).congr' ?_ .rfl
    filter_upwards [inv_riemannZeta_eq_sub_mul]
    simp +contextual [field]
  suffices (fun s ↦ ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] (· - 1) by
    simpa [pow_two] using (isBigO_refl ..).mul this
  simpa using ((differentiable_riemannZeta₁.differentiableAt (x := 1)).inv (by simp)).isBigO_sub

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
B' : ℝ := B / ↑n ^ (totalWeight K - 1)
a : K
ha : a ∈ integralClosure ℤ K ∧ ∀ (φ : K →+* ℂ), ‖φ a‖ ≤ B'
⊢ ∃ x, (∀ (v : InfinitePlace K), v ↑x ≤ B') ∧ ↑x = a

Tactic:
exact ⟨⟨a, ha.1⟩, fun v ↦ v.norm_embedding_eq a ▸ ha.2 v.embedding, rfl⟩

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 h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
⊢ h.map x = h'.map x

Tactic:
by rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq]

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:
rw [mul_assoc, 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✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRootMonic S f
inst✝ : Nontrivial S
x : R
⊢ h.coeff ((algebraMap R S) x) = Pi.single 0 x

Tactic:
ext i
  rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]
  refine (Pi.apply_single (fun _ y => x * y) ?_ 0 1 i).trans (by simp)
  simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this : IsDomain (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen

Tactic:
have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this✝ : IsDomain (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
⊢ minpoly R x = minpoly R (powerBasis' hx').gen
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.cos (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k).re

Tactic:
· refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_cos hk hx).tsum_eq).trans ?_
    · rw [ofReal_tsum]
      refine tsum_congr fun n ↦ ?_
      norm_cast
      ring_nf
    · push_cast
      congr 1
      have : (Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
      rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
      apply Polynomial.map_aeval_eq_aeval_map (by simp)

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k).re
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hg
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := ⋯
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ ∑ x_1 ∈ Finset.range m, ↑m ^ k * bernoulliFun (k + 1) (x + ↑x_1 / ↑m))
    (∑ x_1 ∈ Finset.range m, ↑m ^ k * (↑k + 1) * bernoulliFun k (x + ↑x_1 / ↑m)) x

Tactic:
refine HasDerivAt.fun_sum fun i _ ↦ ?_

Goal state after:
case hg
m : ℕ
m0 : m ≠ 0
x✝¹ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
i : ℕ
x✝ : i ∈ Finset.range m
⊢ HasDerivAt (fun x ↦ ↑m ^ k * bernoulliFun (k + 1) (x + ↑i / ↑m)) (↑m ^ k * (↑k + 1) * bernoulliFun k (x + ↑i / ↑m)) x
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, normalizedFactors (Ideal.map (algebraMap R S) I) = {y}

Tactic:
rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']

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,
    Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
      {y}
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
← sub_eq_iff_eq_add,

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : (2 ^ k / 2)⁻¹ * ↑(bernoulli k) - ↑(bernoulli k) = bernoulliFun k (1 / 2)
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ

Tactic:
simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ↑(∏ i ∈ Ico 1 (p / 2).succ, i))

Tactic:
prod_Ico_id_eq_factorial,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ↑(p / 2)!)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t ↦ ↑t ^ (-↑s - 1) * ∑ k ∈ Icc 1 ⌊t⌋₊, f k) (Set.Ici 1) volume

Tactic:
refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ LocallyIntegrableOn (fun t ↦ ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
have : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩

Goal state after:
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯
this : Fact (Nat.Prime p)
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J(↑p | a) = qrSign p a * J(↑a | p)

Tactic:
qrSign.symm hpo ha

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J(↑p | a) = qrSign a p * J(↑a | p)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x y⁻¹⁻¹

Tactic:
simp [h, hy]

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

Goal state before:
pp: case inr.h₁
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ x ≤ 1

Tactic:
simp [h, hy]

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

Goal state before:
pp: case inr.h₂
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ 1 ≤ y⁻¹⁻¹

Tactic:
simp [h, hy]

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

Goal state before:
pp: case inl
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : 1 < z
⊢ (Set.Icc z 1).Finite

pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
⊢ (Set.Icc z 1).Finite

Tactic:
· rw [Set.Icc_eq_empty_of_lt]
    · exact Set.finite_empty
    · simp [hz1]

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
⊢ (Set.Icc z 1).Finite
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ 0 ≤ sMod p (p - 2)

pp: p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1

Tactic:
· exact sMod_nonneg _ (by positivity) _

Goal state after:
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) < 2 ^ p - 1
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
suffices ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1 by
    simpa [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, cyclotomic.monic n ℂ,
      Polynomial.cyclotomic.roots_eq_primitiveRoots_val]

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ ∏ x ∈ primitiveRoots n ℂ, max 1 ‖x‖ = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
⊢ ∀ (a b : { v // v ≠ 0 }) (t : K),
    ↑a = t • ↑b → (if ↑a 1 = 0 then ∞ else ↑((↑a 1)⁻¹ * ↑a 0)) = if ↑b 1 = 0 then ∞ else ↑((↑b 1)⁻¹ * ↑b 0)

Tactic:
rintro ⟨-, hv⟩ ⟨w, hw⟩ t rfl

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
x : OnePoint K
⊢ (equivProjectivization K) (g • x) = g • (equivProjectivization K) x

Tactic:
Equiv.smul_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
x : OnePoint K
⊢ (equivProjectivization K) ((equivProjectivization K).symm (g • (equivProjectivization K) x)) =
    g • (equivProjectivization K) x