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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ x✝² ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 0 < log 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
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 < ε
⊢ ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: 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
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x

Tactic:
simp only [sum_const, card_Icc, reduceSubDiff, nsmul_eq_mul]

Goal state after:
x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑(⌊log x / log 2⌋₊ - 1) * (log 4 * √x) ≤ 2 * √x * log x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 0 ≤ log x / log 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ ↑(⌊log x / log 2⌋₊ - 1) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log x / log 2 * (log 4 * √x) = log 4 / log 2 * √x * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ 4 = 2 ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log 4 / log 2 * √x * log x = 2 * √x * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x = ψ x - θ x + θ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
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
⊢ ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ 2 * √x * log x + log 4 * x = log 4 * x + 2 * √x * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x ≤ log 4 * x + 2 * √x * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : x < 1
⊢ x < 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < 1 / 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
⊢ ψ x - θ x = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, Λ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n.lcmUpto ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ 0 < 2 ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n * log 2 - log (↑n + 1) ≤ ψ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ 2 * √x * log x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ↑n * log 2 - log (↑n + 1) - 2 * √↑n * log ↑n ≤ θ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ (↑m)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n m : ℕ
hnm : n ≤ m
hn : 1 ≤ n
hm : 1 ≤ m
h : x ≤ 1
⊢ 0 ≤ (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ AntitoneOn (b x) (Set.Ici 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
⊢ 0 ≤ x ^ (↑n)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
this : 0 ≤ x ^ (↑n)⁻¹
N : ℕ
hN : N ≥ ⌊log (x ^ (↑n)⁻¹) / log 2⌋₊
⊢ 0 ≤ ?m.82

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
n : ℕ
hx : 0 ≤ x
⊢ ∃ M, ∀ N ≥ M, ψ (x ^ (↑n)⁻¹) = ∑ k ∈ Icc 1 N, b x (n * k)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ∃ T,
    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)

Tactic:
by

Goal state after:
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
⊢ ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i

Tactic:
by

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

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / ↑p).den

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, 1 / ↑q).den

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ ↑1 = bernoulli (2 * 0) + ∑ p ∈ range (2 * 0 + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * 0, 1 / ↑p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k : ℕ
⊢ bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p ∈ Set.range Int.cast

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
hx : Transcendental R x
p : R[X][Y]
⊢ (algEquivAdjoin hx) (swap p) = (aeval (C ⟨x, ⋯⟩)) p

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p : R[X][Y]
⊢ (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) p) = (aeval y) ((Transcendental.algEquivAdjoin hx) p)

Tactic:
by

Goal state after:
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 • ε
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
⊢ r • a - b • q = ∑ x, (rs k x • bS x - rs j x • bS x)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
f : (↥R[x])[X]
hnezero : f ≠ 0
halg : (aeval y) f = 0
⊢ (Transcendental.algEquivAdjoin hy) (swap ((Transcendental.algEquivAdjoin hx).symm f)) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
hy : Transcendental R y
h : IsAlgebraic (↥R[x]) y
⊢ IsAlgebraic (↥R[y]) ((algebraMap A B) x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
N : ℕ
⊢ ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ : ℕ
h1 : ∀ N ≥ N₁, ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 N, b x (1 * k)
N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
⊢ 1 + 6 * N ≥ N₁

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ : ℕ
h2 : ∀ N ≥ N₂, ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 N, b x (2 * k)
N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ 3 * N ≥ N₂

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ : ℕ
h3 : ∀ N ≥ N₃, ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 N, b x (3 * k)
N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ 2 * N ≥ N₃

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
⊢ FunctionField F K ↔ FiniteDimensional Ft K

Tactic:
by

Goal state after:
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
⊢ Function.Injective ⇑(algebraMap F[X] K)

Tactic:
by

Goal state after:
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
hinj : Function.Injective ⇑(algebraMap F[X] K)
p : F[X]
hp : ↑((algebraMap F[X] ↥(ringOfIntegers F K)) p) = 0
⊢ p = 0

Tactic:
injective_iff_map_eq_zero (algebraMap F[X] K)

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
hinj : ∀ (a : F[X]), (algebraMap F[X] K) a = 0 → a = 0
p : F[X]
hp : ↑((algebraMap F[X] ↥(ringOfIntegers F K)) p) = 0
⊢ p = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ : ℕ
h5 : ∀ N ≥ N₅, ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ N ≥ N₅

Tactic:
by

Goal state after:
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
⊢ Function.Injective ⇑(algebraMap F[X] ↥(ringOfIntegers F K))

Tactic:
by

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

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

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
h7 : ∀ N ≥ N₇, ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
⊢ N ≥ N₇

Tactic:
by

Goal state after:
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
y : K
hy : Transcendental F y
x : K := (algebraMap F⟮X⟯ K) X
Fyx : IntermediateField F K := restrictScalars F (↥F⟮y⟯)⟮x⟯
Fxy : IntermediateField F K := restrictScalars F (↥F⟮x⟯)⟮y⟯
this✝⁵ : Algebra ↥F⟮y⟯ ↥Fyx := (↥F⟮y⟯)⟮x⟯.algebra
this✝⁴ : Module ↥F⟮y⟯ ↥Fyx := Algebra.toModule
this✝³ : SMul ↥F⟮y⟯ ↥Fyx := this✝⁵.toSMul
this✝² : Algebra ↥F⟮x⟯ ↥Fxy := (↥F⟮x⟯)⟮y⟯.algebra
this✝¹ : Module ↥F⟮x⟯ ↥Fxy := Algebra.toModule
this✝ : SMul ↥F⟮x⟯ ↥Fxy := this✝².toSMul
this : FiniteDimensional ↥F⟮y⟯ ↥Fyx
⊢ FiniteDimensional (↥Fyx) K

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
⊢ modPart p r < ↑p

Tactic:
by

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)
rdcp : r.den.Coprime p
⊢ ↑r.num - ↑r.num * ↑(r.den.gcd p) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n ∈ Set.Ici 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n + 1 ∈ Set.Ici 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 6 * n ≤ 6 * n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N₁ N₂ N₃ N₅ N₇ : ℕ
N : ℕ := N₁ + N₂ + N₃ + N₅ + N₇
h7 : ψ (x ^ (↑7)⁻¹) = ∑ k ∈ Icc 1 N, b x (7 * k)
h5 : ψ (x ^ (↑5)⁻¹) = ∑ k ∈ Icc 1 N, b x (5 * k)
h3 : ψ (x ^ (↑3)⁻¹) = ∑ k ∈ Icc 1 (2 * N), b x (3 * k)
h2 : ψ (x ^ (↑2)⁻¹) = ∑ k ∈ Icc 1 (3 * N), b x (2 * k)
h1 : ψ (x ^ (↑1)⁻¹) = ∑ k ∈ Icc 1 (1 + 6 * N), b x (1 * k)
n : ℕ
hn : n ∈ Icc 1 N
⊢ 5 * n ∈ Set.Ici 1

Tactic:
by

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

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

Tactic:
by

Goal state after: