-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
have have₁ have₂ have₃ have₄ have₅ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have₆ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    ∀
      (this :
        Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
          Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have₇ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    ∀
      (this :
        Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
          Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) Finset.univ
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})))
      (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have₈ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀
      (this :
        Membership.mem (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (γ :=
          Finset (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))) {0, 1, -1}
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})))
      (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have₉ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (this :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
            ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
              HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
            (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) ∨
          Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
              ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
                HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
              (1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) ∨
            Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
              ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
                HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
              (-1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
inl :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (h :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
inr :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (h :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          (1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
inr₁ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (h :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          (-1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
inr₂ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (h :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          (1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
inr₃ inr₄ :
  ∀ (this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
    let x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
      Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}));
    let x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing;
    ∀ (h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3)
      (h :
        Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) x :
            HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
          (-1 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))),
      λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
classical
  have := hζ.finite_quotient_toInteger_sub_one (by decide)
  let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
  let _ : Ring (𝓞 K ⧸ Ideal.span {λ}) := CommRing.toRing -- to speed up instance synthesis
  let _ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := AddGroupWithOne.toAddGroup -- ditto
  have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
  have h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3 := by
    rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
    simp only [Nat.cast_ofNat, Int.reduceAbs]
  rw [Finset.univ_of_card_le_three h3.le] at this
  simp only [Finset.mem_insert, Finset.mem_singleton] at this
  rcases this with h | h | h
  · left
    exact Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 h
  · right; left
    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
    rw [RingHom.map_sub, h, RingHom.map_one, sub_self]
  · right; right
    refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
    rw [RingHom.map_add, h, RingHom.map_one, neg_add_cancel]

Premises used: Finset.mem_singleton, sub_self, RingHom.map_one, Finset.mem_insert, RingHom.map_sub, Ideal.Quotient.eq_zero_iff_mem, neg_add_cancel, Iff.mp, RingHom.map_add, Ideal.mem_span_singleton