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

Goal state before:
pp: x : ℝ
N : ℕ
⊢ ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n

Tactic:
by
  induction N with
  | zero => simp
  | succ N ih =>
    rw [show 1 + 6 * (N + 1) = (1 + 6 * N) + 1 + 1 + 1 + 1 + 1 + 1 by ring,
      show 3 * (N + 1) = 3 * N + 1 + 1 + 1 by ring,
      show 2 * (N + 1) = 2 * N + 1 + 1 by ring]
    simp only [le_add_iff_nonneg_left, _root_.zero_le, sum_Icc_succ_top, ih, c]
    rw [show 6 * (N + 1) - 1 = 6 * N + 5 by lia]
    ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x

Tactic:
have : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n) := by
    apply sum_le_sum
    intro n hn
    unfold c
    linarith [(b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n + 1) ≤ b x (6 * n)),
      (b_antitone x hx (by grind) (by grind) (by lia) : b x (6 * n - 1) ≤ b x (5 * n))]

Goal state after:
x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹) ∧ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 7⁻¹) ≤ ψ x - θ x
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j ↦ A (Classical.choose ⋯).succ) j₀.succ % b)) <
    cardPowDegree b • ε
⊢ False

Tactic:
rw [Fin.cons_succ, Fin.cons_succ] at approx

Goal state after:
case refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx : ↑(cardPowDegree (A (Classical.choose ⋯).succ % b - A (Classical.choose ⋯).succ % b)) < cardPowDegree b • ε
⊢ False
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ x.appr (n + 1) < p ^ (n + 1)

Tactic:
simp only [appr, map_natCast, ZMod.natCast_self, map_pow, Int.natAbs, map_mul]
    have hp : p ^ n < p ^ (n + 1) := by apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one
    split_ifs with h
    · apply lt_trans (ih _) hp
    · calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_
      · apply add_lt_add_of_lt_of_le (ih _)
        apply Nat.mul_le_mul_left
        apply le_pred_of_lt
        apply ZMod.val_lt
      · rw [mul_tsub, mul_one, ← _root_.pow_succ]
        apply add_tsub_cancel_of_le (le_of_lt hp)

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ (S ⧸ (↑R (Algebra.linearMap S L)).ker) ≃ₗ[R] S

Tactic:
rw [LinearMap.ker_eq_bot.mpr]
    · exact Submodule.quotEquivOfEqBot _ rfl
    · exact IsIntegralClosure.algebraMap_injective _ R _

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ m)

Tactic:
by
  obtain ⟨m, hm⟩ := MonoidHom.map_cyclic ((g : L ≃* L).restrictRootsOfUnity n).toMonoidHom
  exact ⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
refine (IsBigO.of_bound (log 4) ?_).trans integral_one_div_log_sq_isBigO
  filter_upwards [eventually_ge_atTop 4] with x _
  simp_rw [norm_eq_abs]
  calc |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
        intervalIntegral.abs_integral_le_integral_abs (by linarith)
    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity
  case hf =>
    refine (intervalIntegrable_iff.mpr ?_).abs
    rw [Set.uIoc_of_le (by linarith), ← integrableOn_Icc_iff_integrableOn_Ioc]
    exact integrableOn_theta_div_id_mul_log_sq x
  case hg =>
    refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _ <;> linarith
  case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ cyclotomicCharacter.toFun p 1 = 1

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
      · have _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
        refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
        simp [cyclotomicCharacter.toZModPow_toFun]
      · simp [cyclotomicCharacter.toFun, dif_neg H]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i)
      · have _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
        refine PadicInt.ext_of_toZModPow.mp fun n ↦ ?_
        simp [cyclotomicCharacter.toZModPow_toFun]
      · simp [cyclotomicCharacter.toFun, dif_neg H]

Goal state after:
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
i j : ι
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) (b i) * (algebraMap S Sₘ) (b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))

Tactic:
← map_mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Free R S
i j : ι
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) (b i * b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
⊢ IsCauSeq (padicNorm p) fun x ↦ ↑(f x)

Tactic:
by
  intro ε hε
  obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt_rat p hε
  simp only [← Int.cast_sub]
  refine ⟨k, fun i hik ↦ (padicNorm.dvd_iff_norm_le.mp ?_).trans_lt hk⟩
  obtain ⟨i, rfl⟩ := exists_add_of_le hik
  clear hik
  induction i with
  | zero => simp
  | succ n IH =>
    have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
    simpa using! (this.trans (hi _)).add IH

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ a * a

Tactic:
exact Nat.mul_self_le_mul_self na

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

Goal state before:
pp: case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = ↑z * { re := r, im := i }

Tactic:
smul_val,

Goal state after:
case h
d z : ℤ
a : ℤ√d
r : ℤ
hr : a.re = z * r
i : ℤ
hi : a.im = z * i
⊢ a = { re := z * r, im := z * i }
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = ↑↑(a.re.gcd a.im) * { re := re, im := im }

Tactic:
smul_val,

Goal state after:
case refine_1
d : ℤ
a : ℤ√d
hgcd : 0 < a.re.gcd a.im
re im : ℤ
H1 : re.gcd im = 1
Hre : a.re = ↑(a.re.gcd a.im) * re
Him : a.im = ↑(a.re.gcd a.im) * im
⊢ a = { re := ↑(a.re.gcd a.im) * re, im := ↑(a.re.gcd a.im) * im }
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs * y.norm.natAbs = 1
⊢ x.norm.natAbs = 1

Tactic:
mul_eq_one

Goal state after:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1
⊢ x.norm.natAbs = 1
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case zero
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
hζone : ζ = 1
⊢ Matrix.of (fun i j ↦ Module.finrank K L • 1) default default = 1 * ↑p ^ (p ^ (0 - 1) * (0 - 1))

Tactic:
finrank _ hirr

Goal state after:
case zero
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ 0} K L
hζ : IsPrimitiveRoot ζ (p ^ 0)
hirr : Irreducible (cyclotomic (p ^ 0) K)
hζone : ζ = 1
⊢ Matrix.of (fun i j ↦ φ (p ^ 0) • 1) default default = 1 * ↑p ^ (p ^ (0 - 1) * (0 - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ yz a1 (n + 2) + yz a1 n = ↑(2 * a) * yz a1 (n + 1)

Tactic:
delta yz; rw [← Int.natCast_add, ← Int.natCast_mul, yn_succ_succ]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ Module.finrank K L • 1 = 1

Tactic:
finrank _ hirr

Goal state after:
case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ φ (2 ^ (0 + 1)) • 1 = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
⊢ a = 0

Tactic:
have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective
    suffices lift r a.norm = 0 by
      simp only [re_intCast, add_zero, lift_apply_apply, im_intCast, Int.cast_zero,
        zero_mul] at this
      rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this
    rw [norm_eq_mul_conj, map_mul, ha, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.DirichletCharacter.Bounds

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
n : ℕ
χ : DirichletCharacter F n
a : ZMod n
⊢ ‖χ a‖ ≤ 1

Tactic:
by
  by_cases h : IsUnit a
  · exact (χ.unit_norm_eq_one h.unit).le
  · rw [χ.map_nonunit h, norm_zero]
    exact zero_le_one

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 0 = x ∧ yn a1 0 = y

Tactic:
x1,

Goal state after:
a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 0 = 1 ∧ yn a1 0 = y
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ y
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 k = x ∧ yn a1 k = y

Tactic:
rw [y0] at ky; rw [Nat.eq_zero_of_le_zero ky, x1, y0]; exact ⟨rfl, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N

Tactic:
Finset.filter_congr (s := Finset.range (succ N)) fun n _ ↦ hn' n

Goal state after:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ #({n ∈ Finset.range N.succ | n ≠ 0}) = N
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
⊢ i = k

Tactic:
have ji : j ≡ i [MOD 4 * n] :=
              have : xn a1 j ≡ xn a1 i [MOD xn a1 n] :=
                (xy_modEq_of_modEq b1 a1 ba j).left.symm.trans sx
              (modEq_of_xn_modEq a1 ipos iln this).resolve_right
                fun ji : j + i ≡ 0 [MOD 4 * n] =>
                not_le_of_gt ki <|
                  Nat.le_of_dvd (lt_of_lt_of_le ipos <| Nat.le_add_left _ _) <|
                    modEq_zero_iff_dvd.1 <| (jk.symm.add_right i).trans <| ji.of_dvd yd

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
ipos : i > 0
iln : i ≤ n
yd : 4 * yn a1 i ∣ 4 * n
jk : j ≡ k [MOD 4 * yn a1 i]
ki : k + i < 4 * yn a1 i
ji : j ≡ i [MOD 4 * n]
⊢ i = k
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ |(fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)| = |fract ξ - ↑u' / ↑v| * (↑v / ↑u' / fract ξ)

Tactic:
by rw [abs_mul, abs_of_pos H₁]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = ∏' (p : Primes) (k : ℕ), f (↑p ^ (k + 1))

Tactic:
rw [tprod_primes_pow_eq (hfm.subtype _)]

Goal state after:
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : UniformSpace α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n | IsPrimePow n}
⊢ ∏' (n : ℕ), f n = ∏' (n : { n // IsPrimePow n }), f ↑n
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case convert_3.inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
⊢ Integrable (fun t ↦ ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Tactic:
simp [hai]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (g_nat 0 a t) (rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ g_nat 0 a t = fun i ↦ rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5.inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
⊢ ‖a i‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

Tactic:
simp [hai]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case hg
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ HasSum (fun b ↦ a * rexp (-π * (↑b + a ^ 2) * t)) (a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)))

Tactic:
convert! (hasSum_geometric_of_lt_one (exp_pos _).le <| exp_lt_aux ht).mul_left _ using 1

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ (fun b ↦ a * rexp (-π * (↑b + a ^ 2) * t)) = fun i ↦ a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ i