mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ∣ x + 1
⊢ λ ∣ x + 1 - (↑η - 1 + 3)

Tactic:
exact dvd_sub h <| dvd_add dvd_rfl hζ.toInteger_sub_one_dvd_prime'

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Deficient 0

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 1

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 2

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Deficient 3

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Abundant 0

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ Abundant 12

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: ⊢ ¬Weird 0

Tactic:
by
  decide

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
h : Prime n
h✝ : m > 0
⊢ ∑ x ∈ map { toFun := fun x ↦ n ^ x, inj' := ⋯ } (range m), x = ∑ i ∈ range m, n ^ i

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FactorisationProperties

Goal state before:
pp: n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ m.abundancyIndex ≤ n.abundancyIndex

Tactic:
rw [abundancyIndex, abundancyIndex, hk, cast_mul, div_mul_eq_div_div_swap]

Goal state after:
n m : ℕ
hn : n ≠ 0
k : ℕ
hk : n = m * k
hk0 : k ≠ 0
⊢ ↑(∑ i ∈ m.divisors, i) / ↑m ≤ ↑(∑ i ∈ (m * k).divisors, i) / ↑k / ↑m
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
P Q : Ideal B
hP : P * Q = Ideal.map (algebraMap A B) p
x✝ : B
hxQ : x✝ ∈ Q
hx✝ : (intTrace A B) x✝ ∉ p
hp : ¬p = ⊥
this✝¹ : Algebra (A ⧸ p) (B ⧸ Q) := Ideal.Quotient.algebraQuotientOfLEComap ⋯
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
this : FiniteDimensional K L
H : ↑Q ≤ FractionalIdeal.dual A K 1 * ↑(Ideal.map (algebraMap A B) p)
hne : 1 ≠ 0
y✝ : B
x : L
hx : x ∈ FractionalIdeal.dual A K 1
y : A
hy : y ∈ ↑p
⊢ 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ -2 = -1 * 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic

Goal state before:
pp: case inl
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
h : (quadraticChar F) (-1) = if (-1) ^ (Fintype.card F / 2) = 1 then 1 else -1
n : ℕ
h₂ : Even n
⊢ (if (-1) ^ n = 1 then 1 else -1) = (-1) ^ n

Tactic:
simp only [Even.neg_one_pow h₂, if_true]

Goal state after:
Module: Mathlib.NumberTheory.LucasPrimality

Goal state before:
pp: p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ a * ?m.122 = 1

Tactic:
← pow_succ',

Goal state after:
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ a ^ (?n + 1) = 1

case n
p : ℕ
a : ZMod p
ha : a ^ (p - 1) = 1
hd : ∀ (q : ℕ), Nat.Prime q → q ∣ p - 1 → a ^ ((p - 1) / q) ≠ 1
h : p ≠ 0 ∧ p ≠ 1
hp1 : 1 < p
this : NeZero p
⊢ ℕ
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ (-1) ^ 2 = 1

Tactic:
neg_one_sq

Goal state after:
case ha
n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
this : Fact (2 < 2 ^ 2 ^ n + 1)
key : 2 ^ n = 2 ^ n - 1 + 1
⊢ 1 = 1
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ (-1) ^ 2 = 1

Tactic:
neg_one_sq

Goal state after:
case hfin
a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : ↑a ^ 2 ^ n = -1
ha0 : ↑a ≠ 0
⊢ 1 = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: a b : ℕ
ha : 2 ≤ a
hb : 2 < b
⊢ b = ∑ x ∈ Finset.range b, 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = S'.c ^ 3

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ b ^ (2 * p) - (1 + (b ^ 2 - 1)) = b ^ (2 * p) - (1 + b ^ 2 - 1)

Tactic:
rw [Nat.add_sub_assoc hi_bsquared]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ ↑S'.u⁻¹ * (↑S'.u * S'.c ^ 3) = S'.c ^ 3

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: n : ℕ
⊢ n ∈ maximalIdeal ℕ ↔ n ≠ 1

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 2 ∈ ↑(maximalIdeal ℕ)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 3 ∈ ↑(maximalIdeal ℕ)

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: n : ℕ
h : n ∈ maximalIdeal ℕ
lt : 1 < n
⊢ gcd 2 3 ∣ n

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ {2} ⊆ {2, 3}

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ 3 ∈ {2, 3}

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: ⊢ ¬2 ∣ 3

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : Set ℕ
h0 : setGcd s = 0
⊢ ↑∅ ⊆ s

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl.refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η * S'.b
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = S'.b * (↑η * ↑η ^ 2)

Tactic:
← pow_succ',

Goal state after:
case inr.inl.refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η * S'.b
x✝ : λ ∣ ↑η * S'.b
x : 𝓞 K
hx : ↑η * S'.b = λ * x
⊢ S'.b = S'.b * ↑η ^ (2 + 1)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
le : n ≤ m
⊢ ↑t ⊆ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: s : AddSubmonoid ℕ
⊢ (AddSubmonoid.toNatSubmodule s).FG

Tactic:
apply IsNoetherian.noetherian

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
⊢ 0 < ↑1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b : ℕ
h : 1 ≤ b
m : ℕ
b_ge_two : 2 ≤ b
p : ℕ
hp₁ : b * (b ^ 2 - 1) + 1 + m ≤ p
hp₂ : Prime p
h₁ : 0 < b
h₂ : 4 ≤ b ^ 2
⊢ 1 < 4

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ 1 < ↑2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ -(↑η ^ 2 - 1)
⊢ λ = 1 * ↑η - (-↑⋯.unit * ↑η - 1 * ↑η)

Tactic:
neg_mul,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηsqb : p ∣ 1 * S.a + ↑η ^ 2 * S.b
this : p ∣ -(↑η ^ 2 - 1)
⊢ λ = 1 * ↑η - (-(↑⋯.unit * ↑η) - 1 * ↑η)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ * λ ^ (3 * S.multiplicity - 2) * λ * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
⊢ False

Tactic:
← pow_succ',

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ (3 * S.multiplicity - 2 + 1) * λ * λ ∣ (λ ^ S.multiplicity * S.w) ^ 3
⊢ False
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = ↑(-η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

Tactic:
neg_mul,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = ↑(-(η ^ 2 * S.u₁) * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = ↑(-(η ^ 2 * S.u₁) * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

Tactic:
neg_mul,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = ↑(-(η ^ 2 * S.u₁ * S.u₂⁻¹)) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = -↑(η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3

Tactic:
neg_mul,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = -(↑(η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
⊢ ↑n ≤ ↑n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case insert.refine_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : AddCommMonoid β
inst✝² : FunLike F β ℝ
inst✝¹ : NonnegHomClass F β ℝ
inst✝ : ZeroHomClass F β ℝ
v : F
l : α → β
hv : IsNonarchimedean ⇑v
a : α
s : Finset α
ha : a ∉ s
ih : v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
⊢ v (l a) ≤ ⨆ i, v (l ↑i)

Tactic:
exact Finite.le_ciSup_of_le ⟨_, s.mem_insert_self a⟩ le_rfl

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ -2 ≠ -1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ 0 ≤ ↑(Nat.card ι) ^ totalWeight K

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : S.multiplicity - 1 = 0
⊢ 1 ≤ 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
this : 0 ≤ logHeight A + logHeight x
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: N : ℕ
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 < n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
h_fin₁ : t₁.Finite
h_fin₂ : t₂.Finite
⊢ ∀ (x : Ideal (𝓞 K)), ((↑(Nat.castRingHom ℝ)).comp ↑absNorm) x = 1 → x = 1

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
⊢ (logHeight fun a ↦ x a.1 * y a.2) = logHeight x + logHeight y

Tactic:
simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  rw [mulHeight_fun_mul_eq hx hy]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ ↑n / (↑n + 1) ^ s ≤ (↑n + 1) / (↑n + 1) ^ s

pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)

Tactic:
· gcongr
          linarith

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s ≤ (1 / ↑(n + 1)) ^ (s - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 < n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 ≤ ↑(n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
s : ℝ
hs : 1 ≤ s
⊢ 0 < n + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
⊢ 1 ≤ ↑(n + 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : a ∈ archAbsVal.toFinset), ⟨a, ⋯⟩ ∈ univ

Tactic:
by simp

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, (χ x + ψ (1 - x) - 1 + (χ x - 1) * (ψ (1 - x) - 1)) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
sum_add_distrib,

Goal state after:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x, (χ x + ψ (1 - x) - 1) + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : a ∈ archAbsVal.toFinset), ↑⟨a, ⋯⟩ = a

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : Inhabited (InfinitePlace K)
⊢ 0 < totalWeight K

Tactic:
simpa [totalWeight, archAbsVal, multisetInfinitePlace]
    using Fintype.sum_pos
      (Function.ne_iff.mpr ⟨default, (default : InfinitePlace K).mult_ne_zero⟩).pos

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
have := completedRiemannZeta_eq 1

Goal state after:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / (1 - 1)
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ 0 ≤ 4

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 1 < Module.rank ℝ ℂ

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (1 - id) 0 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
h₃ : HasDerivAt (Gamma ∘ fun x ↦ x / 2 + 1) (deriv Gamma (0 / 2 + 1) * (1 / 2 + 0)) 0
h : -(log (2 * ↑π) * 2) = ↑γ - log (4 * ↑π) + (-log ↑π + -↑γ)
⊢ (((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2)) * Gamma ∘ fun x ↦ x / 2 + 1) 0 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ {↑n} ⊆ Set.range ![a, ↑n]

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
this : ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1
i : InfinitePlace K
a✝ : i ∈ univ
⊢ ↑n ≤ i (![↑a, ↑n] 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v w : InfinitePlace K
a✝ : w ∈ univ.erase v
⊢ ↑n ≤ w (![↑x, ↑n] 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ ↑n ≤ v (![↑x, ↑n] 1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ Real.log (riemannZeta ↑s).re + Real.log (s - 1)) =O[𝓝[>] 1] fun x ↦ x - 1

Tactic:
by
  suffices (fun (s : ℝ) ↦ (riemannZeta₁ s).re.log) =O[𝓝 1] (· - 1) by
    refine (this.mono nhdsWithin_le_nhds).congr'
      (eventually_nhdsWithin_of_forall (fun s hs ↦ ?_)) .rfl
    simp [log_riemannZeta_eq_neg_log_sub_add_ofReal hs]
  suffices DifferentiableAt ℝ (fun (s : ℝ) ↦ (riemannZeta₁ s).re.log) 1 by
    simpa using this.isBigO_sub
  have : Differentiable ℝ riemannZeta₀ := by fun_prop
  fun_prop (disch := simp)

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ v ↑x ≤ B / ↑n ^ (totalWeight K - 1)

Tactic:
classical
  rw [le_div_iff₀' (by positivity)]
  calc
    _ ≤ n ^ (totalWeight K - 1) * ⨆ i, v (![(x : K), n] i) := by
      gcongr; exact Finite.le_ciSup_of_le 0 le_rfl
    _ ≤ (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) *
         (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) * ⨆ i, v (![(x : K), n] i) := by
      rw [pow_totalWeight_sub_one_eq hn]
      gcongr
      · exact Real.iSup_nonneg_of_nonnegHomClass ..
      · exact prod_nonneg fun _ _ ↦ pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass ..) _
      all_goals exact Finite.le_ciSup_of_le 1 <| by simp
    _ ≤ B := by
      rwa [mul_assoc, pow_sub_one_mul v.mult_ne_zero, prod_erase_mul _ _ (mem_univ v)]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ riemannZeta₁ 1 ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
⊢ h.map f = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
⊢ (aeval h.root) f = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : x = 0
⊢ ∀ x ∈ Finset.univ, 0 x = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ h.modByMonicHom (h.map (X ^ n)) = X ^ n

Tactic:
modByMonicHom_map,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
a✝ : Nontrivial R
⊢ X ^ n %ₘ f = X ^ n