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

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

Tactic:
Nat.range_eq_Icc_zero_sub_one _ n.add_one_ne_zero,

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

Goal state before:
pp: n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n) / ↑3 ≤ 2 * ↑n / 3

Tactic:
by norm_cast

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (h.card ε ^ 0).succ → Fin 0 → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin 0), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε

Tactic:
refine ⟨0, 1, ?_, ?_⟩

Goal state after:
case zero.refine_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (h.card ε ^ 0).succ → Fin 0 → R
⊢ 0 ≠ 1

case zero.refine_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (h.card ε ^ 0).succ → Fin 0 → R
⊢ ∀ (k : Fin 0), ↑(abv (A 1 k % b - A 0 k % b)) < abv b • ε
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p l : ℕ
inst✝ : Fact (Nat.Prime p)
hbij : ∑ v ∈ Ico 1 p, ↑v ^ l = ∑ u, ↑u ^ l
⊢ (∑ u, ↑u ^ l + if p - 1 ∣ l then 1 else 0) = 0

Tactic:
FiniteField.sum_pow_units,

Goal state after:
p l : ℕ
inst✝ : Fact (Nat.Prime p)
hbij : ∑ v ∈ Ico 1 p, ↑v ^ l = ∑ u, ↑u ^ l
⊢ ((if Fintype.card (ZMod p) - 1 ∣ l then -1 else 0) + if p - 1 ∣ l then 1 else 0) = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ 2 * ↑k + 1 ≠ 0

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
⊢ p ∈ n.primesLE

Tactic:
have := prime_of_mem_primeFactors h

Goal state after:
case refine_1
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
this : Prime p
⊢ p ∈ n.primesLE
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∏ x ∈ n.primesLE, x ^ ⌊logb ↑x ↑n⌋₊ = ∏ p ∈ n.primesLE, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

Tactic:
← log_div_log

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
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:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
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

case mpr
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
⊢ (∃ i j, i ≠ j ∧ (distinctElems bS adm) i - (distinctElems bS adm) j = x) →
    x ≠ 0 ∧ ∃ a ∈ Finset.univ, (distinctElems bS adm) a.1 - (distinctElems bS adm) a.2 = x
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}
⊢ log ↑(x✝¹ ^ x✝²).minFac = log ↑x✝¹

Tactic:
rw [Prime.pow_minFac _ (by linarith [mem_Icc.mp hk])]

Goal state after:
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}
⊢ Nat.Prime x✝¹
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
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

Tactic:
hT

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 ∣ (↑T - ∑ i ∈ range (2 * k), bernoulli i * ↑((2 * k + 1).choose i) * ↑p ^ (2 * k - i) / (2 * ↑k + 1)).den
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
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FunctionField F K ↔ FiniteDimensional Ft K

Tactic:
constructor

Goal state after:
case mp
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 := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FunctionField F K → FiniteDimensional Ft K

case mpr
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 := ⋯
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
⊢ FiniteDimensional Ft K → FunctionField F K
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
suffices rdcp : r.den.Coprime p by
    rw [rdcp.gcd_eq_one]
    simp only [mul_one, cast_one, sub_self]

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
this : ↑(r.den.gcd p) = ↑r.den * ↑(r.den.gcdA p)
⊢ r.den.Coprime p
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
⊢ p ∣ p ^ 1

Tactic:
rw [pow_one]

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

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

Tactic:
constructor

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

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, H⟩ - ↑↑n‖ < 1
⊢ ‖x - ↑n‖ < 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr
x : ℝ
hx : 0 ≤ x
⊢ ψ x - θ x ≤ ψ (x ^ 2⁻¹) + ψ (x ^ 3⁻¹) + ψ (x ^ 5⁻¹)

Tactic:
exact (psi_sub_theta_bounds hx).1

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

Goal state before:
pp: case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 ↔ ‖x‖ = 1

Tactic:
constructor

Goal state after:
case inr.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖↑x.zmodRepr‖ = 1 → ‖x‖ = 1

case inr.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
H : ‖↑x.zmodRepr‖ ≠ ‖x‖
this : ‖x - ↑x.zmodRepr‖ < 1
⊢ ‖x‖ = 1 → ‖↑x.zmodRepr‖ = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
| fun t ↦ θ t / (t * log t ^ 2)

Tactic:
ext

Goal state after:
x x✝ : ℝ
| θ x✝ / (x✝ * log x✝ ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

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

pp: case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0

Tactic:
· simp_all [eq_comm]

Goal state after:
case inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : x.zmodRepr = 0
⊢ ‖↑x.zmodRepr‖ = ‖x‖ ↔ ‖x‖ = 1 ∨ x = 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ θ x = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
theta_eq_sum_Icc,

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
constructor

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

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x ∈ maximalIdeal ℤ_[p] → toZMod x = 0
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, ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε

Tactic:
by_contra! hg
    obtain ⟨j₀, j₁, j_ne, approx⟩ := exists_approx_polynomial hb hε
      (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
    revert j_ne approx
    refine Fin.cases ?_ (fun j₀ => ?_) j₀ <;>
      refine Fin.cases (fun j_ne approx => ?_) (fun j₁ j_ne approx => ?_) j₁
    · exact absurd rfl j_ne
    · rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
      have := (Classical.choose_spec (hg j₁)).2
      contradiction
    · rw [Fin.cons_succ, Fin.cons_zero, ← not_le] at approx
      have := (Classical.choose_spec (hg j₀)).2
      contradiction
    · rw [Fin.cons_succ, Fin.cons_succ] at approx
      rw [Ne, Fin.succ_inj] at j_ne
      have : j₀ = j₁ := (Classical.choose_spec (hg j₀)).1.symm.trans
        (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
          (Classical.choose_spec (hg j₁)).1)
      contradiction

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)
⊢ ⋯.unit = ⋯.unit ^ p ^ i

Tactic:
ext

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)
⊢ ↑⋯.unit = ↑(⋯.unit ^ p ^ i)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: | fun x ↦ log x ^ 2 * √x

Tactic:
ext

Goal state after:
x✝ : ℝ
| log x✝ ^ 2 * √x✝
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 = traceMatrix A (⇑f ∘ b)

Tactic:
ext

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
i✝ j✝ : ι
⊢ traceMatrix A b i✝ j✝ = traceMatrix A (⇑f ∘ b) i✝ j✝
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: | fun x ↦ √x / log 2 ^ 2

Tactic:
ext

Goal state after:
x✝ : ℝ
| √x✝ / log 2 ^ 2
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:
constructor

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

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ Ideal.span {↑p ^ n} → (toZModPow n) x = 0
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 = (modularCyclotomicCharacter L ⋯) g.toRingEquiv

Tactic:
ext

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
⊢ ↑((autToPow R hμ) g) = ↑((modularCyclotomicCharacter L ⋯) g.toRingEquiv)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ ‖x - ↑(x.appr n)‖ ≤ ↑p ^ (-↑n)

Tactic:
rw [norm_le_pow_iff_mem_span_pow]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
⊢ ⇑f ∘ ⇑(integralBasis K) = ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))

Tactic:
ext

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := ↑(AlgEquiv.restrictScalars ℤ f).mapIntegralClosure
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (⇑f ∘ ⇑(integralBasis K)) x✝ =
    (Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀)) x✝
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) ↔ x = y

Tactic:
constructor

Goal state after:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) → x = y

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
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:
constructor

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

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ g = g' → ∀ (n : ℕ), (toZModPow n).comp g = (toZModPow n).comp g'
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ ↑(d a1) = az a * az a - 1

Tactic:
by rw [Pell.d, Int.ofNat_sub this]; rfl

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

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

Tactic:
ext

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

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).im = (pellZd a1 n * { re := ↑a, im := 1 }).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)

Tactic:
ext

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

case refine_1.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d : ℤ
a✝ : ℤ√d
⊢ 0 + a✝ = a✝

Tactic:
ext

Goal state after:
case refine_2.re
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).re = a✝.re

case refine_2.im
d : ℤ
a✝ : ℤ√d
⊢ (0 + a✝).im = a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_3
d : ℤ
a✝ : ℤ√d
⊢ a✝ + 0 = a✝

Tactic:
ext

Goal state after:
case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ + 0).im = a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_4
d : ℤ
a✝ : ℤ√d
⊢ -a✝ + a✝ = 0

Tactic:
ext

Goal state after:
case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).re = re 0

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (-a✝ + a✝).im = im 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_5
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
ext

Goal state after:
case refine_5.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_5.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
ext

Goal state after:
case refine_1.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case refine_1.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ + b✝).im = (b✝ + a✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

Tactic:
ext

Goal state after:
case refine_2.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

case refine_2.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_3
d : ℤ
a✝ : ℤ√d
⊢ 1 * a✝ = a✝

Tactic:
ext

Goal state after:
case refine_3.re
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).re = a✝.re

case refine_3.im
d : ℤ
a✝ : ℤ√d
⊢ (1 * a✝).im = a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_4
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 1 = a✝

Tactic:
ext

Goal state after:
case refine_4.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).re = a✝.re

case refine_4.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 1).im = a✝.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_5
d : ℤ
a✝ : ℤ√d
⊢ 0 * a✝ = 0

Tactic:
ext

Goal state after:
case refine_5.re
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).re = re 0

case refine_5.im
d : ℤ
a✝ : ℤ√d
⊢ (0 * a✝).im = im 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_6
d : ℤ
a✝ : ℤ√d
⊢ a✝ * 0 = 0

Tactic:
ext

Goal state after:
case refine_6.re
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).re = re 0

case refine_6.im
d : ℤ
a✝ : ℤ√d
⊢ (a✝ * 0).im = im 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_7
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

Tactic:
ext

Goal state after:
case refine_7.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

case refine_7.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_8
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

Tactic:
ext

Goal state after:
case refine_8.re
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

case refine_8.im
d : ℤ
a✝ b✝ c✝ : ℤ√d
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_9
d : ℤ
a✝ b✝ : ℤ√d
⊢ a✝ * b✝ = b✝ * a✝

Tactic:
ext

Goal state after:
case refine_9.re
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).re = (b✝ * a✝).re

case refine_9.im
d : ℤ
a✝ b✝ : ℤ√d
⊢ (a✝ * b✝).im = (b✝ * a✝).im
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ + x✝² + x✝¹) x✝ = (x✝³ + (x✝² + x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 0 + x✝ = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 + x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ + 0 = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ + 0) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ -x✝ + x✝ = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (-x✝¹ + x✝¹) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² + x✝¹) x✝ = (x✝¹ + x✝²) x✝
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * x✝² * x✝¹) x✝ = (x✝³ * (x✝² * x✝¹)) x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 1 * x✝ = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (1 * x✝¹) x✝ = x✝¹ x✝
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ * 1 = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 1) x✝ = x✝¹ x✝