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

Goal state before:
pp: x : ℝ
N : ℕ
ih :
  ∑ 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
⊢ 2 * (N + 1) = 2 * N + 1 + 1

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
x : ι
x✝ : x ∈ Finset.univ
⊢ b • qs k x • bS x + rs k x • bS x - (b • qs j x • bS x + rs j x • bS x) - (b • qs k x • bS x - b • qs j x • bS x) =
    rs k x • bS x - rs j x • bS x

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ¬↑p ∣ ↑r.den

Tactic:
← norm_int_lt_one_iff_dvd,

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ¬‖↑↑r.den‖ < 1
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ ⟨↑r, h⟩ - ↑(modPart p r)

Tactic:
← (isUnit_den r h).dvd_mul_right

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ↑p ∣ (⟨↑r, h⟩ - ↑(modPart p r)) * ↑r.den
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)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : n ∈ Icc 1 N
⊢ b x (7 * n) ≤ c x n

Tactic:
simp only [mem_Icc, c] at hn ⊢

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)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ b x (7 * n) ≤ b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ maximalIdeal ℤ_[p]
hn : x - ↑n ∈ maximalIdeal ℤ_[p]
⊢ ↑m = ↑n

Tactic:
maximalIdeal_eq_span_p

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
⊢ ↑m = ↑n
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ↑x - ↑n = ↑x - ↑r + (↑r - ↑n)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {↑v}
⊢ x * y - ↑(f x) * ↑(f y) = x * (y - ↑(f y)) + (x - ↑(f x)) * ↑(f y)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
⊢ ↑(f 0) = 0

Tactic:
rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
    · exact f_spec _
    · simp only [sub_zero, cast_zero, Submodule.zero_mem]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - (↑(f x) + ↑(f y)) = x - ↑(f x) + (y - ↑(f y))

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
induction k with
  | zero =>
    simp only [add_zero, le_refl, tsub_eq_zero_of_le, dvd_zero]
  | succ k ih =>
    rw [← add_assoc]
    dsimp [appr]
    split_ifs with h
    · exact ih
    rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
    apply dvd_add _ ih
    apply dvd_mul_of_dvd_left
    apply pow_dvd_pow _ (Nat.le_add_right m k)

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ √x * log x ^ 2) =o[atTop] fun x ↦ x

Tactic:
apply isLittleO_mul_iff_isLittleO_div _ |>.mpr

Goal state after:
⊢ (fun x ↦ log x ^ 2) =o[atTop] fun x ↦ x / √x

⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_f.e_f
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ ((e j) pb.gen - (e i) pb.gen) ^ 2 = -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
ring

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
let := Classical.decEq (Module.Free.ChooseBasisIndex R S)

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
let := Classical.decEq (Module.Free.ChooseBasisIndex R S)

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
this : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.e_a
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : ↑2 ≠ 0
hle : 1 ≤ pb.dim
⊢ ↑pb.dim * ↑pb.dim - (↑pb.dim * (↑pb.dim - ↑1) / ↑2 + ↑pb.dim) = ↑pb.dim * (↑pb.dim - ↑1) / ↑2

Tactic:
ring

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

Goal state before:
pp: case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re + b✝.re = b✝.re + a✝.re

Tactic:
ring

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

Goal state before:
pp: case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.im + b✝.im = b✝.im + a✝.im

Tactic:
ring

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

Goal state before:
pp: case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.re + d * (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re + d * b✝.im * c✝.im) + d * a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re * b✝.re + d * a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re + d * b✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.re + c✝.re) + d * a✝.im * (b✝.im + c✝.im) =
    a✝.re * b✝.re + d * a✝.im * b✝.im + (a✝.re * c✝.re + d * a✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.re + d * (a✝.im + b✝.im) * c✝.im =
    a✝.re * c✝.re + d * a✝.im * c✝.im + (b✝.re * c✝.re + d * b✝.im * c✝.im)

Tactic:
ring

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

Goal state before:
pp: case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)

Tactic:
ring

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

Goal state before:
pp: case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.re + d * a✝.im * b✝.im = b✝.re * a✝.re + d * b✝.im * a✝.im

Tactic:
ring

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

Goal state before:
pp: case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re

Tactic:
ring

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

Goal state before:
pp: case re
d : ℤ
a b : ℤ√d
⊢ a.re * b.re + d * a.im * b.im = b.re * a.re + d * b.im * a.im

Tactic:
ring

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

Goal state before:
pp: case im
d : ℤ
a b : ℤ√d
⊢ -(a.im * b.re) + -(a.re * b.im) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
ring

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

Goal state before:
pp: case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a

Tactic:
rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩
    use ⟨r, i⟩
    rw [smul_val, Zsqrtd.ext_iff]
    exact ⟨hr, hi⟩

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
t,

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe z 1 w d
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑d * ↑w * ↑w - ↑z * ↑z)

Tactic:
ring

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

Goal state before:
pp: d x y z w : ℕ
xy : SqLe x 1 y d
zw : SqLe w d z 1
this : 0 ≤ (↑(d * y * y) - ↑(1 * x * x)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑d * ↑y * ↑y - ↑x * ↑x) * (↑z * ↑z - ↑d * ↑w * ↑w)

Tactic:
ring

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

Goal state before:
pp: d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe z 1 w d
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(d * w * w) - ↑(1 * z * z))
⊢ ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) - (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑d * ↑w * ↑w - ↑z * ↑z)

Tactic:
ring

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

Goal state before:
pp: d x y z w : ℕ
xy : SqLe y d x 1
zw : SqLe w d z 1
this : 0 ≤ (↑(1 * x * x) - ↑(d * y * y)) * (↑(1 * z * z) - ↑(d * w * w))
⊢ (↑x * ↑z + ↑d * ↑y * ↑w) * (↑x * ↑z + ↑d * ↑y * ↑w) - ↑d * (↑x * ↑w + ↑y * ↑z) * (↑x * ↑w + ↑y * ↑z) =
    (↑x * ↑x - ↑d * ↑y * ↑y) * (↑z * ↑z - ↑d * ↑w * ↑w)

Tactic:
ring

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

Goal state before:
pp: d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)

Tactic:
ring

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

Goal state before:
pp: d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ z.norm = 1 ↔ z.norm = ↑1

Tactic:
Int.ofNat_one

Goal state after:
d : ℤ
hd : d ≤ 0
z : ℤ√d
⊢ z.norm = 1 ↔ z.norm = 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n t : ℕ
h : yn a1 n * yn a1 n ∣ yn a1 t
nt : n ∣ t
n0l : 0 < n
k : ℕ
ke : t = n * k
⊢ k * xn a1 n ^ (k - 1) * yn a1 n ≡ 0 [MOD yn a1 n * yn a1 n]

Tactic:
by
          have xm := (xy_modEq_yn a1 n k).right; rw [← ke] at xm
          exact (xm.of_dvd <| by simp [_root_.pow_succ]).symm.trans h.modEq_zero_nat

Goal state after:
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

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(yn a1 (n + 2)) + ↑(yn a1 n) = ↑(2 * a) * ↑(yn a1 (n + 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inr.inr.inl.refine_1
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := ↑w }.Nonneg
i : ℕ
h : { re := -↑x, im := ↑y }.re + { re := ↑z, im := ↑w }.re = -↑i
⊢ i ≤ x

Tactic:
dsimp only at h
      exact Int.ofNat_le.1 (le_of_neg_le_neg (Int.le.intro _ h))

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ
⊢ (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
ring

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

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ ({ re := ↑x, im := ↑y } * a).Nonneg

Tactic:
by
  have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
  rw [this]
  exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(d a1) * yz a1 n * (↑(xn a1 j) * yz a1 n) + ↑(xn a1 j)

Tactic:
delta yz

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(d a1) * ↑(yn a1 n) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
this :
  (↑a.re + ↑a.im * ↑r) * (↑b.re + ↑b.im * ↑r) =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * (↑r * ↑r)
⊢ ↑a.re * ↑b.re + ↑d * ↑a.im * ↑b.im + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r =
    ↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * ↑r + ↑a.im * ↑b.im * ↑d

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
r : { r // r * r = ↑d }
a b : ℤ√d
⊢ ↑a.re + ↑b.re + (↑a.im + ↑b.im) * ↑r = ↑a.re + ↑a.im * ↑r + (↑b.re + ↑b.im * ↑r)

Tactic:
ring

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

Goal state before:
pp: case e'_3
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m ↦ ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ m ∈ D, f m ≠ ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * (↑y - ↑x) - (↑⌊ξ * ↑y⌋ - ↑⌊ξ * ↑x⌋)) * (↑n + 1) =
    (ξ * ↑y - ↑⌊ξ * ↑y⌋) * (↑n + 1) - (ξ * ↑x - ↑⌊ξ * ↑x⌋) * (↑n + 1)

Tactic:
ring

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

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
intro xy hxy

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : xy ∈ f '' s
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
Module: Mathlib.NumberTheory.LSeries.Convergence

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x
⊢ x = x + 1 - 1

Tactic:
ring

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

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
h : f =O[atTop] fun n ↦ ↑n ^ x
⊢ x = x + 1 - 1

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1 = 2 * ↑a * ↑y - ↑y * ↑y - 1

Tactic:
ring

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ ⇑f ⍟ ⇑g = ⇑(f * g)

Tactic:
by
  simp [convolution]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ ↑v + -(1 / 2) = (2 * ↑v - 1) / 2

Tactic:
ring

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

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
⊢ HasProd (fun p ↦ (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)

Tactic:
have H : (fun p : Primes ↦ (1 - f p)⁻¹) = fun p : Primes ↦ ∑' (e : ℕ), f (p ^ e) :=
    funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum

Goal state after:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →*₀ F
hsum : Summable fun x ↦ ‖f x‖
H : (fun p ↦ (1 - f ↑p)⁻¹) = fun p ↦ ∑' (e : ℕ), f (↑p ^ e)
⊢ HasProd (fun p ↦ (1 - f ↑p)⁻¹) (∑' (n : ℕ), f n)
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 = ∏' (n : { n // IsPrimePow n }), f ↑n

Tactic:
exact (tprod_subtype_eq_of_mulSupport_subset hf).symm

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

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑π * (2 * ↑n) * z * I + ↑π * ↑n ^ 2 * τ * I

Tactic:
ring

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

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ -π * (t * ↑n ^ 2 - 2 * (|a| * (t * ↑n))) + -π * (a ^ 2 * t) - -π * ((↑n + a) ^ 2 * t) = π * t * ↑n * (|a| + a) * 2

Tactic:
ring

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

Goal state before:
pp: S T : ℝ
hT : 0 < T
k n : ℕ
⊢ -(-π * (T * ↑n ^ 2 - 2 * S * ↑n) - -1 * ↑n) = ↑n * (π * T * ↑n - (2 * π * S + 1))

Tactic:
ring

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

Goal state before:
pp: z τ : ℂ
h : Summable fun x ↦ jacobiTheta₂_term x z τ
hτ✝ : τ.im ≤ 0
hτ : τ.im < 0
n : ℕ
⊢ -π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im = ↑n * (↑n * (-π * τ.im) - 2 * π * z.im)

Tactic:
ring

Goal state after: