mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case inr
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
⊢ spanNorm R (I * J) = spanNorm R I * spanNorm R J

Tactic:
refine eq_of_localization_maximal (fun P hP ↦ ?_)

Goal state after:
case inr
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
let P' := Algebra.algebraMapSubmonoid S P.primeCompl

Goal state after:
case neg
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDomain R
S : Type u_3
inst✝⁹ : CommRing S
inst✝⁸ : IsDomain S
inst✝⁷ : IsIntegrallyClosed R
inst✝⁶ : IsIntegrallyClosed S
inst✝⁵ : Algebra R S
inst✝⁴ : Module.Finite R S
inst✝³ : IsTorsionFree R S
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
this : NeZero P
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ finrank R S)

Tactic:
let P' := Algebra.algebraMapSubmonoid S P.primeCompl

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : IsDomain S
inst✝⁶ : IsIntegrallyClosed R
inst✝⁵ : IsIntegrallyClosed S
inst✝⁴ : Algebra R S
inst✝³ : Module.Finite R S
inst✝² : IsTorsionFree R S
inst✝¹ : IsDedekindDomain R
inst✝ : IsDedekindDomain S
I P : Ideal R
hPd : P.IsMaximal
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (map (algebraMap R S) I)) =
    map (algebraMap R (Localization.AtPrime P)) (I ^ finrank R S)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn :
  ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p
i : ℕ
hi : i < ((cyclotomic (p ^ (n + 1 + 1)) ℤ).comp (X + 1)).natDegree
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
by rw [pow_succ']

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ {n_1 : ℕ},
    n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree →
      ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ ℤ ∙ ↑p

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
n : ℕ
z : L
hzint : IsIntegral R z
hz : p ^ n • z ∈ R[B.gen]
hei : (minpoly R B.gen).IsEisensteinAt (R ∙ p)
⊢ z ∈ R[B.gen]

Tactic:
induction n with

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Goal state before:
pp: K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑|(-1) ^ ((3 - 1) / 2) * ↑3 ^ (3 - 2)| <
    (2 * (π / 4) ^ nrComplexPlaces K * (↑(Module.finrank ℚ K) ^ Module.finrank ℚ K / ↑(Module.finrank ℚ K)!)) ^ 2

Tactic:
IsCyclotomicExtension.finrank (n := 3) K
    (irreducible_rat (by simp)),

Goal state after:
K : Type u
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ↑|(-1) ^ ((3 - 1) / 2) * ↑3 ^ (3 - 2)| < (2 * (π / 4) ^ nrComplexPlaces K * (↑(φ 3) ^ φ 3 / ↑(φ 3)!)) ^ 2
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
this : ↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
← hw

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
h : (logEmbedding K) (Additive.ofMul x) = 0
w : InfinitePlace K
hw : w = w₀
this : ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
⊢ w ((algebraMap (𝓞 K) K) ↑x) = 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))|

Tactic:
← hw

Goal state after:
case pos.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
x : (𝓞 K)ˣ
hr : 0 ≤ r
h : ‖(logEmbedding K) (Additive.ofMul x)‖ ≤ r
w : InfinitePlace K
tool : ∀ (x : ℝ), 0 ≤ x → x ≤ ↑w.mult * x
hw : w = w₀
hyp : ↑w₀.mult * |Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))| ≤ ∑ x_1, |(logEmbedding K) (Additive.ofMul x) x_1|
⊢ |Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑w.mult * |Real.log (w ((algebraMap (𝓞 K) K) ↑x))|
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
⊢ ∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B

Tactic:
let f : InfinitePlace K → ℝ≥0 :=
    fun w ↦ ⟨(w x) / 2, div_nonneg (AbsoluteValue.nonneg _ _) (by simp)⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
⊢ ∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect

Tactic:
by
  rw [not_pseudoperfect_iff_forall]
  refine Or.inr fun s hs ↦ ne_of_lt (lt_of_le_of_lt ?_ h.one_lt)
  rw [Prime.properDivisors h] at hs
  simpa using Finset.sum_le_sum_of_subset hs

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ ∑ i ∈ (n ^ m).properDivisors, i < n ^ m

Tactic:
properDivisors_prime_pow h

Goal state after:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ ∑ i ∈ map { toFun := fun x ↦ n ^ x, inj' := ⋯ } (range m), i < n ^ m
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : 3 ∣ a * b ∨ 3 ∣ c
⊢ False

Tactic:
prime_three.dvd_mul

Goal state after:
case pos
H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
Hgcd : {a, b, c}.gcd id = 1
hF : a ^ 3 + b ^ 3 = c ^ 3
h1 : (3 ∣ a ∨ 3 ∣ b) ∨ 3 ∣ c
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.Basic

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

Tactic:
← div_pow,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : (x / y) ^ 2 = -(y ^ 2 / y ^ 2)
⊢ (x / y) ^ 2 = -1
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 ^ 2 / y ^ 2)
⊢ (x / y) ^ 2 = -1

Tactic:
← div_pow,

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

Goal state before:
pp: n : ℕ
⊢ ∏ k ∈ range n, k.fermatNumber = n.fermatNumber - 2

Tactic:
induction n with

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ (p - 1 + 1) - b) * (b ^ p + b) = (b * b ^ (p - 1) - b) * (b ^ p + b)

Tactic:
by rw [pow_succ']

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case inl
n : ℕ
h : n ∈ maximalIdeal ℕ
lt : n < 1
⊢ n ∈ span {2, 3}

pp: case inr
n : ℕ
h : n ∈ maximalIdeal ℕ
lt : 1 < n
⊢ n ∈ span {2, 3}

Tactic:
· obtain rfl := lt_one_iff.mp lt; exact zero_mem _

Goal state after:
case inr
n : ℕ
h : n ∈ maximalIdeal ℕ
lt : 1 < n
⊢ n ∈ span {2, 3}
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
⊢ λ ∣ S.a + S.b + λ ^ 2 * S.b + 2 * λ * S.b

Tactic:
exact dvd_add (dvd_add (dvd_trans (dvd_pow_self _ (by decide)) S.hab) ⟨λ * S.b, by ring⟩)
    ⟨2 * S.b, by ring⟩

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

Goal state before:
pp: n : ℕ
⊢ padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)

Tactic:
induction n with

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

Goal state before:
pp: ⊢ FermatLastTheoremFor 3

Tactic:
let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]

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

Goal state before:
pp: case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ ∑ x ∈ Finset.range (N + 1), 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑(N + 1) + 1) ^ (s - 1))

Tactic:
rw [Finset.sum_range_succ, hN, Nat.cast_add_one]

Goal state after:
case e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ x ∈ Finset.range N, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
⊢ 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) + 1 / (s - 1) * (1 / (↑N + 1) ^ (s - 1) - 1 / (↑N + 1 + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1 + 1) ^ (s - 1))
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ (∏ w, w x ^ w.mult) * ∏ᶠ (w : FinitePlace K), w x = 1

Tactic:
by
  simp [prod_eq_inv_abs_norm, InfinitePlace.prod_eq_abs_norm, h_x_nezero]

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

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ ↑x / (↑x + 1) ^ s) atTop (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
              (h := fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1))

Goal state after:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

case hgf
s : ℝ
hs : 1 < s
⊢ (fun x ↦ 0) ≤ fun x ↦ ↑x / (↑x + 1) ^ s

case hfh
s : ℝ
hs : 1 < s
⊢ (fun x ↦ ↑x / (↑x + 1) ^ s) ≤ fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case ha
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
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
j : ι'
⊢ 0 ≤ (⨆ i, v (x i)) ^ N

Tactic:
exact HH₁ v

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
⊢ ∃ a, ↑m * a = ↑n * r

Tactic:
by
    have : n • r ∈ span {(m : 𝓞 K)} :=
      (span {(m : 𝓞 K)}).toAddSubgroup.nsmul_relIndex_mem <| Submodule.mem_span_of_mem <| by grind
    simpa [mem_span_singleton', mul_comm] using this

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
x : S
⊢ h.map (h.modByMonicHom x) = x

Tactic:
by
  simp [modByMonicHom, map_modByMonic, map_repr]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s

Tactic:
← LFunction_modOne_eq (χ := 1),

Goal state after:
N : ℕ
inst✝ : NeZero N
s : ℂ
hs : s ≠ 1
⊢ LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * LFunction 1 s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k)

Tactic:
Polynomial.eval_one_map,

Goal state after:
k : ℕ
hk : k ≠ 1
⊢ (algebraMap ℚ ℝ) (Polynomial.eval 1 (Polynomial.bernoulli k)) = ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k) + if k = 1 then 1 else 0

Tactic:
Polynomial.eval_one_map,

Goal state after:
k : ℕ
⊢ (algebraMap ℚ ℝ) (Polynomial.eval 1 (Polynomial.bernoulli k)) = ↑(bernoulli k) + if k = 1 then 1 else 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k 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)
h : ∀ (x : ℝ), f k x = 0
⊢ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m) = 0

Tactic:
exact h x

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))
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
by
  classical
  have mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
      normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) := by
    simp [normalizedFactors_irreducible hf]
  suffices ∃ y, normalizedFactors (I.map (algebraMap R S)) = {y} by
    obtain ⟨y, hy⟩ := this
    have h := prod_normalizedFactors (show I.map (algebraMap R S) ≠ 0 by
          rwa [← bot_eq_zero, Ne,
            map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)])
    rw [associated_iff_eq, hy, Multiset.prod_singleton] at h
    rw [← h]
    exact
      irreducible_of_normalized_factor y
        (show y ∈ normalizedFactors (I.map (algebraMap R S)) by simp [hy])
  rw [normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map hI hI' hx hx']
  use ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩ :
      Ideal S)
  rw [Multiset.map_eq_singleton]
  use ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩
  refine ⟨?_, rfl⟩
  apply Multiset.map_injective Subtype.coe_injective
  rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]
  exact normalizedFactors_irreducible hf

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

Goal state before:
pp: case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ ↑N ^ (-x) * ((∑ j, Φ j) / (1 - x))) s

Tactic:
refine .mul (by fun_prop) (hs₁.elim ?_ ?_)

Goal state after:
case refine_2.refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ s ≠ 1 → DifferentiableAt ℂ (fun x ↦ (∑ j, Φ j) / (1 - x)) s

case refine_2.refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ ∑ j, Φ j = 0 → DifferentiableAt ℂ (fun x ↦ (∑ j, Φ j) / (1 - x)) s
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f - g) s (a - b)

Tactic:
simpa [LSeriesHasSum, term_sub] using! HasSum.sub hf hg

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

Goal state before:
pp: case e_a.e_f.inr
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
m : ℕ
hm : m ≠ n + 1
⊢ (if m = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) m) = F x m

Tactic:
· simp [hm, hF]

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
rcases eq_or_ne s 1 with rfl | hs₁

Goal state after:
case inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
hs : 1 ∈ {s | 1 ≤ s.re}
⊢ 1 ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

case inr
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | 1 ≤ s.re}
hs₁ : s ≠ 1
⊢ s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ}, x ∈ Set.Icc 1 2 → C ≤ (LFunctionResidueClassAux a ↑x).re
⊢ ∃ C, ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x

Tactic:
refine ⟨-C, fun {x} hx ↦ ?_⟩

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H :
  ∀ {x : ℝ},
    1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x = (LFunctionResidueClassAux a ↑x).re + (↑q.totient)⁻¹ / (x - 1)
this : ContinuousOn (fun x ↦ (LFunctionResidueClassAux a ↑x).re) (Set.Icc 1 2)
C : ℝ
hC : ∀ {x : ℝ}, x ∈ Set.Icc 1 2 → C ≤ (LFunctionResidueClassAux a ↑x).re
x : ℝ
hx : x ∈ Set.Ioc 1 2
⊢ (↑q.totient)⁻¹ / (x - 1) - -C ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x✝¹ : ℕ
x✝ : x✝¹ ≠ 0
⊢ f x✝¹ = 0

Tactic:
rw [H', Pi.zero_apply]

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

Goal state before:
pp: case pos
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
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : (↑b / a).val ≤ p / 2
⊢ (a * (↑b / a)).valMinAbs.natAbs = b

pp: case neg
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
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (a * -(↑b / a)).valMinAbs.natAbs = b

Tactic:
· rw [mul_div_cancel₀ _ hap, valMinAbs_def_pos, val_cast_of_lt (hep hb),
          if_pos (le_of_lt_succ (mem_Ico.1 hb).2), Int.natAbs_natCast]

Goal state after:
case neg
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
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
h✝ : ¬(↑b / a).val ≤ p / 2
⊢ (a * -(↑b / a)).valMinAbs.natAbs = b
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) = ε

Tactic:
rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]

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

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ J(a | p) = -1 ↔ ¬IsSquare ↑a

Tactic:
by
  rw [← legendreSym.to_jacobiSym]
  exact legendreSym.eq_neg_one_iff p

Goal state after: