[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ (k + 1)) / 2)) * ↑↑(p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1)))
[PROOFSTEP]
rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (p ^ (k + 1)).pos) hk]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑((-1) ^ ((↑p - 1) / 2)) * ↑↑(p ^ (↑p - 2))
[PROOFSTEP]
rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
hodd : p ≠ 2
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    ↑((-1) ^ (φ ↑(p ^ k) / 2)) * ↑↑(p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1)))
[PROOFSTEP]
rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
[PROOFSTEP]
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ∃ u n, discr ℚ ↑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
[PROOFSTEP]
exact discr_prime_pow_eq_unit_mul_pow hζ (cyclotomic.irreducible_rat (p ^ k).pos)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
refine' ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y = x) → IsIntegral ℤ x
[PROOFSTEP]
swap
[GOAL]
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
⊢ (∃ y, ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y = x) → IsIntegral ℤ x
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case refine'_2.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
y : { x // x ∈ adjoin ℤ {ζ} }
⊢ IsIntegral ℤ (↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) y)
[PROOFSTEP]
exact
  IsIntegral.algebraMap (le_integralClosure_iff_isIntegral.1 (adjoin_le_integralClosure (hζ.isIntegral (p ^ k).pos)) _)
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
let B := hζ.subOnePowerBasis ℚ
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have hint : IsIntegral ℤ B.gen := isIntegral_sub (hζ.isIntegral (p ^ k).pos) isIntegral_one
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : discr ℚ ↑B.basis • x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
H : discr ℚ ↑B.basis • x ∈ adjoin ℤ {B.gen}
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [hun] at H
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
H : (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
replace H := Subalgebra.smul_mem _ H u.inv
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul, Units.inv_mul, Int.cast_one,
  one_mul, PNat.pow_coe, Nat.cast_pow, smul_def, map_pow] at H
[GOAL]
case refine'_1.intro.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ k} ℚ K
u : ℤˣ
n : ℕ
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
cases k
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ IsCyclotomicExtension {1} ℚ K
[PROOFSTEP]
simpa using hcycl
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have : x ∈ (⊥ : Subalgebra ℚ K) := by
  rw [singleton_one ℚ K]
  exact mem_top
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ ⊥
[PROOFSTEP]
rw [singleton_one ℚ K]
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this : IsCyclotomicExtension {1} ℚ K
⊢ x ∈ ⊤
[PROOFSTEP]
exact mem_top
[GOAL]
case refine'_1.intro.intro.zero
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
this✝ : IsCyclotomicExtension {1} ℚ K
this : x ∈ ⊥
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨y, rfl⟩ := mem_bot.1 this
[GOAL]
case refine'_1.intro.intro.zero.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
h : IsIntegral ℤ (↑(algebraMap ℚ K) y)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
[GOAL]
case refine'_1.intro.intro.zero.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h
[GOAL]
case refine'_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : ↑(algebraMap ℤ ℚ) z = y
⊢ ↑(algebraMap ℚ K) y ∈ adjoin ℤ {ζ}
[PROOFSTEP]
rw [← hz, ← IsScalarTower.algebraMap_apply]
[GOAL]
case refine'_1.intro.intro.zero.intro.intro
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.zero} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.zero)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝¹ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.zero} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
this✝ : IsCyclotomicExtension {1} ℚ K
y : ℚ
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * ↑(algebraMap ℚ K) y ∈ adjoin ℤ {B.gen}
this : ↑(algebraMap ℚ K) y ∈ ⊥
h : IsIntegral ℤ y
z : ℤ
hz : ↑(algebraMap ℤ ℚ) z = y
⊢ ↑(algebraMap ℤ K) z ∈ adjoin ℤ {ζ}
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ _
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {((p : ℕ) : ℤ)}) :=
  by
  have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
  have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
  rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
  rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
    show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
  haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
  rw [IsPrimitiveRoot.subOnePowerBasis_gen, map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
  exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (p ^ _).pos)
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ B.gen = map (algebraMap ℤ ℚ) (minpoly ℤ B.gen)
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic ↑(p ^ Nat.succ n✝) ℚ) (X + 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : minpoly ℚ (ζ - 1) = comp (cyclotomic ↑(p ^ Nat.succ n✝) ℚ) (X + 1)
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
  show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = comp (map (Int.castRingHom ℚ) (cyclotomic ↑(p ^ Nat.succ n✝) ℤ)) (X + 1)
⊢ Int.castRingHom ℚ = algebraMap ℤ ℚ
[PROOFSTEP]
rfl
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = comp (map (algebraMap ℤ ℚ) (cyclotomic ↑(p ^ Nat.succ n✝) ℤ)) (X + 1)
⊢ X + 1 = map (algebraMap ℤ ℚ) (X + 1)
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
this : CharZero ℚ
⊢ IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
rw [IsPrimitiveRoot.subOnePowerBasis_gen, map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this✝ : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
h₁ : minpoly ℚ (ζ - 1) = map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1))
h₂ : map (algebraMap ℤ ℚ) (minpoly ℤ (ζ - 1)) = map (algebraMap ℤ ℚ) (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1))
this : CharZero ℚ
⊢ IsEisensteinAt (comp (cyclotomic ↑(p ^ Nat.succ n✝) ℤ) (X + 1)) (Submodule.span ℤ {↑↑p})
[PROOFSTEP]
exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ x ∈ adjoin ℤ {ζ}
[PROOFSTEP]
refine'
  adjoin_le _
    (mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt (n := n) (Nat.prime_iff_prime_int.1 hp.out) hint h
      (by simpa using H) hmin)
[GOAL]
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ ↑↑p ^ n • x ∈ adjoin ℤ {B.gen}
[PROOFSTEP]
simpa using H
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ {B.gen} ⊆ ↑(adjoin ℤ {ζ})
[PROOFSTEP]
simp only [Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
case refine'_1.intro.intro.succ
p : ℕ+
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
x : K
h : IsIntegral ℤ x
u : ℤˣ
n n✝ : ℕ
hcycl : IsCyclotomicExtension {p ^ Nat.succ n✝} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ Nat.succ n✝)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := finiteDimensional {p ^ Nat.succ n✝} ℚ K
hun : discr ℚ ↑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑(p ^ n)
H✝ : u.inv • (↑↑u * ↑↑(p ^ n)) • x ∈ adjoin ℤ {B.gen}
H : ↑(algebraMap ℚ K) ↑↑p ^ n * x ∈ adjoin ℤ {B.gen}
hmin : IsEisensteinAt (minpoly ℤ B.gen) (Submodule.span ℤ {↑↑p})
⊢ (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).gen ∈ adjoin ℤ {ζ}
[PROOFSTEP]
exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
rw [← pow_one p] at hζ hcycl
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ 1} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ 1)
⊢ IsIntegralClosure { x // x ∈ adjoin ℤ {ζ} } ℤ K
[PROOFSTEP]
exact isIntegralClosure_adjoin_singleton_of_prime_pow hζ
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
haveI : CharZero ℚ := StrictOrderedSemiring.to_charZero
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
⊢ IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
[PROOFSTEP]
refine'
  ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, _⟩, rfl⟩, _⟩⟩
    -- Porting note: having `.isIntegral_iff` inside the definition of `this` causes an error.
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
have := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ)
[GOAL]
case refine'_1
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
h : IsIntegral ℤ x
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
⊢ x ∈ adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
obtain ⟨y, rfl⟩ := this.isIntegral_iff.1 h
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ ↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y ∈
    adjoin ℤ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
refine' adjoin_mono _ y.2
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} ⊆ {b | b ^ ↑(p ^ k) = 1}
[PROOFSTEP]
simp only [PNat.pow_coe, Set.singleton_subset_iff, Set.mem_setOf_eq]
[GOAL]
case refine'_1.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this✝ : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
this :
  IsIntegralClosure { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } ℤ (CyclotomicField (p ^ k) ℚ)
y : { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} }
h :
  IsIntegral ℤ
    (↑(algebraMap { x // x ∈ adjoin ℤ {zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)} } (CyclotomicField (p ^ k) ℚ)) y)
⊢ zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ) ^ ↑p ^ k = 1
[PROOFSTEP]
exact hζ.pow_eq_one
[GOAL]
case refine'_2
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
x : CyclotomicField (p ^ k) ℚ
⊢ (∃ y, ↑(algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y = x) → IsIntegral ℤ x
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case refine'_2.intro
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
this : CharZero ℚ
hζ : IsPrimitiveRoot (zeta (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)) ↑(p ^ k)
y : CyclotomicRing (p ^ k) ℤ ℚ
⊢ IsIntegral ℤ (↑(algebraMap (CyclotomicRing (p ^ k) ℤ ℚ) (CyclotomicField (p ^ k) ℚ)) y)
[PROOFSTEP]
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _) _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)
[PROOFSTEP]
rw [← pow_one p]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
⊢ IsIntegralClosure (CyclotomicRing (p ^ 1) ℤ ℚ) ℤ (CyclotomicField (p ^ 1) ℚ)
[PROOFSTEP]
exact cyclotomicRing_isIntegralClosure_of_prime_pow
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ 𝓞 K } K) (integralPowerBasis hζ).gen = ↑{ val := ζ, property := (_ : IsIntegral ℤ ζ) }
[PROOFSTEP]
rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ 𝓞 K } K) (↑(adjoinEquivRingOfIntegers hζ) { val := ζ, property := (_ : ζ ∈ adjoin ℤ {ζ}) }) =
    ↑{ val := ζ, property := (_ : IsIntegral ℤ ζ) }
[PROOFSTEP]
simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ↑(algebraMap { x // x ∈ adjoin ℤ {ζ} } K) { val := ζ, property := (_ : ζ ∈ adjoin ℤ {ζ}) } = ζ
[PROOFSTEP]
rfl
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (integralPowerBasis hζ).dim = φ ↑(p ^ k)
[PROOFSTEP]
simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ, natDegree_cyclotomic]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot (?m.655556 hζ) ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (integralPowerBasis' hζ).dim = φ ↑p
[PROOFSTEP]
erw [@integralPowerBasis_dim p 1 K _ _ _ _ (by convert hcycl; rw [pow_one]) (by rwa [pow_one]), pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (integralPowerBasis hζ).gen ∈ adjoin ℤ {{ val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }}
[PROOFSTEP]
simp only [integralPowerBasis_gen]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ { val := ζ, property := (_ : IsIntegral ℤ ζ) } ∈ adjoin ℤ {{ val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }}
[PROOFSTEP]
convert
  Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ (⟨ζ - 1, _⟩ : 𝓞 K))
    (Subalgebra.one_mem _)
      -- Porting note: `simp` was able to finish the proof.
[GOAL]
case h.e'_4.h.e'_3
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ = ↑({ val := ζ - 1, property := ?m.678368 } + 1)
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ - 1 ∈ 𝓞 K
[PROOFSTEP]
simp only [Subsemiring.coe_add, Subalgebra.coe_toSubsemiring, OneMemClass.coe_one, sub_add_cancel]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ ζ - 1 ∈ 𝓞 K
[PROOFSTEP]
exact Subalgebra.sub_mem _ (hζ.isIntegral (by simp)) (Subalgebra.one_mem _)
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ 0 < ↑(p ^ k)
[PROOFSTEP]
simp
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (subOneIntegralPowerBasis hζ).gen = { val := ζ - 1, property := (_ : ζ - 1 ∈ 𝓞 K) }
[PROOFSTEP]
simp [subOneIntegralPowerBasis]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot (?m.698529 hζ) ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K
[PROOFSTEP]
convert hcycl
[GOAL]
case h.e'_1.h.e'_4
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ p ^ 1 = p
[PROOFSTEP]
rw [pow_one]
[GOAL]
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
inst✝ : CharZero K
ζ : K
hp : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)
[PROOFSTEP]
rwa [pow_one]


[GOAL]
x : ℝ
⊢ LiouvilleWith 1 x
[PROOFSTEP]
use 2
[GOAL]
case h
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
have hn' : (0 : ℝ) < n := by simpa
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
[PROOFSTEP]
simpa
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by rw [lt_div_iff hn', Int.cast_add, Int.cast_one]; exact Int.lt_floor_add_one _
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x < ↑(⌊x * ↑n⌋ + 1) / ↑n
[PROOFSTEP]
rw [lt_div_iff hn', Int.cast_add, Int.cast_one]
[GOAL]
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
exact Int.lt_floor_add_one _
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ |x - ↑(⌊x * ↑n⌋ + 1) / ↑n| < 2 / ↑n ^ 1
[PROOFSTEP]
rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add', add_div_eq_mul_add_div _ _ hn'.ne',
  div_lt_div_right hn']
[GOAL]
case h
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) < x * ↑n + 2
[PROOFSTEP]
convert add_lt_add_right ((Int.floor_le (x * n)).trans_lt (lt_add_one _)) 1 using 1
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
try push_cast
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
try push_cast
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑⌊x * ↑n⌋ + 1 = ↑⌊x * ↑n⌋ + 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_4
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 2 = x * ↑n + 1 + 1
[PROOFSTEP]
ring
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
rcases h with ⟨C, hC⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
[PROOFSTEP]
refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < max C 1 / ↑x_1 ^ p
[PROOFSTEP]
rintro n ⟨hle, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < max C 1 / ↑n ^ p
[PROOFSTEP]
refine ⟨hle, m, hne, hlt.trans_le ?_⟩
[GOAL]
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ max C 1 / ↑n ^ p
[PROOFSTEP]
exact div_le_div_of_le (rpow_nonneg_of_nonneg n.cast_nonneg _) (le_max_left _ _)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
⊢ LiouvilleWith q x
[PROOFSTEP]
rcases h.exists_pos with ⟨C, hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith q x
[PROOFSTEP]
refine ⟨C, hC.mono ?_⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q
[PROOFSTEP]
rintro n ⟨hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ q
[PROOFSTEP]
refine ⟨m, hne, hlt.trans_le <| div_le_div_of_le_left hC₀.le ?_ ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ 0 < ↑n ^ q
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑n ^ q ≤ ↑n ^ p
[PROOFSTEP]
exacts [rpow_pos_of_pos (Nat.cast_pos.2 hn) _, rpow_le_rpow_of_exponent_le (Nat.one_le_cast.2 hn) hle]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
have : ∀ᶠ n : ℕ in atTop, C < n ^ (p - q) := by
  simpa only [(· ∘ ·), neg_sub, one_div] using
    ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_nat_cast_atTop_atTop).eventually (eventually_gt_atTop C)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
[PROOFSTEP]
simpa only [(· ∘ ·), neg_sub, one_div] using
  ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_nat_cast_atTop_atTop).eventually (eventually_gt_atTop C)
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
refine (this.and_frequently hC).mono ?_
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hlt : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
⊢ ∀ (x_1 : ℕ),
    (C < ↑x_1 ^ (p - q) ∧ 1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-q)
[PROOFSTEP]
rintro n ⟨hnC, hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
[PROOFSTEP]
refine ⟨m, hne, hlt.trans <| (div_lt_iff <| rpow_pos_of_pos hn _).2 ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ C < ↑n ^ (-q) * ↑n ^ p
[PROOFSTEP]
rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
⊢ LiouvilleWith p (x * ↑r)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (x * ↑r)
[PROOFSTEP]
refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
[GOAL]
case intro.intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m,
        x * ↑r ≠ ↑m / ↑(r.den • id x_1) ∧
          |x * ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id x_1) ^ p
[PROOFSTEP]
rintro n ⟨_hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
have A : (↑(r.num * m) : ℝ) / ↑(r.den • id n) = m / n * r := by simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
[PROOFSTEP]
simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ∃ m, x * ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x * ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨r.num * m, ?_, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑(r.num * m) / ↑(r.den • id n)
[PROOFSTEP]
rw [A]
[GOAL]
case intro.intro.intro.intro.intro.refine_1
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑m / ↑n * ↑r
[PROOFSTEP]
simp [hne, hr]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x * ↑r - ↑(r.num * m) / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
rw [A, ← sub_mul, abs_mul]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
[PROOFSTEP]
simp only [smul_eq_mul, id.def, Nat.cast_mul]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p
[PROOFSTEP]
refine (mul_lt_mul_of_pos_right hlt <| abs_pos.2 <| Rat.cast_ne_zero.2 hr).trans_le ?_
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ C / ↑n ^ p * |↑r| ≤ ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p
[PROOFSTEP]
rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
[GOAL]
case intro.intro.intro.intro.intro.refine_2
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |↑r| * (C / ↑n ^ p) ≤ ↑|r| * (C / ↑n ^ p)
[PROOFSTEP]
simp only [Rat.cast_abs, le_refl]
[GOAL]
case intro.intro.intro.intro.intro.refine_2.hc
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ ↑r.den ^ p ≠ 0
[PROOFSTEP]
exact (rpow_pos_of_pos (Nat.cast_pos.2 r.pos) _).ne'
[GOAL]
case intro.intro.intro.intro.intro.refine_2.h
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑r.den
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
case intro.intro.intro.intro.intro.refine_2.h₁
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact Nat.cast_nonneg _
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hr : r ≠ 0
h : LiouvilleWith p (x * ↑r)
⊢ LiouvilleWith p x
[PROOFSTEP]
simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel hr, Rat.cast_one, mul_one] using h.mul_rat (inv_ne_zero hr)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hr : r ≠ 0
⊢ LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_rat_iff hr]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hm : m ≠ 0
⊢ LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int, mul_rat_iff (Int.cast_ne_zero.2 hm)]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hm : m ≠ 0
⊢ LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_int_iff hm]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat, mul_rat_iff (Nat.cast_ne_zero.2 hn)]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [mul_comm, mul_nat_iff hn]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * ↑n)
[PROOFSTEP]
exact h.mul_nat hn
[GOAL]
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + ↑r)
[PROOFSTEP]
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
[GOAL]
case intro.intro
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (x + ↑r)
[PROOFSTEP]
refine ⟨r.den ^ p * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
[GOAL]
case intro.intro
p q x y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) →
      ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id x_1) ∧ |x + ↑r - ↑m / ↑(r.den • id x_1)| < ↑r.den ^ p * C / ↑(r.den • id x_1) ^ p
[PROOFSTEP]
rintro n ⟨hn, m, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have hr : (0 : ℝ) < r.den := Nat.cast_pos.2 r.pos
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 (zero_lt_one.trans_le hn).ne'
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r :=
  by
  rw [Algebra.id.smul_eq_mul, id.def]
  nth_rewrite 4 [← Rat.num_div_den r]
  push_cast
  rw [add_div, mul_div_mul_left _ _ (ne_of_gt hr), mul_div_mul_right _ _ hn']
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
[PROOFSTEP]
rw [Algebra.id.smul_eq_mul, id.def]
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den * n) = ↑m / ↑n + ↑r
[PROOFSTEP]
nth_rewrite 4 [← Rat.num_div_den r]
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den * n) = ↑m / ↑n + ↑(↑r.num / ↑r.den)
[PROOFSTEP]
push_cast
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
⊢ (↑r.den * ↑m + ↑r.num * ↑n) / (↑r.den * ↑n) = ↑m / ↑n + ↑r.num / ↑r.den
[PROOFSTEP]
rw [add_div, mul_div_mul_left _ _ (ne_of_gt hr), mul_div_mul_right _ _ hn']
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ ∃ m, x + ↑r ≠ ↑m / ↑(r.den • id n) ∧ |x + ↑r - ↑m / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨r.den * m + r.num * n, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) ∧
    |x + ↑r - ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n)| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
rw [this, add_sub_add_right_eq_sub]
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r ∧ |x - ↑m / ↑n| < ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
[GOAL]
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ x + ↑r ≠ ↑m / ↑n + ↑r
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
have : (r.den ^ p : ℝ) ≠ 0 := (rpow_pos_of_pos hr _).ne'
[GOAL]
case intro.intro.intro.intro.intro
p q x y : ℝ
r✝ : ℚ
m✝ : ℤ
n✝ : ℕ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hr : 0 < ↑r.den
hn' : ↑n ≠ 0
this✝ : ↑(↑r.den * m + r.num * ↑n) / ↑(r.den • id n) = ↑m / ↑n + ↑r
this : ↑r.den ^ p ≠ 0
⊢ C / ↑n ^ p = ↑r.den ^ p * C / ↑(r.den • id n) ^ p
[PROOFSTEP]
simp [mul_rpow, Nat.cast_nonneg, mul_div_mul_left, this]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p (x + ↑r)
⊢ LiouvilleWith p x
[PROOFSTEP]
simpa using h.add_rat (-r)
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑r + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int m, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑m + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_int_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x + ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat n, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [add_comm, add_nat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)
[PROOFSTEP]
rcases h with ⟨C, hC⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (-x)
[PROOFSTEP]
refine ⟨C, hC.mono ?_⟩
[GOAL]
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p
[PROOFSTEP]
rintro n ⟨m, hne, hlt⟩
[GOAL]
case intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ |-x - ↑m / ↑n| < C / ↑n ^ p
[PROOFSTEP]
refine ⟨-m, by simp [neg_div, hne], ?_⟩
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -x ≠ ↑(-m) / ↑n
[PROOFSTEP]
simp [neg_div, hne]
[GOAL]
case intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| < C / ↑n ^ p
[PROOFSTEP]
convert hlt using 1
[GOAL]
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| = |x - ↑m / ↑n|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |↑(-m) / ↑n - -x| = |x - ↑m / ↑n|
[PROOFSTEP]
congr! 1
[GOAL]
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n
[PROOFSTEP]
ring
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑m) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_int, sub_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x
[PROOFSTEP]
rw [← Rat.cast_coe_nat, sub_rat_iff]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
⊢ LiouvilleWith p (↑n - x) ↔ LiouvilleWith p x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
p q x y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
m : ℤ
⊢ x ≠ ↑m
[PROOFSTEP]
rintro rfl
[GOAL]
p q y : ℝ
r : ℚ
m✝ : ℤ
n : ℕ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False
[PROOFSTEP]
rename' m => M
[GOAL]
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False
[PROOFSTEP]
rcases((eventually_gt_atTop 0).and_frequently (h.frequently_lt_rpow_neg hp)).exists with
  ⟨n : ℕ, hn : 0 < n, m : ℤ, hne : (M : ℝ) ≠ m / n, hlt : |(M - m / n : ℝ)| < n ^ (-1 : ℝ)⟩
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ False
[PROOFSTEP]
refine hlt.not_le ?_
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|
[PROOFSTEP]
have hn' : (0 : ℝ) < n := by simpa
[GOAL]
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ 0 < ↑n
[PROOFSTEP]
simpa
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|
[PROOFSTEP]
rw [rpow_neg_one, ← one_div, sub_div' _ _ _ hn'.ne', abs_div, Nat.abs_cast, div_le_div_right hn']
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |↑M * ↑n - ↑m|
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |M * ↑n - m|
[PROOFSTEP]
rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
[PROOFSTEP]
rw [Ne.def, eq_div_iff hn'.ne'] at hne
[GOAL]
case intro.intro.intro.intro
p q y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬↑M * ↑n = ↑m
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m
[PROOFSTEP]
exact_mod_cast hne
[GOAL]
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
hp : 1 < p
⊢ Irrational x
[PROOFSTEP]
rintro ⟨r, rfl⟩
[GOAL]
case intro
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | h0)
[GOAL]
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False
[PROOFSTEP]
refine h.ne_cast_int hp 0 ?_
[GOAL]
case intro.inl
p q y : ℝ
r : ℚ
m : ℤ
n : ℕ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0
[PROOFSTEP]
rw [Rat.cast_zero, Int.cast_zero]
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False
[PROOFSTEP]
refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ ↑r * ↑r⁻¹ = ↑1
[PROOFSTEP]
rw [Rat.cast_inv, mul_inv_cancel]
[GOAL]
case intro.inr
p q y : ℝ
r✝ : ℚ
m : ℤ
n : ℕ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ 1 = ↑1
case intro.inr p q y : ℝ r✝ : ℚ m : ℤ n : ℕ hp : 1 < p r : ℚ h : LiouvilleWith p ↑r h0 : r ≠ 0 ⊢ ↑r ≠ 0
[PROOFSTEP]
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
refine Classical.not_not.1 fun H => ?_
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
H : ¬∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
⊢ False
[PROOFSTEP]
simp only [Liouville, not_forall, not_exists, not_frequently, not_and, not_lt, eventually_atTop] at H
[GOAL]
x : ℝ
hx : Liouville x
n : ℕ
H : ∃ a, ∀ (b : ℕ), b ≥ a → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ False
[PROOFSTEP]
rcases H with ⟨N, hN⟩
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ False
[PROOFSTEP]
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
  by
  intro b hb
  replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
  have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) :=
    by
    simp only [one_div]
    exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
  refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
  exact fun m hm a => hm a
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
⊢ ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
intro b hb
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : b > 1
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) :=
  by
  simp only [one_div]
  exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
[PROOFSTEP]
simp only [one_div]
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => (↑b ^ m)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
[PROOFSTEP]
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
[GOAL]
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ), (∀ (m : ℤ), 1 / ↑b ^ x_1 ≤ dist x (↑m / ↑b)) → ∀ (a : ℤ), 1 / ↑b ^ x_1 ≤ |x - ↑a / ↑b|
[PROOFSTEP]
exact fun m hm a => hm a
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
[PROOFSTEP]
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
  (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
[GOAL]
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
[PROOFSTEP]
rcases(this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩
[GOAL]
case intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
⊢ False
[PROOFSTEP]
rcases hx m with ⟨a, b, hb, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a b : ℤ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
⊢ False
[PROOFSTEP]
lift b to ℕ using zero_le_one.trans hb.le
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
⊢ False
[PROOFSTEP]
norm_cast at hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : |x - ↑a / ↑↑b| < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False
[PROOFSTEP]
push_cast at hne hlt
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
⊢ False
[PROOFSTEP]
cases' le_or_lt N b with h h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
⊢ False
[PROOFSTEP]
refine' (hN b h a hne).not_lt (hlt.trans_le _)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
have hb0 : (0 : ℝ) < b := zero_lt_one.trans hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
hb0 : 0 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
[PROOFSTEP]
exact one_div_le_one_div_of_le (pow_pos hb0 _) (pow_le_pow hb.le hnm)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inr
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ |x - ↑x_1 / ↑b|
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ m
h : b < N
⊢ False
[PROOFSTEP]
exact (hm b h hb _).not_lt hlt
[GOAL]
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x
[PROOFSTEP]
suffices : LiouvilleWith ⌈p⌉₊ x
[GOAL]
x : ℝ
hx : Liouville x
p : ℝ
this : LiouvilleWith (↑⌈p⌉₊) x
⊢ LiouvilleWith p x
case this x : ℝ hx : Liouville x p : ℝ ⊢ LiouvilleWith (↑⌈p⌉₊) x
[PROOFSTEP]
exact this.mono (Nat.le_ceil p)
[GOAL]
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
[PROOFSTEP]
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
[GOAL]
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < 1 / ↑x_1 ^ ↑⌈p⌉₊
[PROOFSTEP]
rintro b ⟨_hb, a, hne, hlt⟩
[GOAL]
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ |x - ↑m / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
[PROOFSTEP]
refine ⟨a, hne, ?_⟩
[GOAL]
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ ⌈p⌉₊
⊢ |x - ↑a / ↑b| < 1 / ↑b ^ ↑⌈p⌉₊
[PROOFSTEP]
rwa [rpow_nat_cast]
[GOAL]
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
[PROOFSTEP]
refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
rcases((eventually_gt_atTop 1).and_frequently ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists with
  ⟨b, hb, a, hne, hlt⟩
[GOAL]
case intro.intro.intro.intro
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
exact ⟨a, b, by exact_mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ 1 < ↑b
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑↑b| < 1 / ↑↑b ^ n
[PROOFSTEP]
simpa [rpow_neg] using hlt