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

Goal state before:
pp: case refine_1
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 j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j

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
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₁)

Tactic:
·

Goal state after:
case refine_1
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 j : Fin (M ^ n).succ
h : (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i = (fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) j
⊢ i = j
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
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) 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
⊢ t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₀) = t ((fun i ↦ {x | t x = s}.toList[Fin.castLE this i]) i₁)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case refine_1
𝕜 : 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
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖if k = 0 then 0 else c k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖if k = 0 then 0 else c k‖ -
      ∫ (t : ℝ) in Set.Ioc ↑1 ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖if k = 0 then 0 else c k‖

pp: case refine_2
𝕜 : 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
⊢ (fun n ↦ f ↑n * if n = 0 then 0 else c n) =ᶠ[atTop] fun n ↦ f ↑n * c n

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
n : ℕ
⊢ ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖if k = 0 then 0 else c k‖ =
    ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖if k = 0 then 0 else c k‖ -
      ∫ (t : ℝ) in Set.Ioc ↑1 ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖if k = 0 then 0 else c k‖
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
⊢ (d + 1).factorization p ≤ d - 1

pp: case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ (d + 1).factorization p ≤ d - 1

Tactic:
·

Goal state after:
case pos
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : p = 2 ∧ d = 2
⊢ (d + 1).factorization p ≤ d - 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ (d + 1).factorization p ≤ d - 1

Tactic:
·

Goal state after:
case neg
p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ (d + 1).factorization p ≤ d - 1
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case succ.refine_1
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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i : Fin (n + 1)
⊢ ↑(abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < abv b • ε

pp: case succ.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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i✝ : Fin (n + 1)
i : Fin n
⊢ ↑(abv (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) < abv b • ε

Tactic:
·

Goal state after:
case succ.refine_1
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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i : Fin (n + 1)
⊢ ↑(abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < abv b • ε
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)

pp: case neg
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:
·

Goal state after:
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)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue

Goal state before:
pp: case succ.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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i✝ : Fin (n + 1)
i : Fin n
⊢ ↑(abv (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) < abv b • ε

Tactic:
·

Goal state after:
case succ.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 ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (M ^ n).succ), ↑(abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < abv b • ε
k₀ k₁ : Fin (h✝.card ε ^ n).succ
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < abv b • ε
i✝ : Fin (n + 1)
i : Fin n
⊢ ↑(abv (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) < abv b • ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
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:
·

Goal state after:
case neg
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)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ (fun n ↦ f ↑n * if n = 0 then 0 else c n) =ᶠ[atTop] fun n ↦ f ↑n * c n

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
⊢ (fun n ↦ f ↑n * if n = 0 then 0 else c n) =ᶠ[atTop] fun n ↦ f ↑n * c n
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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)
⊢ 0 < p

Tactic:
by lia

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

Goal state before:
pp: case refine_1
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
⊢ ⌊↑(A i % b) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊

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:
·

Goal state after:
case refine_1
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
⊢ ⌊↑(A i % b) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
by_cases! hbj : degree b ≤ j

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ ↑j
⊢ (A i₁).coeff j = (A i₀).coeff j

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ ↑j
⊢ (A i₁).coeff j = (A i₀).coeff j

pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
·

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ ↑j
⊢ (A i₁).coeff j = (A i₀).coeff j
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
⊢ d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k

Tactic:
by lia

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

Goal state before:
pp: case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := ⋯
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ (A i₁ - A i₀).degree < ↑(b.natDegree - d)

Tactic:
refine (degree_lt_iff_coeff_zero _ _).mpr fun j hj => ?_

Goal state after:
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
⊢ (A i₁ - A i₀).coeff j = 0
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
by_cases! hbj : degree b ≤ j

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).coeff j = 0

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < b.degree
⊢ (A i₁ - A i₀).coeff j = 0
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).coeff j = 0

pp: case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : ↑j < b.degree
⊢ (A i₁ - A i₀).coeff j = 0

Tactic:
·

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ ↑j
⊢ (A i₁ - A i₀).coeff j = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 < ↑n

pp: case refine_2
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}

Tactic:
·

Goal state after:
case refine_1
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ 1 < ↑n
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}

Tactic:
·

Goal state after:
case refine_2
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}