mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
set r := μ k - μ j with r_eq

Goal state after:
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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case e'_4
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p = |↑p|

pp: case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0

Tactic:
· simp

Goal state after:
case convert_3
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ ↑p ≠ 0
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.Coprime r.den

Tactic:
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right

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)
⊢ ¬p ∣ 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)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n ∈ Set.Ici 1

Tactic:
by grind

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)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n + 1 ∈ Set.Ici 1

Tactic:
by grind

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)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 5 * n ∈ Set.Ici 1

Tactic:
by grind

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)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n - 1 ∈ Set.Ici 1

Tactic:
by grind

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)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n - 1 ∈ Set.Ici 1

Tactic:
by grind

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)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n ∈ Set.Ici 1

Tactic:
by grind

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)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 6 * n + 1 ∈ Set.Ici 1

Tactic:
by grind

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)
this : ∑ n ∈ Icc 1 N, c x n ≤ ∑ n ∈ Icc 1 N, b x (5 * n)
n : ℕ
hn : 1 ≤ n ∧ n ≤ N
⊢ 7 * n ∈ Set.Ici 1

Tactic:
by grind

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
rcases norm_natCast_zmodRepr_eq x with h | h

Goal state after:
case inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : ‖↑x.zmodRepr‖ = 1
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
by grind

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

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs).cast

Tactic:
rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(↑p ^ n * c).valuation - ↑n).natAbs).cast
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(n + c.valuation) - ↑n).natAbs).cast

Tactic:
Nat.cast_add,

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑n + ↑c.valuation - ↑n).natAbs).cast
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
arg 2

Goal state after:
| fun x ↦ log x ^ 2 * √x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: | (fun x ↦ √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
arg 2

Goal state after:
| fun x ↦ √x / log 2 ^ 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ θ t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)

Tactic:
grw [theta_le_log4_mul_x (by linarith)]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
⊢ ∀ᶠ (x : ℝ) in atTop, ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x

Tactic:
filter_upwards [eventually_ge_atTop 2, this] with x hx hx2

Goal state after:
ε : ℝ
εpos : 0 < ε
this : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
⊢ ↑(π ⌊x⌋₊) ≤ (log 4 + ε) * x / log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ (↑0 * log 2 - log (↑0 + 1)) / log ↑0 ≤ ↑(π 0)

pp: case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

pp: case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
· simp

Goal state after:
case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

pp: case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
· simp

Goal state after:
case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = (Int.castRingHom ℤ_[p]) (↑p ^ n)

pp: case e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑((f n) r).val = (Int.castRingHom ℤ_[p]) (nthHom f r (max n k) - nthHom f r n)

Tactic:
· simp

Goal state after:
case e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (max n k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (max n k)) - ↑((f n) r).val = (Int.castRingHom ℤ_[p]) (nthHom f r (max n k) - nthHom f r n)
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inl.zero
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
inst✝ : IsCyclotomicExtension {2 ^ (succ 0 + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (succ 0 + 1))
hirr : Irreducible (cyclotomic (2 ^ (succ 0 + 1)) K)
hk : 2 ^ (succ 0 + 1) ≠ 2
hne : NeZero ↑(2 ^ (succ 0 + 1))
hp2 : 2 = 2 → succ 0 ≠ 0
⊢ (-1) ^ (2 ^ 0 * (2 * 2 ^ 0 - 1)) = (-1) ^ 2 ^ 0

pp: case e_a.inl.succ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ ((n✝ + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ ((n✝ + 1).succ + 1))
hirr : Irreducible (cyclotomic (2 ^ ((n✝ + 1).succ + 1)) K)
hk : 2 ^ ((n✝ + 1).succ + 1) ≠ 2
hne : NeZero ↑(2 ^ ((n✝ + 1).succ + 1))
hp2 : 2 = 2 → (n✝ + 1).succ ≠ 0
⊢ (-1) ^ (2 ^ (n✝ + 1) * (2 * 2 ^ (n✝ + 1) - 1)) = (-1) ^ 2 ^ (n✝ + 1)

Tactic:
· simp

Goal state after:
case e_a.inl.succ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp : Fact (Nat.Prime 2)
n✝ : ℕ
inst✝ : IsCyclotomicExtension {2 ^ ((n✝ + 1).succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ ((n✝ + 1).succ + 1))
hirr : Irreducible (cyclotomic (2 ^ ((n✝ + 1).succ + 1)) K)
hk : 2 ^ ((n✝ + 1).succ + 1) ≠ 2
hne : NeZero ↑(2 ^ ((n✝ + 1).succ + 1))
hp2 : 2 = 2 → (n✝ + 1).succ ≠ 0
⊢ (-1) ^ (2 ^ (n✝ + 1) * (2 * 2 ^ (n✝ + 1) - 1)) = (-1) ^ 2 ^ (n✝ + 1)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 0) x✝ = 0 x✝

Tactic:
rw [mul_apply, zero_apply, mul_zero]

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

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
have := mul_pos (succ_pos k) (tsub_pos_of_lt hp.out.one_lt)

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑p ^ (p ^ k * ((k + 1) * (p - 1)))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
this : 0 < k.succ * (p - 1)
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy zw
      have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
      refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
      convert! this using 1
      simp only [one_mul, Int.natCast_add, Int.natCast_mul]
      ring

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

Goal state before:
pp: case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy zw
      have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
      refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
      convert! this using 1
      simp only [one_mul, Int.natCast_add, Int.natCast_mul]
      ring

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

Goal state before:
pp: case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy zw
      have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
      refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
      convert! this using 1
      simp only [one_mul, Int.natCast_add, Int.natCast_mul]
      ring

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

Goal state before:
pp: case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy zw
      have :=
        Int.mul_nonneg (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le xy))
          (sub_nonneg_of_le (Int.ofNat_le_ofNat_of_le zw))
      refine Int.le_of_ofNat_le_ofNat (le_of_sub_nonneg ?_)
      convert! this using 1
      simp only [one_mul, Int.natCast_add, Int.natCast_mul]
      ring

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

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

Tactic:
norm_one,

Goal state after:
d : ℤ
x : ℤ√d
h : IsUnit x
y : ℤ√d
hy : 1 = x * y
this : Int.natAbs 1 = x.norm.natAbs * y.norm.natAbs
⊢ x.norm.natAbs = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
← norm_eq_one_iff,

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

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

Tactic:
Nat.cast_add,

Goal state after:
case inr.inl.inr.inl
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
this : { re := ↑x + ↑z, im := -↑(y + w) }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w }).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
Nat.cast_add,

Goal state after:
case inr.inl.inr.inl
d x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
z w : ℕ
hb : { re := ↑z, im := -↑w }.Nonneg
this : { re := ↑x + ↑z, im := -(↑y + ↑w) }.Nonneg
⊢ ({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w }).Nonneg
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 : -↑x + ↑z = -↑i
⊢ i ≤ x

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

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

Goal state before:
pp: case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
this : { re := -↑(x + z), im := ↑(y + w) }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
Nat.cast_add,

Goal state after:
case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
this : { re := -(↑x + ↑z), im := ↑(y + w) }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
this : { re := -(↑x + ↑z), im := ↑(y + w) }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg

Tactic:
Nat.cast_add,

Goal state after:
case inr.inr.inr.inr
d x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
z w : ℕ
hb : { re := -↑z, im := ↑w }.Nonneg
this : { re := -(↑x + ↑z), im := ↑y + ↑w }.Nonneg
⊢ ({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
ein,

Goal state after:
case refl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 n % xn a1 n < xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case refl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) + xn a1 i % xn a1 n < xn a1 n

Tactic:
rw [ein, Nat.mod_self, add_zero]

Goal state after:
case refl.inr
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
ij : i < n + 1
j2n : n + 1 ≤ 2 * n
jnn : n + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ n + 1 = 2)
o : n = n ∨ n < n
ein : i = n
⊢ xn a1 (n - 1) < xn a1 n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den

Tactic:
rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' hξ₀.ne', abs_div, abs_of_pos hξ₀,
        div_lt_iff₀ hξ₀, div_mul_comm, mul_one] at h

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ ∀ a ∈ replicate e p, ¬decide (a ∈ s) = true

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ ∀ a ∈ m.primeFactorsList, decide (a ∈ s) = true

Tactic:
by grind

Goal state after: