mathlib-initiative/mathlib-tactics huggingface dataset:
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
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
⊢ Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)

Tactic:
simpa using

Goal state after:
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)
⊢ Fintype.card Fq ^ d ≤ m
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
simpa using

Goal state after:
case refine_2
x : ℝ
hy : 2 ≤ x
this : 0 ≤ x
⊢ 2 ≤ ⌊x⌋₊ ∧ Nat.Prime 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case h
n k : ℕ
hk : k ∈ range (n + 1)
⊢ n.choose k ≤ n.lcmUpto

Tactic:
exact le_of_dvd (lcmUpto_pos n) (choose_dvd_lcmUpto <| by grind)

Goal state after:
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
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

Tactic:
rintro ⟨hx, ⟨i, j⟩, _, rfl⟩
    refine ⟨i, j, ?_, rfl⟩
    rintro rfl
    simp at hx

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ θ x ≤ ψ x

Tactic:
by_cases! h : x < 2

Goal state after:
case pos
x : ℝ
h : x < 2
⊢ θ x ≤ ψ x

case neg
x : ℝ
h : 2 ≤ x
⊢ θ x ≤ ψ x
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case h.e_a
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
hAlg :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)

Tactic:
simpa using

Goal state after:
case h.e_a
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
hT : ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T
hp_ne : ↑p ≠ 0
hAlg :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p =
    ↑T - (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p
⊢ (∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k + 1 - i) / (2 * ↑k + 1)) / ↑p =
    ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 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
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 • ε
⊢ ∀ (i : ι), ↑(abv (rs k i - rs j i)) < abv b • ε

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_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 • ε
⊢ ∀ (i : ι), ↑(abv (μ k * s i % b - μ j * s i % b)) < abv b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case succ.refine_1.refine_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ Fin.cons j t' 0 = Fin.cons j t' 0 ↔ ↑(cardPowDegree (A 0 % b - A 0 % b)) < cardPowDegree b • ε

Tactic:
simpa using

Goal state after:
case succ.refine_1.refine_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i₀ i₁ : Fin (n + 1)
⊢ 0 < ↑(cardPowDegree b) * ε
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ ¬IsField ↥(ringOfIntegers F K)

Tactic:
simpa using

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F[X] K
inst✝¹ : Algebra F⟮X⟯ K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ ¬IsField F[X]
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
simpa using

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n

Tactic:
simpa using

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
hm : x - ↑m ∈ Ideal.span {↑p}
hn : x - ↑n ∈ Ideal.span {↑p}
this : ↑↑m = ↑↑n
⊢ ↑m = ↑n
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1

Tactic:
simpa using

Goal state after:
case h.right
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑x - ↑r‖ < 1
H : ‖↑r‖ ≤ 1
n : ℕ
hnp : ↑n < ↑p
hn : ‖↑r - ↑↑↑n‖ < 1
⊢ ‖↑r - ↑n‖ < 1
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b')) * abv ((Algebra.norm R) (r • a - q * b)) <
    abv ((Algebra.norm R) ((algebraMap R S) b')) * abv ((Algebra.norm R) b)

Tactic:
refine
    lt_of_le_of_lt (le_of_eq ?_)
      (mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb))
        (abv.nonneg _))

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) ((algebraMap R S) b')) * abv ((Algebra.norm R) (r • a - q * b)) =
    abv ((Algebra.norm R) (r • a' - b' • q)) * abv ((Algebra.norm R) b)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < (0 + p').succ

Tactic:
simpa using

Goal state after:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ x.zmodRepr < p'.succ
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]

Tactic:
simpa using

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : toZMod x = 0
⊢ x ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
simpa using

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ¬IsUnit (x - (toZMod x).cast)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
f : ℝ → ℝ
u : ℝ
x✝ : u ∈ Set.uIcc 2 x
⊢ deriv (fun x ↦ log x) u * f u = f u / u

Tactic:
by rw [deriv_log, mul_comm, div_eq_mul_inv]

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

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ t ∈ rootsOfUnity n L, g ↑t = ↑(t ^ m)

Tactic:
simpa using

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
⊢ ∃ m, ∀ (t : Lˣ), t ^ n = 1 → g ↑t = ↑(t ^ m)
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}

Tactic:
simpa using

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

Goal state before:
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

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.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ (↑(x.appr n)).cast = 0 ↔ ↑(x.appr m) = 0

Tactic:
ZMod.cast_natCast (pow_dvd_pow p h),

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(x.appr n) = 0 ↔ ↑(x.appr m) = 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n) = toZModPow m

Tactic:
by
  apply ZMod.ringHom_eq_of_ker_eq
  ext x
  rw [RingHom.mem_ker, RingHom.mem_ker]
  simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]
  simp only [toZModPow, toZModHom, RingHom.coe_mk]
  dsimp
  rw [ZMod.cast_natCast (pow_dvd_pow p h),
    zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]
  · rw [sub_self]
    apply Ideal.zero_mem _
  · rw [Ideal.mem_span_singleton]
    rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩
    use c
    rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x

Tactic:
theta_le_log4_mul_x (by linarith),

Goal state after:
ε : ℝ
εpos : 0 < ε
this✝ : ∀ᶠ (x : ℝ) in atTop, ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : ‖∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)‖ ≤ ε * x / log x
this : 0 ≤ log x
⊢ log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ μ ^ (↑((autToPow R hμ) g)).val = μ ^ (↑((modularCyclotomicCharacter L ⋯) g.toRingEquiv)).val

Tactic:
simpa using

Goal state after:
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ g μ = μ ^ (modularCyclotomicCharacter.toFun n g.toRingEquiv).val
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_a.refine_1
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : (_ : L →ₐ[K] E) × E
hroots :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
hσ :
  σ.snd ≠ σ.fst pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval σ.snd (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
⊢ (aeval σ.snd) (minpoly K pb.gen) = 0

Tactic:
simpa using

Goal state after:
case e_a.refine_1
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : ((minpoly K pb.gen).aroots E).Nodup
σ : (_ : L →ₐ[K] E) × E
hroots :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval (σ pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
hσ :
  σ.snd ≠ σ.fst pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval σ.snd (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
⊢ eval σ.snd (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: 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
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ IsUnit (traceMatrix K ⇑B.basis).det

Tactic:
simpa using

Goal state after:
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
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ ¬(discr K fun i ↦ B.gen ^ ↑i) = 0
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

Goal state after:
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)⁻¹
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
simpa using

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 n * { re := ↑a, im := 1 })
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).re = (↑a * c).re → b.re = c.re

Tactic:
simpa using

Goal state after:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ a * b.re = a * c.re → b.re = c.re
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ (↑a * b).im = (↑a * c).im → b.im = c.im

Tactic:
simpa using

Goal state after:
d a : ℤ
b c : ℤ√d
ha : a ≠ 0
h : (↑a * b).re = (↑a * c).re ∧ (↑a * b).im = (↑a * c).im
⊢ a * b.im = a * c.im → b.im = c.im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
i : α
⊢ IsPoly fun v ↦ (proj i) (v ∘ f)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
i : α
⊢ IsPoly fun v ↦ ↑(v (f i))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
n : ℤ
⊢ IsPoly fun v ↦ (const n) (v ∘ f)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f : α → β
g : Poly α
n : ℤ
⊢ IsPoly fun v ↦ n
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f✝ : α → β
g✝ f g : Poly α
pf : IsPoly fun v ↦ f (v ∘ f✝)
pg : IsPoly fun v ↦ g (v ∘ f✝)
⊢ IsPoly fun v ↦ (f - g) (v ∘ f✝)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f✝ : α → β
g✝ f g : Poly α
pf : IsPoly fun v ↦ f (v ∘ f✝)
pg : IsPoly fun v ↦ g (v ∘ f✝)
⊢ IsPoly fun v ↦ f (v ∘ f✝) - g (v ∘ f✝)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f✝ : α → β
g✝ f g : Poly α
pf : IsPoly fun v ↦ f (v ∘ f✝)
pg : IsPoly fun v ↦ g (v ∘ f✝)
⊢ IsPoly fun v ↦ (f * g) (v ∘ f✝)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.9
β : Type ?u.11
f✝ : α → β
g✝ f g : Poly α
pf : IsPoly fun v ↦ f (v ∘ f✝)
pg : IsPoly fun v ↦ g (v ∘ f✝)
⊢ IsPoly fun v ↦ f (v ∘ f✝) * g (v ∘ f✝)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (x * z) * (c * (x * z)) ≤ d * (y * w) * (d * (y * w))

Tactic:
simpa using

Goal state after:
c d x y z w : ℕ
xy : SqLe x c y d
zw : SqLe z c w d
⊢ c * (c * (x * (x * (z * z)))) ≤ d * (d * (y * (y * (w * w))))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d

Tactic:
simpa using

Goal state after:
c d x y n : ℕ
xy : SqLe x c y d
⊢ c * (x * (n * (n * x))) ≤ d * (y * (n * (n * y)))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
n : ℤ√d
⊢ ↑n.norm = n * star n

Tactic:
by
  ext <;> simp [norm, star, mul_comm, sub_eq_add_neg]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y z w : ℕ
xy✝ : { re := ↑x, im := -↑y }.Nonneg
zw✝ : { re := -↑z, im := ↑w }.Nonneg
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
⊢ (k + j + 1) * (k + j + 1) ≤ k * k

Tactic:
simpa using

Goal state after:
d x y z w : ℕ
xy✝ : { re := ↑x, im := -↑y }.Nonneg
zw✝ : { re := -↑z, im := ↑w }.Nonneg
j k m n : ℕ
xy : SqLe (n + m + 1) d k 1
zw : SqLe (k + j + 1) 1 n d
t : 1 * (k + j + 1) * (k + j + 1) ≤ 1 * k * k := Nat.le_trans zw (sqLe_of_le (Nat.le_add_right n (m + 1)) le_rfl xy)
⊢ (k + j + 1) * (k + j + 1) ≤ k * k