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

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i

Tactic:
[

Goal state after:
n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ‖if True then 0 else c 0‖ + ∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
n : ℕ
⊢ ∑ k ∈ Icc 1 n, ‖c k‖ = ‖if True then 0 else c 0‖ + ∑ x ∈ Icc 1 n, ‖if x = 0 then 0 else c x‖
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
⊢ Summable fun n ↦ f ↑n * c n

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 1 n, ‖c k‖) =O[atTop] fun x ↦ 1
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
⊢ Summable fun n ↦ f ↑n * c n
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝¹ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this✝ : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
this : ∀ (i : Fin (M ^ n).succ), t {x | t x = s}.toList[Fin.castLE this✝ i] = s
⊢ t {x | t x = s}.toList[Fin.castLE this✝ i₀] = t {x | t x = s}.toList[Fin.castLE this✝ i₁]

Tactic:
[

Goal state after:
case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝¹ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this✝ : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
this : ∀ (i : Fin (M ^ n).succ), t {x | t x = s}.toList[Fin.castLE this✝ i] = s
⊢ t {x | t x = s}.toList[Fin.castLE this✝ i₀] = t {x | t x = s}.toList[Fin.castLE this✝ i₁]
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this✝¹ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht : ∀ (i₀ i₁ : Fin (M ^ n.succ).succ), t i₀ = t i₁ → ↑(abv (A i₁ 0 % b - A i₀ 0 % b)) < abv b • ε
s : Fin M
hs : M ^ n < {x | t x = s}.card
this✝ : (M ^ n).succ ≤ {x | t x = s}.toList.length
i₀ i₁ : Fin (M ^ n).succ
this : ∀ (i : Fin (M ^ n).succ), t {x | t x = s}.toList[Fin.castLE this✝ i] = s
⊢ t {x | t x = s}.toList[Fin.castLE this✝ i₀] = t {x | t x = s}.toList[Fin.castLE this✝ i₁]

Tactic:
this

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : p = 2 ∧ m = 2
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)

Tactic:
obtain ⟨rfl, rfl⟩ := hm2; norm_num

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
k : ℕ
hk : k ≠ 0
⊢ (f ↑k * if k = 0 then 0 else c k) = f ↑k * c k

Tactic:
[

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖f x‖) t
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici 1) volume
g : ℝ → ℝ
hg₂ : IntegrableAtFilter g atTop volume
h : ∀ (n : ℕ), ∑ k ∈ Icc 1 n, ‖c k‖ = ∑ k ∈ Icc 0 n, ‖(fun n ↦ if n = 0 then 0 else c n) k‖
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ x ∈ Icc 0 n, ‖if x = 0 then 0 else c x‖) =O[atTop] fun x ↦ 1
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ x ∈ Icc 0 ⌊t⌋₊, ‖if x = 0 then 0 else c x‖) =O[atTop] g
k : ℕ
hk : k ≠ 0
⊢ (f ↑k * if k = 0 then 0 else c k) = f ↑k * c k
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs

Goal state before:
pp: case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
⊢ ∀ (i₀ i₁ : Fin n),
    (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁ →
      ↑|A i₁ % b - A i₀ % b| < |b| • ε

Tactic:
intro i₀

Goal state after:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ : Fin n
⊢ ∀ (i₁ : Fin n),
    (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i ↦ ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁ →
      ↑|A i₁ % b - A i₀ % b| < |b| • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

Tactic:
[

Goal state after:
n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ↑(π ⌊x⌋₊) * log ↑⌊x⌋₊ ≤ ↑(π ⌊x⌋₊) * log x

Tactic:
rcases lt_or_ge x 1 with h | h

Goal state after:
case inl
x : ℝ
h : x < 1
⊢ ↑(π ⌊x⌋₊) * log ↑⌊x⌋₊ ≤ ↑(π ⌊x⌋₊) * log x

case inr
x : ℝ
h : 1 ≤ x
⊢ ↑(π ⌊x⌋₊) * log ↑⌊x⌋₊ ≤ ↑(π ⌊x⌋₊) * log x
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case mp
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
i : Fin (cardM bS adm).succ
left✝ : (i, i) ∈ Finset.univ
hx : (distinctElems bS adm) (i, i).1 - (distinctElems bS adm) (i, i).2 ≠ 0
⊢ False

Tactic:
simp at hx

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

Goal state before:
pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤
    max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)

Tactic:
have : (1 : ℤ) ≤ Fintype.card Fq := mod_cast (@Fintype.one_lt_card Fq _ _).le

Goal state after:
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : cardPowDegree (x - y) < a
hyz : cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ (x - z).natDegree ≤
    max (↑(Fintype.card Fq) ^ (x - y).natDegree) (↑(Fintype.card Fq) ^ (y - z).natDegree)
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
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
have dim_pos := Fintype.card_pos_iff.mpr bS.index_nonempty

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

Goal state before:
pp: 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]
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)) < ε

Tactic:
[

Goal state after:
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]
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)) < ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ψ x = ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n))

Tactic:
[

Goal state after:
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ψ x = ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
rw [psi_eq_zero_of_lt_two hx, theta_eq_zero_of_lt_two hx, sub_zero, abs_zero]

Goal state after:
case pos
x : ℝ
hx✝ : 1 ≤ x
hx : x < 2
⊢ 0 ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ (1 / ↑i))| ≤ 2 * √x * log x

Tactic:
[

Goal state after:
case neg
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ (1 / ↑i))| ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
⊢ N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊ → ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
hN

Goal state after:
case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
[

Goal state after:
case h
x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a.refine_1
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ (algebraMap Ft K) (e 1) = 1

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a.refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
⊢ (algebraMap F⟮X⟯ K) 1 = 1

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a.refine_3
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a✝ b✝ : F⟮X⟯
⊢ (algebraMap Ft K) (e (a✝ * b✝)) = (algebraMap Ft K) (e a✝) * (algebraMap Ft K) (e b✝)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a.refine_4
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a✝ b✝ : F⟮X⟯
⊢ (algebraMap F⟮X⟯ K) (a✝ * b✝) = (algebraMap F⟮X⟯ K) a✝ * (algebraMap F⟮X⟯ K) b✝

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case e_a.refine_5
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
c : F⟮X⟯
x : K
a✝ : F[X]
⊢ (algebraMap Ft K) (e ((algebraMap F[X] F⟮X⟯) a✝)) = (algebraMap F⟮X⟯ K) ((algebraMap F[X] F⟮X⟯) a✝)

Tactic:
simp only [map_one, map_mul, AlgEquiv.commutes, ← IsScalarTower.algebraMap_apply]

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

Goal state before:
pp: case refine_2.refine_1.e_6
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 ι
ε : ℝ := ⋯
ε_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 := ⋯
s : ι →₀ R := ⋯
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := ⋯
rs : Fin (cardM bS adm).succ → ι → R := ⋯
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 := ⋯
r : R := ⋯
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ (bS.repr (∑ x, (rs k x • bS x - rs j x • bS x))) i = rs k i - rs j i

Tactic:
[

Goal state after:
case refine_2.refine_1.e_6
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 ι
ε : ℝ := ⋯
ε_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 := ⋯
s : ι →₀ R := ⋯
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := ⋯
rs : Fin (cardM bS adm).succ → ι → R := ⋯
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 := ⋯
r : R := ⋯
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ (bS.repr (∑ x, (rs k x • bS x - rs j x • bS x))) i = rs k i - rs j i
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∃ n < p, x - ↑n ∈ maximalIdeal ℤ_[p]

Tactic:
by
  simp only [maximalIdeal_eq_span_p, Ideal.mem_span_singleton, ← norm_lt_one_iff_dvd]
  obtain ⟨r, hr⟩ := rat_dense p (x : ℚ_[p]) zero_lt_one
  have H : ‖(r : ℚ_[p])‖ ≤ 1 := by
    rw [norm_sub_rev] at hr
    calc
      _ = ‖(r : ℚ_[p]) - x + x‖ := by ring_nf
      _ ≤ _ := Padic.nonarchimedean _ _
      _ ≤ _ := max_le (le_of_lt hr) x.2
  obtain ⟨n, hzn, hnp, hn⟩ := exists_mem_range_of_norm_rat_le_one r H
  lift n to ℕ using hzn
  use n
  constructor
  · exact mod_cast hnp
  simp only [norm_def, coe_sub, coe_natCast] at hn ⊢
  rw [show (x - n : ℚ_[p]) = x - r + (r - n) by ring]
  apply lt_of_le_of_lt (Padic.nonarchimedean _ _)
  apply max_lt hr
  simpa using hn

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (ψ - θ) =O[atTop] Real.sqrt

Tactic:
[

Goal state after:
⊢ (ψ - θ) =O[atTop] Real.sqrt
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case neg
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ 0 = (log ↑n)⁻¹ * a n

Tactic:
· simp [a, h]

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ (↑n).zmodRepr = n % p

Tactic:
nth_rw 1 [← Nat.mod_add_div n p]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ (↑(n % p + p * (n / p))).zmodRepr = n % p
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case hy₁
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ n % p < p

Tactic:
exact Nat.mod_lt _ (Nat.Prime.pos Fact.out)

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

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

Tactic:
apply pow_dvd_pow _ (Nat.le_add_right m k)

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
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))

Tactic:
exact IsIntegralClosure.algebraMap_injective _ R _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
[

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

Goal state before:
pp: A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i✝ j✝ : ι
⊢ traceMatrix A b i✝ j✝ = traceMatrix A (⇑f ∘ b) i✝ j✝

Tactic:
[

Goal state after:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i✝ j✝ : ι
⊢ traceMatrix A b i✝ j✝ = traceMatrix A (⇑f ∘ b) i✝ j✝