-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- Let `(x : 𝓞 K)`. Then we have that `λ` divides one amongst `x`, `x - 1` and `x + 1`. -/
lemma lambda_dvd_or_dvd_sub_one_or_dvd_add_one [NumberField K] [IsCyclotomicExtension {3} ℚ K] :
    λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Proof state:
case inl.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x

Tactic:
exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h

Result:
no goals

Proof state:
case inr.inl.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left

Result:
case inr.inl.h.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x - 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝ : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
let _ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
rw [Finset.univ_of_card_le_three h3.le] at this

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ {0, 1, -1}
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Proof state:
case inr.inl.h.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ (Ideal.Quotient.mk (Ideal.span {λ})) (x - 1) = 0

Tactic:
rw [RingHom.map_sub, h, RingHom.map_one, sub_self]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left

Result:
case inl.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x

Proof state:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
right

Result:
case inr.inr.h
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x - 1 ∨ λ ∣ x + 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 := by
  rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one (by decide),
    hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
  simp only [PNat.val_ofNat, Nat.cast_ofNat, Int.reduceAbs]

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this✝ : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup
this : (Ideal.Quotient.mk (Ideal.span {λ})) x ∈ Finset.univ
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ 1 < 3

Tactic:
decide

Result:
no goals