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

Goal state before:
pp: case pos
n i : ℕ
h : i ≤ n + 1
h' : i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 1)

pp: case neg
n i : ℕ
h : i ≤ n + 1
h' : ¬i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 0)

pp: case pos
n i : ℕ
h : ¬i ≤ n + 1
h✝ : i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 1)

pp: case neg
n i : ℕ
h : ¬i ≤ n + 1
h✝ : ¬i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 0)

Tactic:
· subst h'
    simp
    grind

Goal state after:
case neg
n i : ℕ
h : i ≤ n + 1
h' : ¬i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 0)

case pos
n i : ℕ
h : ¬i ≤ n + 1
h✝ : i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 1)

case neg
n i : ℕ
h : ¬i ≤ n + 1
h✝ : ¬i = n + 1 - 1
⊢ 0 * (-1) ^ i = (-1) ^ (n + 1) • (0 + (n + 1) • 0)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
⊢ ∑ i ∈ range 0, ‖f ↑i * c i‖ ≤ max (C₁ + C₂) 1

Tactic:
simp only [range_zero, norm_mul, sum_empty, le_sup_iff, zero_le_one, or_true]

Goal state after:
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
⊢ -1 / 2 * (↑p + 1 + 1) * ↑n ^ (p + 1 - 0) / (↑p + 1 + 1) + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ

Tactic:
tsub_zero,

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
⊢ -1 / 2 * (↑p + 1 + 1) * ↑n ^ (p + 1) / (↑p + 1 + 1) + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ p < 2 * k + 2

Tactic:
have := Nat.le_of_dvd (by lia) hdvd; lia

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

Goal state before:
pp: 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
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < degree 0
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝² : k₁ ≤ N
a✝¹ : p₁ ≠ 0
a✝ : ↑p₁ ≤ x
⊢ Nat.Prime p₁ →
    ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
      ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b

Tactic:
hp₁

Goal state after:
case refine_2
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
k₁ p₁ : ℕ
hk₁ : k₁ ≠ 0
a✝² : k₁ ≤ N
a✝¹ : p₁ ≠ 0
a✝ : ↑p₁ ≤ x
hp₁ : Nat.Prime p₁
⊢ ↑p₁ ≤ x ^ (↑k₁)⁻¹ →
    ∀ (a b : ℕ), a ≠ 0 → a ≤ N → b ≠ 0 → ↑b ≤ x → Nat.Prime b → ↑b ≤ x ^ (↑a)⁻¹ → p₁ ^ k₁ = b ^ a → k₁ = a ∧ p₁ = b
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) (-1 / 2 * ↑(2 * k + 1) * ↑p ^ (2 * k - 1) / (2 * ↑k + 1)) ≤ 1

Tactic:
push_cast

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.Bernoulli

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

Tactic:
push_cast

Goal state after:
case succ.zero.inl
k : ℕ
hk : k > 0
hi : 0 + 1 < 2 * k
inst✝ : Fact (Nat.Prime 2)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / ↑2)
⊢ (Rat.padicValuation 2) (-(2 ^ (2 * k - 1) / 2)) ≤ 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
x : R
⊢ x ∈ finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x

Tactic:
simp only [finsetApprox, Finset.mem_erase, Finset.mem_image]

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
x : R
⊢ (x ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x) ↔
    ∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = 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 j : Fin (cardM bS adm).succ
left✝ : (i, j) ∈ Finset.univ
hx : (distinctElems bS adm) (i, j).1 - (distinctElems bS adm) (i, j).2 ≠ 0
⊢ i ≠ j

Tactic:
rintro rfl

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

Goal state before:
pp: k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ x ∈ range (2 * k), bernoulli x * ↑((2 * k + 1).choose x) * ↑p ^ (2 * k + 1 - x) / (↑(2 * k) + 1) +
      bernoulli (2 * k) * ↑(2 * k + 1) * ↑p ^ 1 / (↑(2 * k) + 1) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)

Tactic:
push_cast

Goal state after:
k p : ℕ
hk : 0 < k
hfilter : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) = ∑ v ∈ range p, ↑v ^ (2 * k)
⊢ ∑ x ∈ range (2 * k), bernoulli x * ↑((2 * k + 1).choose x) * ↑p ^ (2 * k + 1 - x) / (2 * ↑k + 1) +
      bernoulli (2 * k) * (2 * ↑k + 1) * ↑p ^ 1 / (2 * ↑k + 1) =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) +
      ↑p * bernoulli (2 * k)
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_3
K : Type u_4
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Algebra F⟮X⟯ K
inst✝² : FunctionField F K
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F F⟮X⟯ K
⊢ Algebra.IsAlgebraic (↥F⟮(algebraMap F⟮X⟯ K) X⟯) K

Tactic:
exact .tower_top (K := F⟮(X : F⟮X⟯)⟯) _

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

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

Tactic:
push_cast

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ ↑r.num - ↑r.num * ↑(r.den.gcdA p) * ↑r.den = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ↑(∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then 1 else 0) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
push_cast

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_1
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
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ J ≠ 0

Tactic:
rintro rfl

Goal state after:
case refine_1
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
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * 0
⊢ False
Module: Mathlib.NumberTheory.Padics.RingHoms

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

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

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

Tactic:
cast_add

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

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

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f x + f y) ∈ Ideal.span {↑v}
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
cast_add

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - (↑(f x) + ↑(f y)) = x - ↑(f x) + (y - ↑(f y))
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
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n + p ^ n * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val)

Tactic:
push_cast

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
⊢ ↑p ^ (n + 1) ∣
    x - (↑(x.appr n) + ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: 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
⊢ c ≠ 0

Tactic:
rintro rfl

Goal state after:
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
hc : x - ↑(x.appr n) = ↑p ^ n * 0
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity

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

Goal state before:
pp: case ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑a ∈ Ideal.span {↑p ^ n}

pp: case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑b ∈ Ideal.span {↑p ^ n}

Tactic:
· simpa using ha

Goal state after:
case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑(p ^ n)}
hb : x - ↑b ∈ Ideal.span {↑(p ^ n)}
⊢ x - ↑b ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a.inl
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)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * (1 - 0) * (2 ^ k.succ * (1 - 0) - 1) / 2) = (-1) ^ (2 ^ k.succ * (1 - 0) / 2)

Tactic:
tsub_zero,

Goal state after:
case e_a.inl
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)
k : ℕ
inst✝ : IsCyclotomicExtension {2 ^ (k.succ + 1)} K L
hζ : IsPrimitiveRoot ζ (2 ^ (k.succ + 1))
hirr : Irreducible (cyclotomic (2 ^ (k.succ + 1)) K)
hk : 2 ^ (k.succ + 1) ≠ 2
hne : NeZero ↑(2 ^ (k.succ + 1))
hp2 : 2 = 2 → k.succ ≠ 0
⊢ (-1) ^ (2 ^ k.succ * 1 * (2 ^ k.succ * 1 - 1) / 2) = (-1) ^ (2 ^ k.succ * 1 / 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: f : ℕ → ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), ↑p ^ i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := ⟨fun x ↦ ↑(f x), ⋯⟩
hs : ↑x = mk s
e : ℤ_[p]
he : x = ↑p ^ n * e + ↑(x.appr n)
N : ℕ
hN : ‖↑p ^ n * ↑e + ↑(↑(x.appr n) - f (N + n))‖ < ↑p ^ (-↑n)
H : ↑p ^ (-↑n) < ‖↑(↑(x.appr n) - f (N + n))‖
⊢ ‖↑p ^ n * ↑e‖ ≤ ↑p ^ (-↑n)

Tactic:
simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one

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
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)

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
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
· rcases eq_or_ne p 2 with (rfl | hp2)
    · rcases Nat.exists_eq_succ_of_ne_zero (hp2 rfl) with ⟨k, rfl⟩
      rw [succ_sub_succ_eq_sub, tsub_zero, mul_one]; simp only [_root_.pow_succ']
      rw [mul_assoc, Nat.mul_div_cancel_left _ zero_lt_two, Nat.mul_div_cancel_left _ zero_lt_two]
      cases k
      · simp
      · simp_rw [_root_.pow_succ', (even_two.mul_right _).neg_one_pow,
          ((even_two.mul_right _).mul_right _).neg_one_pow]
    · have hpo : Odd p := hp.out.odd_of_ne_two hp2
      obtain ⟨a, ha⟩ := (hp.out.even_sub_one hp2).two_dvd
      rw [ha, mul_left_comm, mul_assoc, Nat.mul_div_cancel_left _ two_pos,
        Nat.mul_div_cancel_left _ two_pos, mul_right_comm, pow_mul, (hpo.pow.mul _).neg_one_pow,
        pow_mul, hpo.pow.neg_one_pow]
      refine Nat.Even.sub_odd ?_ (even_two_mul _) odd_one
      rw [mul_left_comm, ← ha]
      exact one_le_mul (one_le_pow _ _ hp.1.pos) (succ_le_iff.2 <| tsub_pos_of_lt hp.1.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
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ x✝ : Poly α
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
by ext; simp only [add_apply, mul_apply]; apply add_mul

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
injection pellZd_add a1 m n with _ h

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq✝ : ↑(xn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).re + ↑(d a1) * (pellZd a1 m).im * (pellZd a1 n).im
h : ↑(yn a1 (m + n)) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
a : α
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inl a) = (v ⊗ t) (inl a)

Tactic:
dsimp [(· ∘ ·)]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ ((v ⊗ (0 ::ₒ t) ∘ g) ∘ (inl ⊗ inr ∘ f)) (inr b) = (v ⊗ t) (inr b)

Tactic:
dsimp [(· ∘ ·)]

Goal state after:
case inr
α β γ : Type u
f : β → γ
g : γ → Option β
inv : ∀ (x : β), g (f x) = some x
p : Poly (α ⊕ β)
v : α → ℕ
t : β → ℕ
ht : p (v ⊗ t) = 0
b : β
⊢ (0 ::ₒ t) (g (f b)) = t b
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
h : ↑x.norm = ↑↑1
hx : 0 ≤ x.norm
⊢ 1 = x * star x

Tactic:
norm_eq_mul_conj,

Goal state after:
d : ℤ
x : ℤ√d
h : x * star x = ↑↑1
hx : 0 ≤ x.norm
⊢ 1 = x * star x
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
x : ℤ√d
h : -↑x.norm = ↑↑1
hx : x.norm ≤ 0
⊢ 1 = x * -star x

Tactic:
norm_eq_mul_conj,

Goal state after:
d : ℤ
x : ℤ√d
h : -(x * star x) = ↑↑1
hx : x.norm ≤ 0
⊢ 1 = x * -star x
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mpr
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → z.norm = 0

Tactic:
rintro rfl

Goal state after:
case mpr
d : ℤ
hd : d < 0
⊢ norm 0 = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

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

Tactic:
rw [add_comm, add_comm (y : ℤ)]

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

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))

Tactic:
let k2nl : 2 * n - k < n := by lia

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
⊢ ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) ↑a.norm = 0

Tactic:
norm_eq_mul_conj,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
d : ℤ
r : { r // r * r = ↑d }
hd : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : (lift r) a = 0
h_inj : Function.Injective Int.cast
⊢ (lift r) (a * star a) = 0