internlm/Lean-Github huggingface dataset:
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p ∧ orderOf (ClassGroup.mk Izero.unit') ∣ Fintype.card (ClassGroup A)
Tactic:
refine ⟨?_, orderOf_dvd_card⟩
Proof state after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ orderOf (ClassGroup.mk Izero.unit') ∣ p
Tactic:
rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff]
Proof state after:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑(Izero.unit' ^ p)).IsPrincipal
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case neg
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : IsUnit I
⊢ (↑↑(Izero.unit' ^ p)).IsPrincipal
Tactic:
simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI]
Proof state after:
no goals
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ (↑I).IsPrincipal
Tactic:
rw [Izero, FractionalIdeal.coe_zero]
Proof state after:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ ⊥.IsPrincipal
Theorem: isPrincipal_of_isPrincipal_pow_of_Coprime'
Proof state before:
case pos
K✝ : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p✝} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p✝
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Fintype (ClassGroup A)
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : ℕ
H : p.Coprime (Fintype.card (ClassGroup A))
I : FractionalIdeal A⁰ K
hI : (↑(I ^ p)).IsPrincipal
Izero : I = 0
⊢ ⊥.IsPrincipal
Tactic:
exact bot_isPrincipal
Proof state after:
no goals
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
⊢ ∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
by_contra H1
Proof state after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
have hI' : (I : FractionalIdeal R⁰ K) ≠ 0 :=
  by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hI (dvd_zero _)
Proof state after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
⊢ False
Tactic:
have hJ' : (J : FractionalIdeal R⁰ K) ≠ 0 :=
  by rw [← coeIdeal_bot, Ne, coeIdeal_inj]; rintro rfl; exact hJ (dvd_zero _)
Proof state after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : (↑(↑I / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
rw [isPrincipal_iff] at h
Proof state after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : ∃ x, ↑I / ↑J = spanSingleton R⁰ x
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
h : ∃ x, ↑I / ↑J = spanSingleton R⁰ x
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
obtain ⟨a, ha⟩ := h
Proof state after:
case intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a : K
ha : ↑I / ↑J = spanSingleton R⁰ a
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a : K
ha : ↑I / ↑J = spanSingleton R⁰ a
⊢ False
Tactic:
obtain ⟨s, t, rfl⟩ := IsLocalization.mk'_surjective R⁰ a
Proof state after:
case intro.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case intro.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
⊢ False
Tactic:
by_cases h : s = 0
Proof state after:
case pos
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : s = 0
⊢ False

case neg
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
⊢ False
Tactic:
obtain ⟨n, hn⟩ := WfDvdMonoid.multiplicity_finite hx.not_unit h
Proof state after:
case neg.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
⊢ False
Tactic:
obtain ⟨m, hm⟩ := WfDvdMonoid.multiplicity_finite hx.not_unit (nonZeroDivisors.ne_zero t.prop)
Proof state after:
case neg.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ (IsLocalization.mk' K s t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ False
Tactic:
rw [IsFractionRing.mk'_eq_div] at ha
Proof state after:
case neg.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ False
Theorem: exists_not_dvd_spanSingleton_eq
Proof state before:
case neg.intro.intro
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ False
Tactic:
refine this (n + m + 1) (Nat.le_add_left 1 (n + m)) ⟨s, t, ?_, ?_, ha.symm⟩
Proof state after:
case neg.intro.intro.refine_1
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ ¬x ^ (n + m + 1) ∣ s

case neg.intro.intro.refine_2
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁸ : Field K✝
inst✝⁷ : CharZero K✝
inst✝⁶ : IsCyclotomicExtension {p} ℚ K✝
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
hx : Prime x
I J : Ideal R
hI : ¬Ideal.span {x} ∣ I
hJ : ¬Ideal.span {x} ∣ J
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
hI' : ↑I ≠ 0
hJ' : ↑J ≠ 0
this :
  ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
s : R
t : ↥R⁰
ha : ↑I / ↑J = spanSingleton R⁰ ((algebraMap R K) s / (algebraMap R K) ↑t)
h : ¬s = 0
n : ℕ
hn : ¬x ^ (n + 1) ∣ s
m : ℕ
hm : ¬x ^ (m + 1) ∣ ↑t
⊢ ¬x ^ (n + m + 1) ∣ ↑t