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

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))
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:
rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]

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

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2 * √x) =o[atTop] fun x ↦ x

pp: ⊢ ∀ᶠ (x : ℝ) in atTop, log x ^ 2 ≠ 0

Tactic:
·

Goal state after:
⊢ (fun x ↦ log x ^ 2 * √x) =o[atTop] fun x ↦ x
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ log x ^ 2) =o[atTop] fun x ↦ x / √x

pp: ⊢ ∀ᶠ (x : ℝ) in atTop, √x ≠ 0

Tactic:
·

Goal state after:
⊢ (fun x ↦ log x ^ 2) =o[atTop] fun x ↦ x / √x
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 : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast

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 ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).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 : x - ↑(x.appr n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ ↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: ⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2) =O[atTop] fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2

pp: ⊢ (fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
·

Goal state after:
⊢ (fun x ↦ ∫ (t : ℝ) in 2..x, 1 / log t ^ 2) =O[atTop] fun x ↦ 4 * x / log x ^ 2 + √x / log 2 ^ 2
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‖
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

pp: case refine_2
⊢ (fun x ↦ √x / log 2 ^ 2) =O[atTop] fun x ↦ x / log x ^ 2

Tactic:
·

Goal state after:
case refine_1
⊢ (fun x ↦ 4 * x / log x ^ 2) =O[atTop] fun x ↦ x / log x ^ 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 ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast

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 ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ (↑c.valuation).natAbs).cast
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}

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

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

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
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: case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 < Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

pp: case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
·

Goal state after:
case inl
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 < Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)

Tactic:
·

Goal state after:
case inr
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
t : ↥(rootsOfUnity n L)
this : 1 ≤ Nat.card ↥(rootsOfUnity n L)
h : 1 = Nat.card ↥(rootsOfUnity n L)
⊢ (RingEquiv.refl L) ↑↑t = ↑(↑t ^ ZMod.val 1)
Module: Mathlib.NumberTheory.Padics.RingHoms

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

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

Tactic:
·

Goal state after:
case ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(x.appr n) - ↑(x.appr n) ∈ Ideal.span {↑p ^ m}
Module: Mathlib.NumberTheory.Padics.RingHoms

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

Tactic:
·

Goal state after:
case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑(x.appr n) - ↑(x.appr m) ∈ Ideal.span {↑p ^ m}
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inl
⊢ (↑0 * log 2 - log (↑0 + 1)) / log ↑0 ≤ ↑(π 0)

pp: case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

pp: case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
·

Goal state after:
case inl
⊢ (↑0 * log 2 - log (↑0 + 1)) / log ↑0 ≤ ↑(π 0)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)

pp: case inr.inr
n : ℕ
h : 1 < n
⊢ (↑n * log 2 - log (↑n + 1)) / log ↑n ≤ ↑(π n)

Tactic:
·

Goal state after:
case inr.inl
⊢ (↑1 * log 2 - log (↑1 + 1)) / log ↑1 ≤ ↑(π 1)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}

pp: case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
·

Goal state after:
case refine_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed {b | b ∈ closure (Set.range Int.cast)}
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)

Tactic:
·

Goal state after:
case refine_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ∀ (a : ℕ), ↑a ∈ closure (Set.range Int.cast)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1

pp: case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1

Tactic:
·

Goal state after:
case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1

Tactic:
·

Goal state after:
case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p 1 = 1
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case pos
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ↑p ≤ √x
⊢ log √x ≤ log ↑p + log √x

pp: case neg
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ¬↑p ≤ √x
⊢ log √x ≤ log ↑p + 0

Tactic:
·

Goal state after:
case pos
x : ℝ
hx : 1 ≤ x
p : ℕ
x✝ : p ∈ ⌊x⌋₊.primesLE
h : ↑p ≤ √x
⊢ log √x ≤ log ↑p + log √x
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

pp: case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
·

Goal state after:
case pos
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g

Tactic:
·

Goal state after:
case neg
L : Type u
inst✝³ : CommRing L
inst✝² : IsDomain L
n : ℕ
inst✝¹ : NeZero n
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : L ≃+* L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ cyclotomicCharacter.toFun p (f * g) = cyclotomicCharacter.toFun p f * cyclotomicCharacter.toFun p g
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case neg
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

pp: case pos
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))

Tactic:
·

Goal state after:
case neg
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬∀ (i : ℕ), ∃ ζ, IsPrimitiveRoot ζ (p ^ i)
⊢ Continuous ⇑((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x

pp: case hbc
x : ℝ
hx : 1 ≤ x
⊢ ↑(#({a ∈ ⌊x⌋₊.primesLE | ↑a ≤ √x})) ≤ √x

Tactic:
·

Goal state after:
case ha
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm R) a)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_1
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ IsIntegral K (ζ k)

pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ ∀ x ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup),
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
      Metric.ball 1 ε

Tactic:
·

Goal state after:
case pos.refine_1
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ IsIntegral K (ζ k)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ ∀ x ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup),
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
      Metric.ball 1 ε

Tactic:
·

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
⊢ ∀ x ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup),
    ((Units.coeHom ℤ_[p]).comp ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L))) x ∈
      Metric.ball 1 ε
Module: Mathlib.RingTheory.Localization.NormTrace

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

pp: case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ j ≠ 0

Tactic:
by lia

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

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i)

pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1

Tactic:
·

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ ((MulSemiringAction.toRingAut Gal(L/K) L) σ) ↑(⋯.unit ^ i) = ↑(⋯.unit ^ i)
Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter

Goal state before:
pp: case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1

Tactic:
·

Goal state after:
case pos.refine_2
p : ℕ
inst✝³ : Fact (Nat.Prime p)
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
ζ : ℕ → L
hζ : ∀ (i : ℕ), IsPrimitiveRoot (ζ i) (p ^ i)
ε : ℝ
hε : 0 < ε
k : ℕ
hk' : k ≠ 0
hk : ↑p ^ (-↑k) < ε
σ : Gal(L/K)
hσ : σ ∈ id ((fun g ↦ g.carrier) K⟮ζ k⟯.fixingSubgroup)
i : ℕ
hi : i < p ^ k
ht : ⋯.unit ^ i ∈ rootsOfUnity (p ^ k) L
⊢ p ^ k ≠ 1