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

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val +
      (x.appr (m + k) - x.appr m)

Tactic:
]

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - (↑m + ↑k)).natAbs)).val +
      (x.appr (m + k) - x.appr m)
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]
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 • ε
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 : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(cardPowDegree (A 0 % b - A i'.succ % b)) < cardPowDegree b • ε
⊢ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε

Tactic:
]

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]
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 • ε
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 : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(cardPowDegree (A 0 % b - A i'.succ % b)) < cardPowDegree b • ε
⊢ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (∫ (x : ℝ) in 2..√x, 1 / log x ^ 2) + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

pp: case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume 2 √x

pp: case hbc
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume (√x) x

Tactic:
]

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (∫ (x : ℝ) in 2..√x, 1 / log x ^ 2) + ∫ (x : ℝ) in √x..x, 1 / log x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

case hab
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume 2 √x

case hbc
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ IntervalIntegrable (fun t ↦ 1 / log t ^ 2) volume (√x) x
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case pos
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) ∣ 0

Tactic:
]

Goal state after:
case pos
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) ∣ 0
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:
]

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

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / log √x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
]

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / log √x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 2 ^ 2 * ((x - √x) / log x ^ 2) + (√x - 2) / log 2 ^ 2 ≤ 4 * (x / log x ^ 2) + √x / log 2 ^ 2

Tactic:
]

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ 2 ^ 2 * ((x - √x) / log x ^ 2) + (√x - 2) / log 2 ^ 2 ≤ 4 * (x / log x ^ 2) + √x / log 2 ^ 2
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
hc' : c ≠ 0
⊢ (↑p ^ n * c).valuation = (↑p ^ n * c).valuation

Tactic:
]

Goal state after:
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
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(↑p ^ n * c).valuation - ↑n).natAbs).cast

Tactic:
]

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
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ (↑(↑p ^ n * c).valuation - ↑n).natAbs).cast
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
i k : ℕ
hi : k ≤ i
⊢ ↑p ^ k ∣ aux g (p ^ i) - aux g (p ^ k)

Tactic:
obtain ⟨i, rfl⟩ := exists_add_of_le hi

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
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
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast)

Tactic:
]

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
c : ℤ_[p]
hc : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr A (⇑f ∘ b)

Tactic:
]

Goal state after:
A : Type u
B : Type v
C : Type z
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
⊢ (traceMatrix A b).det = discr A (⇑f ∘ b)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
ι' : Type u_1
inst✝² : Fintype ι'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ discr A ⇑b = discr A ⇑b

Tactic:
]

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (⋯.unit ^ p ^ i) ^ aux g (p ^ k) = 1
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
]

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : (⋯.unit ^ aux g (p ^ (k + i))) ^ p ^ i / (⋯.unit ^ p ^ i) ^ aux g (p ^ k) = 1
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inl
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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h)).cast

Tactic:
]

Goal state after:
case neg.inl
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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h)).cast
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False

Tactic:
]

Goal state after:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖

pp: x : ℝ
hx : 4 ≤ x
⊢ Set.EqOn (fun x ↦ |1 / log x ^ 2|) (fun t ↦ 1 / log t ^ 2) (Set.uIcc 2 x)

Tactic:
]

Goal state after:
x : ℝ
hx : 4 ≤ x
⊢ ∫ (x : ℝ) in 2..x, 1 / log x ^ 2 ≤ ‖4 * x / log x ^ 2 + √x / log 2 ^ 2‖

x : ℝ
hx : 4 ≤ x
⊢ Set.EqOn (fun x ↦ |1 / log x ^ 2|) (fun t ↦ 1 / log t ^ 2) (Set.uIcc 2 x)
Module: Mathlib.NumberTheory.Chebyshev

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

pp: x : ℝ
hx : 4 ≤ x
⊢ 0 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
]

Goal state after:
x : ℝ
hx : 4 ≤ x
⊢ 0 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ maximalIdeal ℤ_[p]

Tactic:
]

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
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = c * ↑p ^ n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = ↑(unitCoeff h)
⊢ c - (toZMod c).cast ∈ maximalIdeal ℤ_[p]
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
]

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑(p ^ (k + i)) ∣ ↑(p ^ i) * (aux g (p ^ (k + i)) - aux g (p ^ k))
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: A : Type u
B : Type v
ι : Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Fintype ι
b : ι → B
P : Matrix ι ι A
⊢ P.det * P.det * (traceMatrix A b).det = P.det * P.det * (traceMatrix A b).det

Tactic:
]

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

Goal state before:
pp: case neg.inl
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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : (↑c).valuation = 0
⊢ ↑c = ↑c

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 : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : (↑c).valuation = 0
⊢ Irreducible ↑p

Tactic:
]

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
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ (x - ↑(x.appr n)).valuation = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : (↑c).valuation = 0
⊢ Irreducible ↑p
Module: Mathlib.NumberTheory.Chebyshev

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

pp: x : ℝ
a✝ : 4 ≤ x
⊢ 0 ≤ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2

Tactic:
]

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ 0 ≤ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.inr
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
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ c.valuation

Tactic:
]

Goal state after:
case neg.inr
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
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ c.valuation
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ IntegrableOn (fun x ↦ θ x / (x * log x ^ 2)) (Set.Icc 2 x) volume

Tactic:
]

Goal state after:
x : ℝ
a✝ : 4 ≤ x
⊢ IntegrableOn (fun x ↦ θ x / (x * log x ^ 2)) (Set.Icc 2 x) volume
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
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ (traceForm K L).Nondegenerate

Tactic:
]

Goal state after:
ι : 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
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ (traceForm K L).Nondegenerate
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
t : ℝ
x✝ : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right✝ : t ≤ x
⊢ log 4 * t / (t * log t ^ 2) ≤ log 4 * t / (t * log t ^ 2)

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
]

Goal state after:
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
g : L ≃+* L
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ : g ζ = ↑(⋯.unit ^ aux g (p ^ (k + i)))
H₂ : ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ ↑p ^ k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) = (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) - θ x / log x

Tactic:
]

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) = (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)) - θ x / log x
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))

Tactic:
]

Goal state after:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
g : L ≃+* L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
⊢ ↑↑(t ^ aux g n) = ↑(↑t ^ (aux g n % ↑(Nat.card ↥(rootsOfUnity n L))))
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ (embeddingsMatrixReindex K E b ?e).det * (embeddingsMatrixReindex K E b ?e).det =
    (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det

pp: case e
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
b : ι → L
inst✝ : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
⊢ ι ≃ (L →ₐ[K] E)

Tactic:
]

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

Goal state before:
pp: case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ x.appr n
⊢ x.appr n = 0

Tactic:
]

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ x.appr n
⊢ x.appr n = 0
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}
⊢ (toZModPow n) x = 0

Tactic:
]

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

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

Goal state before:
pp: L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Nat.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ↑(↑ζ ^ c.val) = ↑(↑ζ ^ c.val)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ ∏ x, (∏ j > x, ((e j) pb.gen - (e x) pb.gen)) ^ 2 = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
]

Goal state after:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ ∏ x, (∏ j > x, ((e j) pb.gen - (e x) pb.gen)) ^ 2 = ∏ i, ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0

Tactic:
]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0
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‖
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x

Tactic:
]

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‖
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2) ≤ log 4 * x / log x + ε * x / log x
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: case e_f
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
i : Fin pb.dim
⊢ ∏ x > i, ((e x) pb.gen - (e i) pb.gen) ^ 2 = ∏ j > i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
]

Goal state after: