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

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k
⊢ f ↑2 * c 2 + ∑ k ∈ Ioc ⌊2⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
sum_mul_eq_sub_sub_integral_mul c zero_le_two hb hf_diff hf_int

Goal state after:
case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f ↑2 * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k
⊢ f ↑2 * c 2 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 2 * ∑ k ∈ Icc 0 ⌊2⌋₊, c k -
        ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 2 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)! * ↑p ! =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
refine sum_congr rfl fun x _ => ?_

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p ↦ bernoulli p / ↑p !) * PowerSeries.mk fun q ↦ (coeff (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p ↦ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / (↑p + 1)
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
refine summable_mul_of_bigO_atTop_aux c 0 h_bdd (by rwa [Nat.cast_zero]) (fun n ↦ ?_) hg₁ hg₂

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

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
by_cases! le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊

Goal state after:
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : b.natDegree ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree 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:
← Int.lt_ceil

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

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

Tactic:
rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,
    show 2 * k + 1 - 2 * k = 1 by lia]

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

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

Tactic:
by
  have hfilter : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) = ∑ v ∈ range p, (v : ℚ) ^ (2 * k) := by
    cases p <;> simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]
  rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,
    show 2 * k + 1 - 2 * k = 1 by lia]
  push_cast
  field_simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
rw [show 2 * k + 1 - i = (2 * k - i) + 1 by lia, pow_succ]

Goal state after:
k p : ℕ
inst✝ : Fact (Nat.Prime p)
hp_ne : ↑p ≠ 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * ↑((2 * k + 1).choose i) * (↑p ^ (2 * k - i) * ↑p) / (2 * ↑k + 1) / ↑p =
    bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ x

Tactic:
by
  grw [psi_eq_psi_coe_floor, ← psi_ge]
  gcongr
  · exact (Nat.sub_one_lt_floor x).le
  · exact floor_le hx
  · exact one_le_two

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den

Tactic:
obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, m > 0 → ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p).den
hk : k > 0
T : ℤ
hT :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den
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 ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ ∑ x, rs k x • (bS.repr (bS x)) i - ∑ x, rs j x • (bS.repr (bS x)) i = rs k i - rs j i

Tactic:
Basis.repr_self_apply,

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 ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq✝ : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
hjk' : ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε
q : S := ∑ i, (qs k i - qs j i) • bS i
r : R := μ k - μ j
r_eq : r = μ k - μ j
this : r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)
i : ι
⊢ ((∑ x, rs k x • if x = i then 1 else 0) - ∑ x, rs j x • if x = i then 1 else 0) = rs k i - rs j i
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
by
  rcases eq_or_ne ‖(x.zmodRepr : ℤ_[p])‖ ‖x‖ with H | H
  · rw [H]
  · have := x.norm_sub_zmodRepr_lt_one
    constructor <;> intro h <;> rw [← h] at this ⊢
    · exact norm_eq_of_norm_sub_lt_right this
    · exact (norm_eq_of_norm_sub_lt_left this).symm

Goal state after:
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
⊢ ↑0 = 0

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
⊢ 0 - ↑(f 0) ∈ 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
⊢ 0 - ↑0 ∈ Ideal.span {↑v}

Tactic:
cast_zero

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
⊢ 0 = 0

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
⊢ 0 - ↑(f 0) ∈ 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
⊢ 0 - ↑0 ∈ Ideal.span {↑v}
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
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:
refine ContinuousOn.integrableOn_Icc fun z ⟨_, _⟩ ↦ ContinuousWithinAt.congr ?_
      (fun _ _ ↦ deriv_inv_log_apply) deriv_inv_log_apply

Goal state after:
case hf_int
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ log ↑n
z : ℝ
x✝ : z ∈ Set.Icc 2 x
left✝ : 2 ≤ z
right✝ : z ≤ x
⊢ ContinuousWithinAt (fun x ↦ -x⁻¹ / log x ^ 2) (Set.Icc 2 x) z
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:

Tactic:
_ ≤ ∫ x in a..b, 1 / log a ^ 2 := by
      refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound
      apply intervalIntegrable_one_div_log_sq <;> linarith
  _ ≤ _ := by simp [field]

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

Goal state before:
pp: case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑0 = 0

pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Tactic:
cast_zero

Goal state after:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ 0 = 0

p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.NumberField.Discriminant.Defs

Goal state before:
pp: ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ (algebraMap ℤ ℚ) r * (algebraMap ℤ ℚ) r' = 1

Tactic:
hr,

Goal state after:
ι : Type u_2
ι' : Type u_3
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq ι'
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
inst✝ : NumberField K
b : Basis ι ℚ K
b' : Basis ι' ℚ K
h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)
h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)
hint : IsIntegral ℤ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
r : ℤ
hr : (algebraMap ℤ ℚ) r = ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det
this : IsIntegral ℤ (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
r' : ℤ
hr' : (algebraMap ℤ ℚ) r' = (b'.toMatrix ⇑(b.reindex (b.indexEquiv b'))).det
⊢ ((b.reindex (b.indexEquiv b')).toMatrix ⇑b').det * (algebraMap ℤ ℚ) r' = 1
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det

Tactic:
exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g') ↔ g = g'

Tactic:
by
  constructor
  · intro hg
    ext x : 1
    apply ext_of_toZModPow.mp
    intro n
    change (toZModPow n).comp g x = (toZModPow n).comp g' x
    rw [hg n]
  · rintro rfl _
    rfl

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)

Tactic:
rcases eq_or_ne p 2 with (rfl | hp2)

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

case e_a.inr
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
hp2 : p ≠ 2
⊢ (-1) ^ (p ^ k * (p - 1) * (p ^ k * (p - 1) - 1) / 2) = (-1) ^ (p ^ k * (p - 1) / 2)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 (n + 1) * { re := ↑a, im := -1 }
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n

Tactic:
pellZd_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
t : b * { re := ↑a, im := -1 } ≤ pellZd a1 n * { re := ↑a, im := 1 } * { re := ↑a, im := -1 }
⊢ b * { re := ↑a, im := -1 } ≤ pellZd a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b * { re := ↑a, im := -1 } * { re := ↑a, im := 1 } = pellZd a1 (m + 1)

Tactic:
pellZd_succ,

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b * { re := ↑a, im := -1 } * { re := ↑a, im := 1 } = pellZd a1 m * { re := ↑a, im := 1 }
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
pellZd_succ,

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 (m + n) * { re := ↑a, im := 1 } = pellZd a1 m * pellZd a1 (n + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 (m + n) * { re := ↑a, im := 1 } = pellZd a1 m * pellZd a1 (n + 1)

Tactic:
pellZd_succ,

Goal state after:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ pellZd a1 (m + n) * { re := ↑a, im := 1 } = pellZd a1 m * (pellZd a1 n * { re := ↑a, im := 1 })
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ
⊢ (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)

Tactic:
by
  ring

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ p (v ⊗ t ∘ inl) = 0

Tactic:
rwa [show (v ⊗ t) ∘ (inl ⊗ inr ∘ inl) = v ⊗ t ∘ inl from
                    funext fun s => by rcases s with a | b <;> rfl] at hl

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

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

Tactic:
heven.neg_one_pow

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))