awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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
⊢ 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 {λ}))

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

Premises used: Finset.univ_of_card_le_three, Eq.le
-- 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
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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
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 {λ}))
⊢ Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3

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

Premises used: Finset.univ_of_card_le_three, Eq.le
-- 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
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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
⊢ 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 {λ}))

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at this

Premises used: Finset.mem_singleton, Finset.mem_insert
-- 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
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inl :
  ∀
    (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 :
  ∀
    (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₁ :
  ∀
    (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:
rcases this with h | h | h
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inl : λ ∣ x
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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

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

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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

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

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr : λ ∣ x - 1 ∨ λ ∣ x + 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
right
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr : λ ∣ x - 1
⊢ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
left
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 - 1

Tactic:
Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr :
  Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) (x - 1) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
⊢ λ ∣ x - 1

Tactic:
refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr :
  HSub.hSub (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) (β :=
      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 {λ}))
      ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) 1 :
        HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) =
    0
inr₁ :
  HSub.hSub (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) 1
      ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) 1) =
    0
inr₂ : HSub.hSub (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) 1 1 = 0
inr₃ inr₄ : Eq.{u_1 + 1} (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) 0 0
⊢ Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) (x - 1) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))

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

Premises used: sub_self, RingHom.map_one, RingHom.map_sub
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr : λ ∣ x - 1 ∨ λ ∣ x + 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
right
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr : λ ∣ x + 1
⊢ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
right
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 + 1

Tactic:
Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton
-- 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
this : Finite.{u_1 + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_1 : Fintype (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) :=
  Fintype.ofFinite (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
x_2 : Ring (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := CommRing.toRing
x_3 : AddGroup (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) := AddGroupWithOne.toAddGroup
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 {λ}))
inr :
  Eq (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) (x + 1) :
      HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
    (0 : HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ}))
⊢ λ ∣ x + 1

Tactic:
refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_

Premises used: Ideal.Quotient.eq_zero_iff_mem, Iff.mp, Ideal.mem_span_singleton