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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
by
  rw [theta_eq_log_primorial]
  trans log (4 ^ ⌊x⌋₊)
  · gcongr <;> norm_cast
    exacts [primorial_pos _, primorial_le_four_pow _]
  rw [Real.log_pow, mul_comm]
  gcongr
  exact floor_le hx

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.zero
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
⊢ (Rat.padicValuation p) (bernoulli (0 + 1) * ↑((2 * k + 1).choose (0 + 1)) * ↑p ^ (2 * k - (0 + 1)) / (2 * ↑k + 1)) ≤ 1

Tactic:
rw [zero_add, Nat.choose_one_right, bernoulli_one]

Goal state after:
case succ.zero
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hi : 0 + 1 < 2 * k
⊢ (Rat.padicValuation p) (-1 / 2 * ↑(2 * k + 1) * ↑p ^ (2 * k - 1) / (2 * ↑k + 1)) ≤ 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.refine_1
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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ Fin.cons j t' 0 = Fin.cons j t' i₁ ↔ ↑(cardPowDegree (A i₁ % b - A 0 % b)) < cardPowDegree b • ε

Tactic:
refine Fin.cases ?_ (fun i₁ => ?_) i₁

Goal state after:
case succ.refine_1.refine_1
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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ Fin.cons j t' 0 = Fin.cons j t' 0 ↔ ↑(cardPowDegree (A 0 % b - A 0 % b)) < cardPowDegree b • ε

case succ.refine_1.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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁✝ : Fin (n + 1)
i₁ : Fin n
⊢ Fin.cons j t' 0 = Fin.cons j t' i₁.succ ↔ ↑(cardPowDegree (A i₁.succ % b - A 0 % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁ : Fin (n + 1)
i₀ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀.succ % b)) < cardPowDegree b • ε

Tactic:
refine Fin.cases ?_ (fun i₁ => ?_) i₁

Goal state after:
case succ.refine_2.refine_1
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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁ : Fin (n + 1)
i₀ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' 0 ↔ ↑(cardPowDegree (A 0 % b - A i₀.succ % b)) < cardPowDegree b • ε

case succ.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 • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁✝ : Fin (n + 1)
i₀ i₁ : Fin n
⊢ Fin.cons j t' i₀.succ = Fin.cons j t' i₁.succ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε
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
j : Fin (cardM bS adm).succ
i : ι
x✝ : i ∈ Finset.univ
⊢ b • qs j i • bS i + rs j i • bS i = b • ((b * qs j i + rs j i) / b) • bS i + ((b * qs j i + rs j i) % b) • bS i

Tactic:
← μ_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
j : Fin (cardM bS adm).succ
i : ι
x✝ : i ∈ Finset.univ
⊢ b • qs j i • bS i + rs j i • bS i = b • (μ j * s i / b) • bS i + (μ j * s i % b) • bS i
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
let n := modPart p r

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
n : ℤ := modPart p r
⊢ ‖⟨↑r, h⟩ - ↑(modPart p r)‖ < 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case refine_2.refine_1
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₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ 0
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
⊢ False

Tactic:
have := (Classical.choose_spec (hg j₀)).2

Goal state after:
case refine_2.refine_1
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₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ 0
approx : ¬cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
this : cardPowDegree b • ε ≤ ↑(cardPowDegree (A 0 % b - A (Classical.choose ⋯).succ % b))
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case hf_diff
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (fun n ↦ (log n)⁻¹) t

pp: case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume

Tactic:
· -- Differentiability
    intro z ⟨_, _⟩
    have : z ≠ 0 := by linarith
    have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> linarith
    fun_prop

Goal state after:
case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
⊢ IntegrableOn (deriv fun n ↦ (log n)⁻¹) (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := ⋯
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ∑ n ∈ Icc 0 ⌊x⌋₊, log ↑n * a n

Tactic:
refine sum_congr rfl fun n _ ↦ ?_
    split_ifs with h <;> simp [a, h]

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

Goal state before:
pp: case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(x.appr n) = 0
⊢ x.appr n < p ^ (n + 1)

pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)

Tactic:
· apply lt_trans (ih _) hp

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)
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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ⋯
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
r' : S
hr' : (algebraMap R S) M ∣ r'
a : S
ha : a ∈ ↑I
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt : abv ((Algebra.norm R) (r • a - q * b)) < abv ((Algebra.norm R) b)
⊢ q * b ∣ r' * a

Tactic:
simp only [Algebra.smul_def] at lt

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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
r' : S
hr' : (algebraMap R S) M ∣ r'
a : S
ha : a ∈ ↑I
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt : abv ((Algebra.norm R) ((algebraMap R S) r * a - q * b)) < abv ((Algebra.norm R) b)
⊢ q * b ∣ r' * a
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
| ↑(p ^ i * p ^ k)

Tactic:
Nat.cast_mul

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
| ↑(p ^ i) * ↑(p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ log 4 * ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2|

Tactic:
abs_of_nonneg

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ log 4 * ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 = log 4 * ∫ (t : ℝ) in 2..x, 1 / log t ^ 2

x : ℝ
a✝ : 4 ≤ x
⊢ 0 ≤ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: 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
⊢ IsCauSeq (padicNorm p) fun n ↦ ↑(nthHom f r n)

Tactic:
intro ε hε
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (p : ℚ) ^ (-((k : ℕ) : ℤ)) < ε := exists_pow_neg_lt_rat p hε
  use k
  intro j hj
  refine lt_of_le_of_lt ?_ hk
  -- Need to do beta reduction first, as `norm_cast` doesn't.
  -- Added to adapt to https://github.com/leanprover/lean4/pull/2734.
  beta_reduce
  norm_cast
  rw [← padicNorm.dvd_iff_norm_le]
  exact mod_cast pow_dvd_nthHom_sub f_compat r k j hj

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

Goal state before:
pp: case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ ZMod.cast 1 = 1

Tactic:
ZMod.cast_eq_val,

Goal state after:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ ↑(ZMod.val 1) = 1
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 * b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))

Tactic:
exact Algebra.trace_localization R M _

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

Goal state before:
pp: 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
⊢ limNthHom f_compat 0 = 0

Tactic:
simp [limNthHom]; rfl

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

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis

Tactic:
have H₂ : (aeval (hζ.subOnePowerBasis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.powerBasis ℚ).gen := by simp

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
ce : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
H₁ : (aeval (IsPrimitiveRoot.powerBasis ℚ hζ).gen) (X - 1) = (subOnePowerBasis ℚ hζ).gen
H₂ : (aeval (subOnePowerBasis ℚ hζ).gen) (X + 1) = (IsPrimitiveRoot.powerBasis ℚ hζ).gen
⊢ discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = discr ℚ ⇑(subOnePowerBasis ℚ hζ).basis
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ x = y

Tactic:
← lift_self x,

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ (lift ⋯) x = y
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case succ
f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n N : ℕ
IH : ↑(f (N + n)) = ↑(f n)
⊢ ↑(f (N + 1 + n)) = ↑(f n)

Tactic:
rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
    exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ yn a1 n ^ 2 ∣ d a1 * yn a1 (n * k) * yn a1 n

Tactic:
sq

Goal state after:
case h₂
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ yn a1 n * yn a1 n ∣ d a1 * yn a1 (n * k) * yn a1 n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d a b : ℕ
⊢ Nonnegg c d (↑a) (-↑b) ↔ SqLe b c a d

Tactic:
nonnegg_comm

Goal state after:
c d a b : ℕ
⊢ Nonnegg d c (-↑b) ↑a ↔ SqLe b c a d
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case succ
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
· by_cases hk : p ^ (k + 1) = 2
    · obtain rfl : p = 2 := by
        rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
      nth_rw 2 [← pow_one 2] at hk
      replace hk := Nat.pow_right_injective rfl.le hk
      rw [add_eq_right] at hk
      subst hk
      rw [pow_one] at hζ hcycl
      have : natDegree (minpoly K ζ) = 1 := by
        rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
        exact natDegree_X_sub_C (-1)
      rcases Fin.equiv_iff_eq.2 this with ⟨e⟩
      rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]
      simp only [powerBasis_dim,
        zero_add, pow_one, totient_two, reduceDiv, pow_zero, cast_ofNat, tsub_self,
        Nat.add_one_sub_one, mul_one, mul_zero]
      simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
      convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
      · congr 1
        ext i
        simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
        suffices (e.symm i : ℕ) = 0 by simp [this]
        rw [← Nat.lt_one_iff]
        convert! (e.symm i).2
        rw [this]
      · simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]
        rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; simp
    · exact discr_prime_pow_ne_two hζ hirr hk

Goal state after: