awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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 {λ}))
Tactic: have := Finset.mem_univ (Ideal.Quotient.mk (Ideal.span {λ}) x)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 {λ}))
⊢ Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3
have rw : Int.natAbs (↑3 : ℤ) = 3
Tactic: rw [← Nat.card_eq_fintype_card, hζ.card_quotient_toInteger_sub_one,
      hζ.norm_toInteger_sub_one_of_prime_ne_two' (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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 {λ}))
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have h3 : Fintype.card.{u_1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) = 3
Tactic: 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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 {λ}))
Tactic: rw [Finset.univ_of_card_le_three h3.le] at this
Cleared hypotheses: this, h3
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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 {λ}))
Tactic: simp only [Finset.mem_insert, Finset.mem_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 {λ}))
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have 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
Tactic: rcases this with h | h | h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have inl : λ ∣ x
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
have inr : λ ∣ x - 1 ∨ λ ∣ x + 1
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 ∨ λ ∣ x + 1
have inr : λ ∣ x - 1
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
have 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 {λ}))
Tactic: refine Ideal.mem_span_singleton.1 <| Ideal.Quotient.eq_zero_iff_mem.1 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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 {λ}))
⊢ 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 {λ}))
have 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
Tactic: rw [RingHom.map_sub, h, RingHom.map_one, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
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
⊢ 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 {λ}))
have inr₁ : HSub.hSub (α := HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {λ})) 1
    ((Ideal.Quotient.mk (Ideal.span {λ}) : (a : 𝓞 K) → 𝓞 K ⧸ Ideal.span {λ}) 1) =
  0
Tactic: rw [RingHom.map_sub, h, RingHom.map_one, sub_self]