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

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p q : K[X]
x✝ : ¬q = 0
h0 : ¬p = 0 ∧ ¬q = 0
h1 : v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) < 1
hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1
this : ∀ (r : K[X]), v ↑r ≠ 1 → r ≠ 0 → {p | v ↑p < 1 ∧ ¬p = 0}.Nonempty
⊢ {p | v ↑p < 1 ∧ ¬p = 0}.Nonempty

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (S ∙ f A.det) ≤ M
this : Nontrivial (R ⧸ p)
⊢ (-1).det = (-1) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
⊢ 𝓟D.inertiaDeg A = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : (valuation K v) x.ofVal < exp (m.log / ↑e)
hx₀ : x ≠ 0
⊢ (valuation K v) x.ofVal ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : (valuation K v) x.ofVal < exp (m.log / ↑e)
hx₀ : x ≠ 0
⊢ exp (m.log / ↑e) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
⊢ a.degree < πᵥ.degree

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ Disjoint {x | ∃ k, beattySeq r k = x} {x | ∃ k, beattySeq' s k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hπᵥ : ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne = a * b
hb : ¬IsUnit b
⊢ 1 ≤ v ↑a

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
⊢ Irreducible (⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ πᵥ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ v ↑πᵥ < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ ¬∃ j k m, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1 ∧ ↑m ≤ ↑j / s ∧ (↑j + 1) / s < ↑m + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : ((valuation K v) x.ofVal).log < (exp (m.log / ↑e)).log
hx₀ : x ≠ 0
⊢ (valuation K v) x.ofVal ^ v.asIdeal.ramificationIdx' w.asIdeal ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : ((valuation K v) x.ofVal).log < (exp (m.log / ↑e)).log
hx₀ : x ≠ 0
⊢ σw (σL (σwV ↑γL)) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
j : ℤ
h : r > 0
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) q) = 1
⊢ v ((algebraMap K[X] K⟮X⟯) π) ^ k * v ((algebraMap K[X] K⟮X⟯) q) =
    v ↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
j : ℤ
h : r > 0
⊢ j ∈ {x | ∃ k, beattySeq' r k = x} ∨ ∃ k, ↑k ≤ ↑j / r ∧ (↑j + 1) / r < ↑k + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k, beattySeq r k = x}ᶜ = {x | ∃ k, beattySeq' s k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k, beattySeq' r k = x}ᶜ = {x | ∃ k, beattySeq s k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
⊢ UniformContinuous ⇑(algebraMap (WithVal (valuation K v)) (WithVal (valuation L w)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 1 ≤ ↑k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ 1 ≤ ↑k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∈ s.prodPrimes.divisors
⊢ Squarefree d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∏ p ∈ d.primeFactors, s.nu p = s.nu d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ 0 < ∏ p ∈ d.primeFactors, s.nu p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ 0 < s.nu d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ s.nu d ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
⊢ ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ ∏ p ∈ d.primeFactors, s.nu p < ∏ p ∈ d.primeFactors, 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ ∏ p ∈ d.primeFactors, 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
⊢ s.nu d < 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
⊢ multSum d = s.nu d * s.totalMass + rem d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
⊢ ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ siftedSum = ∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬q % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1 ∧ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x} = {n | 0 < n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x} = {n | 0 < n}

Tactic:
by
  apply Set.eq_of_subset_of_subset
  · rintro j (⟨⟨k, hk, hjk⟩, -⟩ | ⟨⟨k, hk, hjk⟩, -⟩)
    · rw [Set.mem_ofPred_eq, ← hjk, beattySeq, Int.floor_pos]
      exact one_le_mul_of_one_le_of_one_le (by norm_cast) hrs.lt.le
    · rw [Set.mem_ofPred_eq, ← hjk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one]
      exact one_lt_mul_of_le_of_lt (by norm_cast) hrs.symm.lt
  intro j (hj : 0 < j)
  have hb₁ : ∀ s ≥ 0, j ∈ {beattySeq s k | k > 0} ↔ j ∈ {beattySeq s k | k} := by
    intro _ hs
    refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
    rw [← hk, beattySeq, Int.floor_pos] at hj
    exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans_le hj) hs
  have hb₂ : ∀ s ≥ 0, j ∈ {beattySeq' s k | k > 0} ↔ j ∈ {beattySeq' s k | k} := by
    intro _ hs
    refine ⟨fun ⟨k, _, hk⟩ ↦ ⟨k, hk⟩, fun ⟨k, hk⟩ ↦ ⟨k, ?_, hk⟩⟩
    rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj
    exact_mod_cast pos_of_mul_pos_left (zero_lt_one.trans hj) hs
  rw [Set.mem_symmDiff, hb₁ _ hrs.nonneg, hb₂ _ hrs.symm.nonneg, ← compl_beattySeq hrs,
    Set.notMem_compl_iff, Set.mem_compl_iff, and_self, and_self]
  exact or_not

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
⊢ {x | ∃ k > 0, beattySeq' r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ v ↑πᵥ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
h0 : v ↑πᵥ ≠ 0
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ p ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
⊢ ∃ z, v f = v ↑πᵥ ^ z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
⊢ v ↑πᵥ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d =
    s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d

Tactic:
by

Goal state after: