Theorem: exists_not_dvd_spanSingleton_eq (FltRegular/CaseII/AuxLemmas.lean)

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

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 _)
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

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 _)
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

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

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

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

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

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

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)
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

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

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⟩
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

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
⊢ ↑I ≠ 0
Tactic:
rw [← coeIdeal_bot, Ne, coeIdeal_inj]
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
⊢ ¬I = ⊥

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
⊢ ¬I = ⊥
Tactic:
rintro rfl
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
J : Ideal R
hJ : ¬Ideal.span {x} ∣ J
hI : ¬Ideal.span {x} ∣ ⊥
h : (↑(↑⊥ / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑⊥ / ↑J
⊢ False

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
J : Ideal R
hJ : ¬Ideal.span {x} ∣ J
hI : ¬Ideal.span {x} ∣ ⊥
h : (↑(↑⊥ / ↑J)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑⊥ / ↑J
⊢ False
Tactic:
exact hI (dvd_zero _)
State after:
no goals

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
⊢ ↑J ≠ 0
Tactic:
rw [← coeIdeal_bot, Ne, coeIdeal_inj]
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
⊢ ¬J = ⊥

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
⊢ ¬J = ⊥
Tactic:
rintro rfl
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 : Ideal R
hI : ¬Ideal.span {x} ∣ I
hI' : ↑I ≠ 0
hJ : ¬Ideal.span {x} ∣ ⊥
h : (↑(↑I / ↑⊥)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑⊥
⊢ False

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 : Ideal R
hI : ¬Ideal.span {x} ∣ I
hI' : ↑I ≠ 0
hJ : ¬Ideal.span {x} ∣ ⊥
h : (↑(↑I / ↑⊥)).IsPrincipal
H1 : ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑⊥
⊢ False
Tactic:
exact hJ (dvd_zero _)
State after:
no goals

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
⊢ ∀ (n : ℕ),
    1 ≤ n → ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
intro n hn
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
n : ℕ
hn : 1 ≤ n
⊢ ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J

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
n : ℕ
hn : 1 ≤ n
⊢ ¬∃ a b, ¬x ^ n ∣ a ∧ ¬x ^ n ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
induction' n, hn using Nat.le_induction with n' hn' IH
State after:
case base
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
n : ℕ
⊢ ¬∃ a b, ¬x ^ 1 ∣ a ∧ ¬x ^ 1 ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J

case succ
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬∃ a b, ¬x ^ (n' + 1) ∣ a ∧ ¬x ^ (n' + 1) ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J

State before:
case base
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
n : ℕ
⊢ ¬∃ a b, ¬x ^ 1 ∣ a ∧ ¬x ^ 1 ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
simp_rw [pow_one]
State after:
case base
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
n : ℕ
⊢ ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J

State before:
case base
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
n : ℕ
⊢ ¬∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
exact H1
State after:
no goals

State before:
case succ
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬∃ a b, ¬x ^ (n' + 1) ∣ a ∧ ¬x ^ (n' + 1) ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
Tactic:
rintro ⟨a, b, ha, hb, e⟩
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
have e₀ := e
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
rw [div_eq_mul_inv, ← spanSingleton_mul_spanSingleton,
  ← one_div_spanSingleton, ← mul_div_assoc, mul_one, div_eq_iff,
  ← mul_div_right_comm, eq_div_iff hJ', ← coeIdeal_span_singleton, ← coeIdeal_span_singleton,
  ← coeIdeal_mul, ← coeIdeal_mul, coeIdeal_inj] at e
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False

case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ spanSingleton R⁰ ((algebraMap R K) b) ≠ 0

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False

case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ spanSingleton R⁰ ((algebraMap R K) b) ≠ 0
Tactic:
on_goal 2 =>
  rw [Ne, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
    (IsFractionRing.injective R K).eq_iff]
  rintro rfl
  apply hb (dvd_zero _)
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ False
Tactic:
by_cases h : x ^ n' ∣ a
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
⊢ 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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
⊢ False

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ spanSingleton R⁰ ((algebraMap R K) b) ≠ 0
Tactic:
rw [Ne, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
  (IsFractionRing.injective R K).eq_iff]
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬b = 0

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) b) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
⊢ ¬b = 0
Tactic:
rintro rfl
State after:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ 0
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) 0) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) 0) = ↑I / ↑J
⊢ False

State before:
case succ.intro.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ 0
e : spanSingleton R⁰ ((algebraMap R K) a) / spanSingleton R⁰ ((algebraMap R K) 0) = ↑I / ↑J
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) 0) = ↑I / ↑J
⊢ False
Tactic:
apply hb (dvd_zero _)
State after:
no goals

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
⊢ False
Tactic:
have ha' : x ∣ a := (dvd_pow_self _ (Nat.one_le_iff_ne_zero.mp hn')).trans h
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ False

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
hb' : x ∣ b
⊢ False
Tactic:
obtain ⟨a', rfl⟩ := ha'
State after:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
b : R
hb : ¬x ^ (n' + 1) ∣ b
hb' : x ∣ b
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
e : Ideal.span {x * a'} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ x * a'
⊢ False

State before:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
b : R
hb : ¬x ^ (n' + 1) ∣ b
hb' : x ∣ b
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
e : Ideal.span {x * a'} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ x * a'
⊢ False
Tactic:
obtain ⟨b', rfl⟩ := hb'
State after:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ (n' + 1) ∣ x * b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False

State before:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ (n' + 1) ∣ x * a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ (n' + 1) ∣ x * b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
Tactic:
rw [pow_succ', mul_dvd_mul_iff_left hx.ne_zero] at ha hb
State after:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False

State before:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) (x * a') / (algebraMap R K) (x * b')) = ↑I / ↑J
⊢ False
Tactic:
rw [_root_.map_mul, _root_.map_mul, mul_div_mul_left] at e₀
State after:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) a' / (algebraMap R K) b') = ↑I / ↑J
⊢ False

case pos.intro.intro.hc
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ (algebraMap R K) x ≠ 0

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
this : gcd (Ideal.span {x}) I = 1
⊢ x ∣ b
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at ha' ⊢
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
⊢ Ideal.span {x} ∣ Ideal.span {b}

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
⊢ Ideal.span {x} ∣ Ideal.span {b}
Tactic:
replace h := ha'.trans (dvd_mul_right _ J)
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
h : Ideal.span {x} ∣ Ideal.span {a} * J
⊢ Ideal.span {x} ∣ Ideal.span {b}

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
ha' : Ideal.span {x} ∣ Ideal.span {a}
this : gcd (Ideal.span {x}) I = 1
h : Ideal.span {x} ∣ Ideal.span {a} * J
⊢ Ideal.span {x} ∣ Ideal.span {b}
Tactic:
rwa [e, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at h
State after:
no goals

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ gcd (Ideal.span {x}) I = 1
Tactic:
rwa [Irreducible.gcd_eq_one_iff]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ Irreducible (Ideal.span {x})

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ Irreducible (Ideal.span {x})
Tactic:
rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ x ≠ 0

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ Ideal.span {x} ≠ ⊥

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ x ≠ 0
Tactic:
exact hx.ne_zero
State after:
no goals

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ Ideal.span {x} ≠ ⊥
Tactic:
rw [Ne, Ideal.span_singleton_eq_bot]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ ¬x = 0

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : x ^ n' ∣ a
ha' : x ∣ a
⊢ ¬x = 0
Tactic:
exact hx.ne_zero
State after:
no goals

State before:
case pos.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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) a' / (algebraMap R K) b') = ↑I / ↑J
⊢ False
Tactic:
exact IH ⟨a', b', ha, hb, e₀⟩
State after:
no goals

State before:
case pos.intro.intro.hc
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ (algebraMap R K) x ≠ 0
Tactic:
rw [Ne, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff]
State after:
case pos.intro.intro.hc
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ ¬x = 0

State before:
case pos.intro.intro.hc
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a' : R
ha : ¬x ^ n' ∣ a'
h : x ^ n' ∣ x * a'
b' : R
hb : ¬x ^ n' ∣ b'
e : Ideal.span {x * a'} * J = I * Ideal.span {x * b'}
e₀ : spanSingleton R⁰ ((algebraMap R K) x * (algebraMap R K) a' / ((algebraMap R K) x * (algebraMap R K) b')) = ↑I / ↑J
⊢ ¬x = 0
Tactic:
exact hx.ne_zero
State after:
no goals

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
⊢ False
Tactic:
refine IH ⟨a, b, h, ?_, e₀⟩
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
⊢ ¬x ^ n' ∣ b

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
⊢ ¬x ^ n' ∣ b
Tactic:
intro hb
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : x ^ n' ∣ b
⊢ False

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : x ^ n' ∣ b
⊢ False
Tactic:
apply h
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : x ^ n' ∣ b
⊢ x ^ n' ∣ a

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : x ^ n' ∣ b
⊢ x ^ n' ∣ a
Tactic:
rw [← Ideal.mem_span_singleton, ← Ideal.dvd_span_singleton] at hb ⊢
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Tactic:
replace hb := hb.trans (dvd_mul_left _ I)
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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}

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
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
this : gcd (Ideal.span {x ^ n'}) J = 1
⊢ Ideal.span {x ^ n'} ∣ Ideal.span {a}
Tactic:
rwa [← e, mul_comm, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at hb
State after:
no goals

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ gcd (Ideal.span {x ^ n'}) J = 1
Tactic:
rwa [← Ideal.isCoprime_iff_gcd, ← Ideal.span_singleton_pow,
  IsCoprime.pow_left_iff, Ideal.isCoprime_iff_gcd, Irreducible.gcd_eq_one_iff]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Irreducible (Ideal.span {x})

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 0 < n'

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Irreducible (Ideal.span {x})
Tactic:
rwa [irreducible_iff_prime, Ideal.prime_iff_isPrime, Ideal.span_singleton_prime]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ x ≠ 0

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Ideal.span {x} ≠ ⊥

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ x ≠ 0
Tactic:
exact hx.ne_zero
State after:
no goals

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ Ideal.span {x} ≠ ⊥
Tactic:
rw [Ne, Ideal.span_singleton_eq_bot]
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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ ¬x = 0

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ ¬x = 0
Tactic:
exact hx.ne_zero
State after:
no goals

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
n n' : ℕ
hn' : 1 ≤ n'
IH : ¬∃ a b, ¬x ^ n' ∣ a ∧ ¬x ^ n' ∣ b ∧ spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
a b : R
ha : ¬x ^ (n' + 1) ∣ a
hb✝ : ¬x ^ (n' + 1) ∣ b
e : Ideal.span {a} * J = I * Ideal.span {b}
e₀ : spanSingleton R⁰ ((algebraMap R K) a / (algebraMap R K) b) = ↑I / ↑J
h : ¬x ^ n' ∣ a
hb : Ideal.span {x ^ n'} ∣ I * Ideal.span {b}
⊢ 0 < n'
Tactic:
rwa [Nat.pos_iff_ne_zero, ← Nat.one_le_iff_ne_zero]
State after:
no goals

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
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:
rw [div_eq_iff hJ', h, IsLocalization.mk'_zero, spanSingleton_zero, zero_mul] at ha
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 = 0
h : s = 0
⊢ False

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
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 = 0
h : s = 0
⊢ False
Tactic:
exact hI' ha
State after:
no goals

State before:
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
Tactic:
intro hs
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
hs : x ^ (n + m + 1) ∣ s
⊢ False

State before:
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
hs : x ^ (n + m + 1) ∣ s
⊢ False
Tactic:
refine hn (dvd_trans (pow_dvd_pow _ ?_) hs)
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
hs : x ^ (n + m + 1) ∣ s
⊢ n + 1 ≤ n + m + 1

State before:
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
hs : x ^ (n + m + 1) ∣ s
⊢ n + 1 ≤ n + m + 1
Tactic:
linarith
State after:
no goals

State before:
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
Tactic:
intro ht
State after:
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
ht : x ^ (n + m + 1) ∣ ↑t
⊢ False

State before:
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
ht : x ^ (n + m + 1) ∣ ↑t
⊢ False
Tactic:
refine hm (dvd_trans (pow_dvd_pow _ (Nat.le_add_left _ _)) ht)
State after:
no goals